Subject: Term

Keywords: ::abstraction

Title: Definition

--------------------------------------------------

Definitions are a method of encoding term expansions.
A definition consists of a lhs or model term and a rhs or
expansion. The lhs may have variable parameters and first or
second order variable subterms. A subterm may also be a literal
term. Importantly though, a lhs subterm can only be a variable
or a completely literal term, ie the subterm may not contain
a variable. It can be a variable, but cannot contain a variable.

No two lhs may match any single term instance. Thus there can never
be any ambiguity over which definition is used to expand an a term.

We use the words abstraction and definition interchangeably. 
Definition may be the more generic word, and abstraction our 
implementation of a definition. This is not a convention that 
we strictly enforce.

Definitions are specified in ABS objects.   

Definitions are an integral part of nuprl formal content.
However they are also used extensively as macro device for ML
expressions, especially in Tactic Expressionss in proofs.

Definitions are unfolded by matching an instance to the lhs 
and then substituting (See Substition) into the rhs.⋅
--------------------------------------------------

Authors: 

Contributors: RICH:t

⋅

Home