Inductive Proof System - Revision history

Polygon: Added category:analysis techniques

2025-10-31T23:23:57Z

Added category:analysis techniques

← Older revision		Revision as of 23:23, 31 October 2025
Line 230:		Line 230:

	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.		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.
	[[Category:Deciders]]		[[Category:Deciders]][[Category:Analysis Techniques]]

Int-y1: standardize

2025-10-08T07:25:35Z

standardize <pre>

← Older revision		Revision as of 07:25, 8 October 2025
Line 74:		Line 74:
	We can divide the tape into blocks of fixed size, and merge adjacent identical blocks into one and record the number of repetitions.		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:<pre>		Here is an example of how a half-tape is compressed using macro machine:
			<pre>
	111110110110101010110110 0^inf		111110110110101010110110 0^inf
	= 111 110 110 110 101 010 110 110 000^inf (use block size 3)		= 111 110 110 110 101 010 110 110 000^inf (use block size 3)
Line 81:		Line 82:

	=== Nested Repeater ===		=== Nested Repeater ===
	We can compress the tape by looking for repeaters:<pre>		We can compress the tape by looking for repeaters:
			<pre>
	101110111 0^inf		101110111 0^inf
	= 1 0 1 1 1 0 1 1 1 0^inf		= 1 0 1 1 1 0 1 1 1 0^inf
Line 89:		Line 91:
	= 1 0 1^3 0 1^3 0^inf (use a a^n = a^(n+1) 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)		= 1 (0 1^3)^2 0^inf (use a a = a^2 for a = 0 1^3)
	</pre>Decompression is simple: we only decompress the tape when the head points to a repeater:<pre>		</pre>
			Decompression is simple: we only decompress the tape when the head points to a repeater:
			<pre>
	l X> a^(n+1) r = l X> a a^n r		l X> a^(n+1) r = l X> a a^n r
	l X> a^0 r = l X> r		l X> a^0 r = l X> r
Line 102:		Line 106:
	For counters and other complex pattern, we can design some specific methods to represent them.		For counters and other complex pattern, we can design some specific methods to represent them.

	A typical binary counter can be represented by:<pre>		A typical binary counter can be represented by:
			<pre>
	definition of C:		definition of C:
	C(d0,d1,dh,1) = dh 0^inf		C(d0,d1,dh,1) = dh 0^inf
