next up previous contents index
Next: Extraction Terms Up: Simulating Lambda--prl Constructs Previous: Lists

Primitive Recursive Functions

Since primitive  recursive function objects are not available in Nuprl , they have to be simulated. Consider the primitive recursive function

Shown below is a DEF that serves as a template for defining such functions.gif

    (F such that F(0,y)=(<G:base>)(y),

The DEF above could be used to define an exponentiation DEF in the following way.

    ((F such that F(0,y)=(\z.z)(y),

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