P versus NP: finite reachable symbol support

PvsNP.stmtPushSymbols

For every machine $M$ and every statement $q$ of that machine, this definition returns the set $U(q)$ of tagged symbols given by the structural recursion described here. It contains symbols that could be selected by the syntax’s push functions at any control state, even if those states or branch bodies cannot occur in an execution. Here $M$ is a TM2 machine with a finite type $K$ of stack indices and decidable equality on $K$, designated input and output indices $k_0,k_1$, stack-symbol types $\Gamma_k$, a finite type $\Lambda$ of program labels with a main label, a finite type $\sigma$ of control states with an initial state, a finite input alphabet $\Gamma_{k_0}$, and a statement $m(\ell)$ for each label $\ell\in\Lambda$. No finiteness of $\Gamma_k$ for other $k$ is assumed. A tagged symbol $(k,a)$ has $k\in K$ and $a\in\Gamma_k$; tags from different stacks remain distinct. For a statement $q$, its set $U(q)$ of syntactically possible pushed tagged symbols is recursively defined: a push onto $k$ with symbol function $f:\sigma\to\Gamma_k$ and continuation $q_0$ contributes $\{(k,f(v)):v\in\sigma\}\cup U(q_0)$; a peek, pop, or control-state load contributes only its continuation’s set; a conditional branch contributes the union of both branch sets; a jump to a program label and a halt contribute the empty set. Thus both branch bodies and all control states are counted, regardless of reachability, while a jump does not recursively inspect its target.

PvsNP.machineSymbols

For every machine $M$, this definition returns the set $U_M$ described here, as a subset of the disjoint union of its stack alphabets. It contains all input symbols whether or not they appear in a particular input, and the push sets of every labeled statement whether or not that label is reachable; it need not contain every symbol of the output or other work alphabets. Here $M$ is a TM2 machine with a finite type $K$ of stack indices and decidable equality on $K$, designated input and output indices $k_0,k_1$, stack-symbol types $\Gamma_k$, a finite type $\Lambda$ of program labels with a main label, a finite type $\sigma$ of control states with an initial state, a finite input alphabet $\Gamma_{k_0}$, and a statement $m(\ell)$ for each label $\ell\in\Lambda$. No finiteness of $\Gamma_k$ for other $k$ is assumed. A tagged symbol $(k,a)$ has $k\in K$ and $a\in\Gamma_k$; tags from different stacks remain distinct. For a statement $q$, its set $U(q)$ of syntactically possible pushed tagged symbols is recursively defined: a push onto $k$ with symbol function $f:\sigma\to\Gamma_k$ and continuation $q_0$ contributes $\{(k,f(v)):v\in\sigma\}\cup U(q_0)$; a peek, pop, or control-state load contributes only its continuation’s set; a conditional branch contributes the union of both branch sets; a jump to a program label and a halt contribute the empty set. Thus both branch bodies and all control states are counted, regardless of reachability, while a jump does not recursively inspect its target. Put $U_M=\{(k_0,a):a\in\Gamma_{k_0}\}\cup\bigcup_{\ell\in\Lambda}U(m(\ell))$, including every input-alphabet symbol and all syntactically possible pushes from every labeled statement.

PvsNP.SupportedStacks

For every machine $M$, every set $S$ of tagged symbols, and every family of finite stack lists $\operatorname{stk}(k)\in\Gamma_k^*$ indexed by all $k\in K$, this predicate means $\forall k\in K,\ \forall a\in\Gamma_k,\ a\in\operatorname{stk}(k)\Rightarrow(k,a)\in S$. No finiteness assumption is made on $S$, multiplicity and order in the stacks do not affect the condition, and all-empty stacks satisfy it even for $S=\varnothing$. Here $M$ is a TM2 machine with a finite type $K$ of stack indices and decidable equality on $K$, designated input and output indices $k_0,k_1$, stack-symbol types $\Gamma_k$, a finite type $\Lambda$ of program labels with a main label, a finite type $\sigma$ of control states with an initial state, a finite input alphabet $\Gamma_{k_0}$, and a statement $m(\ell)$ for each label $\ell\in\Lambda$. No finiteness of $\Gamma_k$ for other $k$ is assumed. A tagged symbol $(k,a)$ has $k\in K$ and $a\in\Gamma_k$; tags from different stacks remain distinct.