Inductive Proof System

An Inductive Proof System is an Accelerated Simulator and Decider which operates by automatically detecting and proving transition rules using Mathematical Induction.

Inductive Rule

An inductive rule is a general transition rule (a start and end configuration, generalized with variables for repetition counts) along with a proof. The proof generally has two pieces: the base case and the inductive case. Each is a list of steps where each step is (A) a specific TM transition, (B) an application of the inductive hypothesis, (C) an application of a previously defined rule.

Rule Levels

We can assign levels to any Inductive Rule. A Level 0 (L0) rule does not depend on any previously defined inductive rules. A Level 1 (L1) rule depends only upon previously proven L0 rules, etc. All L0 Rules (which only invoke the inductive hypothesis once) are Shift rules.

Example Proofs

Notation

In this article we will use the following notation for an Inductive Rule and its proof:

$P(n)$

• Proof by induction on n:
  • Base case: List of steps to prove the base case $P(0)$. Often this is the empty list since $P(0)$ is trivially true (in zero steps).
  • Inductive case: List of steps to prove $P(n+1)$ of which some can be "IH" the inductive hypothesis that $P(n)$.

Bouncer

Consider the bouncer 1RB0RC_0LC---_1RD1RC_0LE1RA_1RD1LE (bbch). We can prove the following Inductive Rules:

1. Shift (L0) Rule: $C(n):{\textrm {C>}}\;1^{n}\to 1^{n}\;{\textrm {C>}}$
   • Proof by induction on n
     • Base case: []
       $${\textrm {C>}}\;1^{0}=1^{0}\;{\textrm {C>}}$$
     • Inductive case: [C1, IH]
       $${\textrm {C>}}\;1^{n+1}\xrightarrow {C1} 1\;{\textrm {C>}}\;1^{n}\xrightarrow {IH} 1^{n+1}\;{\textrm {C>}}$$
2. Shift (L0) Rule: $E(n):1^{n}\;{\textrm {<E}}\to {\textrm {<E}}\;1^{n}$
   • Proof by induction on n
     • Base case: []
     • Inductive case: [E1, IH]
3. L1 Rule: $A(n):{\textrm {A>}}\;1^{n}\;0^{\infty }\to 1^{2n}\;{\textrm {A>}}\;0^{\infty }$
   • Proof by induction on n
     • Base case: []
     • Inductive case: [A1, C(n), C0, D0, E(n+1), E0, D1, IH]
       $${\begin{array}{l}\\{\textrm {A>}}\;1^{n+1}\;0^{\infty }&\xrightarrow {A1} &0\;{\textrm {C>}}\;1^{n}\;0^{\infty }\\&\xrightarrow {C(n)} &0\;1^{n}\;{\textrm {C>}}\;0^{\infty }\\&\xrightarrow {C0} &0\;1^{n+1}\;{\textrm {D>}}\;0^{\infty }\\&\xrightarrow {D0} &0\;1^{n+1}\;{\textrm {<E}}\;0^{\infty }\\&\xrightarrow {E(n+1)} &0\;{\textrm {<E}}\;1^{n+1}\;0^{\infty }\\&\xrightarrow {E0} &1\;{\textrm {D>}}\;1^{n+1}\;0^{\infty }\\&\xrightarrow {D1} &1^{2}\;{\textrm {A>}}\;1^{n}\;0^{\infty }\\&\xrightarrow {IH} &1^{2(n+1)}\;{\textrm {A>}}\;0^{\infty }\\\end{array}}$$
4. L2 Rule: $0^{\infty }\;1^{a}\;{\textrm {A>}}\;0^{\infty }\to 0^{\infty }\;1^{2a+6}\;{\textrm {A>}}\;0^{\infty }$
   • Proof: [A0, B0, C1, C0, D0, E(a+2), E0, D1, A(a+1)]
     $${\begin{array}{l}\\0^{\infty }\;1^{a}\;{\textrm {A>}}\;0^{\infty }&\xrightarrow {A0,B0,C1,C0,D0} &0^{\infty }\;1^{a+2}\;{\textrm {<E}}\;0^{\infty }\\&\xrightarrow {E(a+2)} &0^{\infty }\;{\textrm {<E}}\;1^{a+2}\;0^{\infty }\\&\xrightarrow {E0,D1} &0^{\infty }\;1^{2}\;{\textrm {A>}}\;1^{a+1}\;0^{\infty }\\&\xrightarrow {A(a+1)} &0^{\infty }\;1^{2a+4}\;{\textrm {A>}}\;0^{\infty }\\\end{array}}$$

