next up previous contents index
Next: Partial Function Types Up: Recursive Definition Previous: Computation

Example Proof

The dom predicate defined earlier in the chapter is used here to demonstrate induction. Given the definitions

     ~<T>== (<T>) -> void
     some <v>:<A>.<P>== <v>:(<A>)#(<P>)
     N== {n:int| ~(n<0)}
     true== (0 in int)
     D(<x>)== rec(dom,x. int_eq(f(x); 0; true; dom(x+1)); <x>)
figure gif sketches the proof of
     f:N->N, r:D(0) >> some y:N. f(y)=0.
Although D(0) is inhabited only by axiom, evaluating the extracted term produces a root.

Figure: A Sample Proof Using Recursion

Richard Eaton
Thu Sep 14 08:45:18 EDT 1995