Roll your own induction principles

November 18th, 2005 by James Chapman

The other day I tried to write division on natural numbers in epigram. This function is not obviously structurally recursive so we cannot use the standard justification ‘<=rec ‘ to justify our recursive calls and also leave our function looking like the one we wanted to write in the first place. We can exhibit a view to do a custom case analysis that does the necessary subtraction for us yielding patterns of arguments to ‘plus’ (this is the Compare view from VFL). We can then exhibit another view to justify the recursive call on an argument to ‘plus’. I found a likely candidate in Edwin Brady’s thesis and Conor informed me that it first saw the light of day in a talk by James McKinna in 2002. It’s called ‘PlusRec’ and I don’t understand it.

One Response to “Roll your own induction principles”

  1. Hank Says:

    Hi James,

    There’s a definition of division, or more precisely [a/b] on page 223 of Kleene’s
    “Introduction to Metamathematics”. It’s by plain old type 0 primitive recursion.
    I’ll write it out, followed by the definitions it needs. (I admit it needs a bit of
    staring to see it’s correct.)

    [0/b] = 0
    [a'/b] = [a/b] + sgbar | b – (rm(a,b))’ |

    rm(0,b) = 0
    rm(a’,b) = (rm(a,b))’ . sg | b – (rm(a,b))’ |

    |a – b| = (a .- b) + (b -. a)

    a -. 0 = a
    a -. b’ = pd(a -. b)

    sgbar 0 = 1
    sgbar b’ = 0

    sg a = sgbar(sgbar a)

    I hope that’s enough!

Leave a Reply