Adding Recursive Definitions

Nuprl 's object language contains terms for doing recursion over types such as lists and integers. These terms can be awkward to use, and we recommend instead that all recursive definitions are built using the Y combinator  . The ML function recdef  greatly simplifies constructing general recursive definitions using the Y-combinator. recdef  also takes care of introducing a well-formedness lemma for the definition. Its usage is:

The term tdef should have structure

where the term lhs has form

, the variables are a subset of the variables variables , and none of the variables are free in any of the antecedent propositions .

recdef allows you to create recursive definitions with both curried arguments supplied by application, and subterm arguments . The parameters are specified as in abstraction definitions.

The rhs term should include at least one instance of the head of the application in lhs. That is, a term of form

where the 's are the same as in lhs. All the free variables in lhs should be appropriately typed in the context . place is a library position.

On evaluation of recdef, four objects are added to the library.

• A display object named id _df which defines a default display form for the id term.

• an abstraction object named id which defines the abstraction

  

• An ML object named id_ml . This contains an invocation of a ML function that updates caches that hold information conversions related to the definition. These conversions are described below. This function invocation is given the display form:

  

  and it serves to document the recursive definition. For this reason, the abstraction objects in recursive definitions are usually made invisible in theory listings.

• A theorem object named id_wf for a well-formedness theorem. The goal of the theorem is constructed from the tdef term. It has form

  

  An initial tactic is executed on the goal of this theorem to set up a subgoal that is usually suitable for induction. You then need to go in and complete the proof of this theorem yourself.

As with def, so_apply abstraction should be used for the second-order variables in lhs and rhs. recdef takes care of converting these to second-order variables for the abstraction object.

The basic conversions associated with a recursive definition are RecUnfoldTopC and RecFoldTopC. If the definition has arguments provided by application, then additional conversions RecEtaExpC and RecEtaConC are defined to =-expand and -contract the definition. More information on these and related conversions can be found in Section .

An example invocation of recdef from the ML Top Loop is:

This creates the following library objects: