next up previous contents index
Next: Conversion Descriptions Up: Rewriting Previous: Introduction to Conversions

Nuprl Conversions

 

In Nuprl, convn  is an ML concrete type abbreviation for the type

env -> term -> (term # reln # just). env  , reln  and just  are abstract types for environments , relations  and justifications  . A conversion is a function that takes as arguments an environment e and a term to be rewritten t, and returns a triple . The environment e specifies amongst other things the types of all the variables which might be free in the term t. The term is the rewritten version of the term t. The relation r specifies the relationship between t and . Writing r using infix notation, we can say that is true. The relation r is usually some equivalence relation but it also can be an order relation. The justification j is an object that tell Nuprl how to prove that . Conversions fail if they are not appropriate for the term they are applied to. More information on environments, rewrite relations, and justifications can be found in Section gif ,Section gif and Section gif

respectively.

A tactic Rewrite : convn -> int -> tactic   is used for applying a conversion to some clause of a sequent. It takes care of executing the justifications generated by conversions. Section gif

lists common variations on this tactic.

Atomic conversions   are either based on direct computation rules or can be created from lemmas and hypotheses. Conversions are composed using higher order functions called conversionals in a way similar to the way in which tactics are composed using tacticals. One set of conversionals are for controlling the sequence in which atomic conversions are applied to the subterms of a term.

Conversionals rely for their correct functioning on a variety of different kinds of lemmas being proven about the relations r and the terms making up any clause being rewritten; lemmas are required that state reflexivity, transitivity and symmetry properties of the relations r and congruence properties of the terms making up the clauses. These lemmas are described in Section gif .



next up previous contents index
Next: Conversion Descriptions Up: Rewriting Previous: Introduction to Conversions



Karla Consroe
Wed Oct 23 13:48:45 EDT 1996