2025年10月22日¶

\(\newcommand{Cone}{\mathop{\operatorname{cone}}}\) \(\newcommand{Span}{\mathop{\operatorname{span}}}\) \(\newcommand{Supp}{\mathop{\operatorname{supp}}}\)

(Max)-Geometrical 4-VASS is Tower-hard¶

Max geometrical dimension means to take max over geometrical dimensions in each SCC.

We start by examining the construction showing 8-VASS to be Tower-hard.

The goal is to produce a triple \((\text{Tower}(n), c, c \cdot \text{Tower}(n))\) to simulate tower-bounded zero tests.
We start with the triple \((8, c, 8 \cdot c)\) where \(c\) is guessed.
The amplifier can take triple \((8 B, C, 8 BC)\) and a pad counter to produce \((2^B, C', 2^B C')\) for \(C'\) guessed.
We then flush this triple back (times 8) for the next iteration.
There will be \(n\) iterations with \(n\) from the input.

Given counter names \(\texttt{b, c, d, b', c', d', t}\). Note that controlling counter does not increase (max) geometrical dimension, so we ignore it. The most complex SCC is the amplifier:

b' += 1
loop: c' += 1;  d' += 1

loop[with b', d', t zero tested]:
    // multiply b' by 256

    loop: b' -= 1; t += 256         [Modify c properly: c += 256 - 1]
    ZT(b' using b, c, d)
    loop: b' += 1; t -= 1           [Modify c properly: c += 1 - 1]
    ZT(t using b, c, d)

    // multiply d' by 256

    loop: d' -= 1; t += 256         [Modify c properly: c += 256 - 1]
    ZT(d' using b, c, d)
    loop: d' += 1; t -= 1           [Modify c properly: c += 1 - 1]
    ZT(t using b, c, d)

Inside the big outer loop, it is maintained that \(\Delta(b' + d' + t + c) = 0\), making the geo-dim 1 lower than number of counters touched (notice that \(c'\) is not touched, so we get \(6 - 1 = 5\)).

The idea is to separate the two inner multiplications into 2 loops, each multiply one counter.

For that, we need two copies of original triples \(b_1, c_1, d_1\) and \(b_2, c_2, d_2\) that are identical initially. When multiplying \(b'\) we use the first triple, and when multiplying \(d'\) we use the second.

To save one more counter, we can actually merge \(d_1\) and \(d_2\).

Misc.¶

With max-geometrical dimension, one don't need to use controlling counters for zero tests --- just make enough copies of counters and drop them one by one.

About PVASS, BVASS¶

1-thin PVASS with \(d\) counters and \(k\) indices (i.e. SCC level drops at most \(k\)) can be reduced to C-m-eVASS with 2d counters.

For a production \(S \to w_1 S' w_2\) where \(S\) and \(S'\) are in the same SCC of rule graph, we add transition \(q_S \to q_{S'}\) whose effect has: 1. on the first \(d\) counters, the composed reachability relation of \(w_1\) 2. on the last \(d\) counters, the reversed composed reachability relation of \(w_2\).

The source would be \((\mathbf{s}, \mathbf{t})\) and we aim to reach a configuration \((\mathbf{x}, \mathbf{x})\).
1-thin PVASS with \(k\) indices has finite reachability set \(F_k\):

for \(F_0(n) = 2n\): \(F_0 \to (-1)\; F_0\; 2\)

for \(F_d(n) = F_{d-1}^n(1)\): \(F_d \to (-1) F_d F_{d-1}\).
complexity of PVASS is claimed to be \(F_{\omega^{d+4}}\).
Decidability of \(d\)-BVASS is claimed to appear in LICS 2026, together with the above result.