| I can not agree with the claim that Bitcoin's Script Interpreter is 2PDA as it is defined in Hopcroft et al. Definition of the 2PDA as given by Hopcroft relies on the notion of looping with the number of loop iterations not known or fixed in advance. For example: p. 351 (2nd ed), proof of the theorem 8.13 that you referenced, items 5 and 6 state: 5. [Our two-stack machine S] simulates a move of [one-tape Turing machine] M as follows: .... 6. S accepts if the new state of M is accepting. Otherwise, S simulates another move of M in the same way. Bitcoin script is only capable of doing the "Otherwise, S simulates another move of M in the same way." part a limited, predetermined number of times. The book introduces the notion of language accepted by PDA and TM in exactly the same way. See, for example, sections 6.2.1 "Acceptance by final state" and 6.2.2 "Acceptance by Empty Stack" that formalize the notion of language accepted by the PDA. Both of them feature "many transition steps" notation, without specifying the upper bound on the number of steps. If the upper bound is fixed, any language accepted by such PDA could be trivially extended to not be accepted by iteration-limited PDA, but still be accepted by the PDA without iteration limit. So Bitcoin's Script Interpreter is NOT an implementation of 2-PDA, and Minsky's Theorem is not applicable. |
E.g. In bitcoin script any encounter with OP_RETURN moves you immediately into an accepting state whereupon the program halts and interpreter performs a predicate evaluation on the state of the stack.
Hopcroft et. al. also makes no claim on the input to the FSM being infinite (requiring an infinite loop). Quite the opposite. The FSM clearly reads the Program until it encounters a "simulated blank" signifying the end of input, so it can start processing the "tape".
A simpler way of satisfying the requirement of Bitcoin Script Interpreter as a 2-PDA is simply to define the State Transition function in terms of Bitcoin Script Primitives.
Q × ( ∑ ∪ {ε} ) × S × Q × S*
Where:
* Q is the finite number of states
* ∑ is input alphabet
* S is stack symbols
* q0 is the initial state (q0 ∈ Q)
* I is the initial stack top symbol (I ∈ S)
* F is a set of accepting states (F ∈ Q)
Resolving each of the above is left as an exercise to the reader.
I do concede that the actual usefulness of the computation is limited to the extent that the Bitcoin Implementation limits the size of the "input tape" i.e. the limits on size of Script.
Hence the need for Big Blocks and unbounded Script sizes to allow the market to discover the correct trade-offs between economic benefit and computational cost.