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)

Find and Prove Rules

We need some automated way to find rules and prove/use them.

Find New Rule by Generalizing Known Rules

We can prove special rules, and generalize them by interpolation (and maybe also need to generalize their proof).

Example:

0^inf A> 0^inf → 0^inf A> 0 0^inf
0^inf A> 0 0^inf → 0^inf 1 A> 0^inf
0^inf 1 A> 0^inf → 0^inf 1 A> 0 0^inf
0^inf 1 A> 0 0^inf → 0^inf 1 1 A> 0^inf
0^inf 1 1 A> 0^inf → 0^inf 1^2 A> 0^inf

0^inf 1^2 A> 0^inf → 0^inf 1^2 A> 0 0^inf
0^inf 1^2 A> 0 0^inf → 0^inf 1^2 1 A> 0^inf
0^inf 1^2 1 A> 0^inf → 0^inf 1^3 A> 0^inf

0^inf 1^3 A> 0^inf → 0^inf 1^3 A> 0 0^inf
0^inf 1^3 A> 0 0^inf → 0^inf 1^3 1 A> 0^inf
0^inf 1^3 1 A> 0^inf → 0^inf 1^4 A> 0^inf

interpolation:
0^inf 1^(2+i) A> 0^inf → 0^inf 1^(2+i) A> 0 0^inf
0^inf 1^(2+i) A> 0 0^inf → 0^inf 1^(2+i) 1 A> 0^inf
0^inf 1^(2+i) 1 A> 0^inf → 0^inf 1^(3+i) A> 0^inf

merge:
0^inf 1^(2+i) A> 0^inf → 0^inf 1^(3+i) A> 0^inf

induction:
0^inf 1^2 A> 0^inf → 0^inf 1^(2+n) A> 0^inf

Find New Rule by Specializing Known Rules

We can maintain a sequence of used rules, and keep the rules as general as possible, then specialize the rules when needed.

Example:

l A> 0^inf → l A> 0 0^inf
l A> 0 r → l 1 A> r
l A> 0^inf → l A> 0 0^inf
l A> 0 r → l 1 A> r
l 1 1 A> r → l 1^2 A> r

l A> 0^inf → l A> 0 0^inf
l A> 0 r → l 1 A> r
l 1^n 1 A> r → l 1^(n+1) A> r

l A> 0^inf → l A> 0 0^inf
l A> 0 r → l 1 A> r
l 1^n 1 A> r → l 1^(n+1) A> r

to merge
l1 A> 0^inf → l1 A> 0 0^inf
l2 A> 0 r2 → l2 1 A> r2
we need to solve equation:
l1 A> 0 0^inf = l2 A> 0 r2
then we have l1=l2, 0^inf=r2 and substitute them:
l2 A> 0^inf → l2 A> 0 0^inf
l2 A> 0 0^inf → l2 1 A> 0^inf
and then these two rules are ready to be merged as
l2 A> 0^inf → l2 1 A> 0^inf
then we can merge
l2 A> 0^inf → l2 1 A> 0^inf
l 1^n 1 A> r → l 1^(n+1) A> r
in a similar way into
l 1^n A> 0^inf → l 1^(n+1) A> 0^inf

induction:
l 1^n A> 0^inf → l 1^(n+m) A> 0^inf

A method for solving equations (similar to unification in type theory):

First we use ((X -> A→B) /\ (Y -> C→D)) -> (B=C -> X -> Y -> A→D) to get a rule A→D that has premises B=C,X,Y.
Then we simplify the rule (B=C -> X -> Y -> A→D) by solving equantions in the premise:
If (a,b)=(c,d) is in the premise list, we can replace it with a=c, b=d, where (x,y) can be tape segment concatenation (x y), tape segment repeation (x^y) or something similar.
If a=b is in the premise list, a is variable, we substitute all occurence of a by b in the rule.
If a*x+b=c*y+d is in the premise list, x,y are natural number variables, a,b,c,d are natural number constants, we can divide a,b,c,d by gcd(a,b,c,d) and then substitute x,y by a'*x'+b',c'*x'+d' based on some number theory methods.
For an expression of natural numbers, we can simplify it as a1*x1+a2*x2+...+an*xn+b, where a1,a2,...,an,b are natural number constants.
We can remove a=a from the premise list.
If the premise list is not empty after using these methods repeatly, we just leave it as part of the rule.

Recursive Record-Breaking Analysis

We can run a Turing machine on a tape segment until it leaves the tape segment.

In this process, every time the Turing machine visits a new position, we recursively consider when the Turing machine will leave the positions it has already visited (i.e. visit the next new position or leave the current tape segment).

We can use memoize search in this process for acceleration, and regard the process of leaving a tape segment as a rule. Then the rule sequence (or rule dependency graph) may be generalized to new induction rules.