Line 109:		Line 114:
	increment rule: l qR QR> C(d0,d1,dh,n) → l <QL qL C(d0,d1,dh,n+1)		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.		where d0,d1,dh,qL,qR are tape segments, l is half-tape, QL,QR are TM states, n is positive integer.
	</pre>For [[Bell eats counter\|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.		</pre>
			For [[Bell eats counter\|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 counter\|sync bouncer counters]], the counter may overflow, so we can use a different representation of the binary counter:<pre>		For [[Sync bouncer counter\|sync bouncer counters]], the counter may overflow, so we can use a different representation of the binary counter:
			<pre>
	C'(0,0,0) = dh 0^inf		C'(0,0,0) = dh 0^inf
	C'(2a,2b+1,0) = d0 C'(a,b,0)		C'(2a,2b+1,0) = d0 C'(a,b,0)
Line 119:		Line 126:
	overflow: l qR' QR'> C'(0,b,n) → l <QL' qL' C'(2b+1,0,n+1)		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.		where a,b,n are natural numbers, l is half-tape, QL,QR are states, and d0,d1,dh,qL,qR are tape segments.
	</pre>We can also support arithmetic sequence:<pre>		</pre>
			We can also support arithmetic sequence:
			<pre>
	0 1^2 0 1^3 0 1^4 0 1^5 = ((0 1^(2+1*i)) for i in range(4))		0 1^2 0 1^3 0 1^4 0 1^5 = ((0 1^(2+1*i)) for i in range(4))
	</pre>And some simple structural counters that can be described by a single integer:<pre>		</pre>
			And some simple structural counters that can be described by a single integer:
			<pre>
	B(1) = dh 0^inf		B(1) = dh 0^inf
	B(2n+0) = w^n d0 B(n)		B(2n+0) = w^n d0 B(n)
Line 134:		Line 145:
	We can prove special rules, and generalize them by interpolation (and maybe also need to generalize their proof).		We can prove special rules, and generalize them by interpolation (and maybe also need to generalize their proof).

	Example:<pre>		Example:
			<pre>
	0^inf A> 0^inf → 0^inf A> 0 0^inf		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 A> 0 0^inf → 0^inf 1 A> 0^inf
Line 159:		Line 171:
	induction:		induction:
	0^inf 1^2 A> 0^inf → 0^inf 1^(2+n) A> 0^inf		0^inf 1^2 A> 0^inf → 0^inf 1^(2+n) A> 0^inf


	</pre>		</pre>

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

	Example:<pre>		Example:
			<pre>
	l A> 0^inf → l A> 0 0^inf		l A> 0^inf → l A> 0 0^inf
	l A> 0 r → l 1 A> r		l A> 0 r → l 1 A> r
Line 199:		Line 210:
	induction:		induction:
	l 1^n A> 0^inf → l 1^(n+m) A> 0^inf		l 1^n A> 0^inf → l 1^(n+m) A> 0^inf
			</pre>
			A method for solving equations (similar to unification in type theory):
	</pre>A method for solving equations (similar to unification in type theory):<pre>		<pre>
	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.		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:		Then we simplify the rule (B=C -> X -> Y -> A→D) by solving equantions in the premise:

MrSolis: :3

2025-10-07T23:25:48Z

← Older revision		Revision as of 23:25, 7 October 2025
Line 21:		Line 21:
	Consider the [[bouncer]] {{TM\|1RB0RC_0LC---_1RD1RC_0LE1RA_1RD1LE\|non-halt}}. We can prove the following Inductive Rules:		Consider the [[bouncer]] {{TM\|1RB0RC_0LC---_1RD1RC_0LE1RA_1RD1LE\|non-halt}}. We can prove the following Inductive Rules:

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

	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 <math>0^\infty \; 1^0 \; \textrm{A>} \; 0^\infty</math> and thus this TM will never halt.		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 <math>0^\infty \; 1^0 \; \textrm{A}\textrm{>} \; 0^\infty</math> and thus this TM will never halt.

	== Tape Compression ==		== Tape Compression ==

Mxdys: unification in inductive decider

2024-11-16T08:14:37Z

unification in inductive decider

← Older revision		Revision as of 08:14, 16 November 2024
Line 201:		Line 201:


			</pre>A method for solving equations (similar to unification in type theory):<pre>
			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 ax+b=cy+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 a1x1+a2x2+...+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.
	</pre>		</pre>

Mxdys: Find and Prove Rules in Inductive Decider

2024-11-15T21:47:10Z

Find and Prove Rules in Inductive Decider

@@ Line 127: / Line 127: @@
 l qR QR> B(n) → l <QL qL B(n+1)
 </pre>
 [[Category:Deciders]]

Mxdys: tape compression methods for inductive decider

2024-11-15T20:04:23Z

tape compression methods for inductive decider

← Older revision		Revision as of 20:04, 15 November 2024
Line 67:		Line 67:

	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 <math>0^\infty \; 1^0 \; \textrm{A>} \; 0^\infty</math> and thus this TM will never halt.		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 <math>0^\infty \; 1^0 \; \textrm{A>} \; 0^\infty</math> 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:<pre>
			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
			</pre>

			=== Nested Repeater ===
			We can compress the tape by looking for repeaters:<pre>
			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)
			</pre>Decompression is simple: we only decompress the tape when the head points to a repeater:<pre>
			l X> a^(n+1) r = l X> a a^n r
			l X> a^0 r = l X> r
			</pre>

			=== Fixed Length Repeater ===
			<pre>
			1101111101111110 0^inf = 1101 (11)^2 0 (11)^3 0 0^inf (length = 2)
			</pre>

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

			A typical binary counter can be represented by:<pre>
			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.
			</pre>For [[Bell eats counter\|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 counter\|sync bouncer counters]], the counter may overflow, so we can use a different representation of the binary counter:<pre>
			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.
			</pre>We can also support arithmetic sequence:<pre>
			0 1^2 0 1^3 0 1^4 0 1^5 = ((0 1^(2+1*i)) for i in range(4))
			</pre>And some simple structural counters that can be described by a single integer:<pre>
			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)
			</pre>
	[[Category:Deciders]]		[[Category:Deciders]]

DF376: /* Bouncer */

2024-08-13T13:11:17Z

Bouncer

← Older revision		Revision as of 13:11, 13 August 2024
Line 19:		Line 19:

	=== Bouncer ===		=== Bouncer ===
	Consider the [[bouncer]] {{TM\|1RB0RC_0LC---_1RD1RC_0LE1RA_1RD1LE}}. We can prove the following Inductive Rules:		Consider the [[bouncer]] {{TM\|1RB0RC_0LC---_1RD1RC_0LE1RA_1RD1LE\|non-halt}}. We can prove the following Inductive Rules:

	# Shift (L0) Rule: <math>C(n) : \textrm{C>} \; 1^n \to 1^n \; \textrm{C>}</math>		# Shift (L0) Rule: <math>C(n) : \textrm{C>} \; 1^n \to 1^n \; \textrm{C>}</math>

Sligocki: Add example

2024-07-17T04:25:19Z

Add example

@@ Line 4: / Line 4: @@
 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.
-TODO(Shawn): Give examples
+=== Rule Levels ===
 [[Category:Deciders]]

Sligocki at 04:34, 24 June 2024

2024-06-24T04:34:50Z

← Older revision		Revision as of 04:34, 24 June 2024
Line 5:		Line 5:

	TODO(Shawn): Give examples		TODO(Shawn): Give examples
			[[Category:Deciders]]

Sligocki at 20:03, 14 June 2024

2024-06-14T20:03:13Z

← Older revision		Revision as of 20:03, 14 June 2024
Line 1:		Line 1:
	An '''Inductive Proof System''' is an [[Accelerated Simulator]] and [[Decider]] which operates by automatically detecting and proving [[Transition rule\|transition rules]] using Mathematical Induction.		An '''Inductive Proof System''' is an [[Accelerated Simulator]] and [[Decider]] which operates by automatically detecting and proving [[Transition rule\|transition rules]] using Mathematical Induction.

	TODO(Shawn): ~~Provide formal definition.~~		== 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.

			TODO(Shawn): Give examples