We can see now that the last rule can be applied repeatedly forever, so if it is ever applied once, the TM will never halt. In fact, in this case the start config is equal to $0^{\infty }\;1^{0}\;{\textrm {A>}}\;0^{\infty }$ and thus this TM will never halt.

Tape Compression

We need some automated way to compress the tape into a tuple of integers, and decompress the tape when needed.

Macro Machine

We can divide the tape into blocks of fixed size, and merge adjacent identical blocks into one and record the number of repetitions.

Here is an example of how a half-tape is compressed using macro machine:

111110110110101010110110 0^inf
= 111 110 110 110 101 010 110 110 000^inf (use block size 3)
= 111 110^3 101 010 110^2 000^inf

Nested Repeater

We can compress the tape by looking for repeaters:

101110111 0^inf
= 1 0 1 1 1 0 1 1 1 0^inf
= 1 0 1 1 1 0 1 1^2 0^inf (use a a = a^2 for a = 1)
= 1 0 1 1 1 0 1^3 0^inf (use a a^n = a^(n+1) for a = 1)
= 1 0 1 1^2 0 1^3 0^inf (use a a = a^2 for a = 1)
= 1 0 1^3 0 1^3 0^inf (use a a^n = a^(n+1) for a = 1)
= 1 (0 1^3)^2 0^inf (use a a = a^2 for a = 0 1^3)

Decompression is simple: we only decompress the tape when the head points to a repeater:

l X> a^(n+1) r = l X> a a^n r
l X> a^0 r = l X> r

Fixed Length Repeater

1101111101111110 0^inf = 1101 (11)^2 0 (11)^3 0 0^inf (length = 2)

Others

For counters and other complex pattern, we can design some specific methods to represent them.

A typical binary counter can be represented by:

definition of C:
C(d0,d1,dh,1) = dh 0^inf
C(d0,d1,dh,2n+0) = d0 C(d0,d1,n), n>0
C(d0,d1,dh,2n+1) = d1 C(d0,d1,n), n>0
increment rule: l qR QR> C(d0,d1,dh,n) → l <QL qL C(d0,d1,dh,n+1)
where d0,d1,dh,qL,qR are tape segments, l is half-tape, QL,QR are TM states, n is positive integer.

For bell eats counters, when the head points to C, (i.e. l X> C(_,_,_,_)), if X=QL we can decompress tape in l to see whether it's prefix matches qR, if it matches we can apply the increment rule of the counter, otherwise we decompress C by expanding the definition of C (but not recursively unless the head points to C again) so that we can run the TM further. For sync bouncer counters, the counter may overflow, so we can use a different representation of the binary counter:

C'(0,0,0) = dh 0^inf
C'(2a,2b+1,0) = d0 C'(a,b,0)
C'(2a+1,2b,0) = d1 C'(a,b,0)
C'(a,b,n) is well formed iff a+b+1=2^n
increment: l qR QR> C'(a+1,b,n) → l <QL qL C'(a,b+1,n)
overflow: l qR' QR'> C'(0,b,n) → l <QL' qL' C'(2b+1,0,n+1)
where a,b,n are natural numbers, l is half-tape, QL,QR are states, and d0,d1,dh,qL,qR are tape segments.

We can also support arithmetic sequence:

0 1^2 0 1^3 0 1^4 0 1^5 = ((0 1^(2+1*i)) for i in range(4))

And some simple structural counters that can be described by a single integer:

B(1) = dh 0^inf
B(2n+0) = w^n d0 B(n)
B(2n+1) = w^n d1 B(n)
l qR QR> B(n) → l <QL qL B(n+1)