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” fi and gi that are defined by:

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

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

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

Base step:

f0(x, y) = w == g0(x, y)

f1(x, y) = P(x) ? y : H(x, f0(N(x)))

= P(x) ? y : w

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

= g1(x,y)

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

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

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

by the induction hypothesis

= P(x) ? y : P(N(x)) ? H(y): H(fi-1(N2(x), H(y)))

= P(x) ? y : H(P(N(x)) ? y : fi-1(N2(x), H(y))

by “factoring” H out of the conditional

= P(x) ? y : H( P(N(x)) ? y : gi-1(N2(x), H(y)))

by the induction hypothesis

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

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

== fi(x, y)


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