Truncation Induction

Here is an example of something I could prove that McCarthy couldn’t:

Given the equations:

f(x,y) = P(x) ? y : H(f(N(x)))

g(x,y) = P(x) ? y : g(N(x), H(y))

The functions f and g are equivalent, regardless of what x, P, H, and N are.

In normal induction we needed N(x) to be something that drives x towards a value in which P is true. Instead we do it by inventing a series of “truncated functions” f_i and g_i that are defined by:

f₀, and g₀ are both the empty function. We say f₀(x, y) or g₀(x, y) is w, meaning undefined or the program Runs forever.

function f_i+1(x, y) = P(x) ? y : H(f_i(N(x)))

g_i+1(x, y) = P(x) ? y : g_i(N(x), H(y))

Base step:

f₀(x, y) = w == g₀(x, y)

f₁(x, y) = P(x) ? y : H(x, f₀(N(x)))

= P(x) ? y : w

= P(x) ? y : g₀(N(x), H(y))

= g₁(x,y)

Induction step: Assume it’s true for all 1≤ i

g_i+1(x,y) = P(x) ? y : g_i(N(x), H(y))

= P(x) ? y : f_i(N(x), H(y))

by the induction hypothesis

= P(x) ? y : P(N(x)) ? H(y): H(f_i-1(N²(x), H(y)))

= P(x) ? y : H(P(N(x)) ? y : f_i-1(N²(x), H(y))

by “factoring” H out of the conditional

= P(x) ? y : H( P(N(x)) ? y : g_i-1(N²(x), H(y)))

by the induction hypothesis

= P(x) ? y : H(g_i(N(x), y))

= P(x) ? y : H(f_i(N(x),y) by the induction hypothesis

== f_i(x, y)

QED

This result holds regardless of whether the functions are defined or not.