Abstractions

Abstractions  are terms which are definitionally equal  to other terms. They are introduced by abstraction objects in Nuprl theories. An abstraction can be defined in terms of other abstractions, but the dependency graph for abstractions should be acyclic. In particular, an abstraction may not depend on itself. Recursive definitions can be introduced as described in Section .

Abstraction definitions have form:

lhs == rhs

The terms lhs  and rhs  are pattern terms, and there is implicit universal quantification over the the free variables in lhs and rhs. When Nuprl unfolds  some instance lhs-inst of lhs, it first matches lhs-inst against lhs, generating bindings for the free variables of lhs such that if the bindings were applied as a substitution to lhs, one would get back lhs-inst. It then applies the substitution to rhs to calculate the term rhs-inst which lhs-inst unfolds to.

For an example of a abstraction, see Figure . Here we define a type of segments of integers.

  
Figure: Definition of the int_seg abstraction

The structure of the left-hand side is more redily apparent if we write it in uniform syntax: i..j

is int_seg(i;j), a term with opid int_seg, no parameters, and 2 subterms. An instance of the left-hand side is ..10

and this would unfold to k: k < 10 .

Abstractions can have binding structure; for example, consider the exists unique abstraction in Figure .

  
Figure: Definition of the exists_uni abstractions

To handle abstractions with binding variables in a systematic way, we define the procedure for unfolding an abstraction using second-order  matching and substitution functions.

If you are familiar with second-order matching  and substitution, you can skip this paragraph. First-order  and substitution functions are inadequate for handling terms with binding structure.

For example, there is no way of applying a first order substitution to the pattern term ``'' to get the instance ``''; if we attempt to apply the substitution to ``'', we force renaming of the bound variable x to , and we get ``''. One could somehow suppress renaming but then substitution becomes ill-behaved; on substitution, free variables can become bound - a process known as capture  . For more on this, consult some introductory book on predicate logic.

A second-order binding  is a binding of a second-order variable to a second-order term . A second-order variable  is essentially an identifier as with normal variables, but it also has an associated arity  ; some . Second-order terms are a generalization of terms, and can be represented by bound-terms such as . They can be thought of as `terms with holes  ', terms with zero or more subtrees missing. The binding variables are place-holders for the missing subtrees. In any second-order binding , the arity of v must be equal to n.

An instance of a second-order  variable v with arity n, is a term we write as , where are terms. We call the arguments of v .

A second-order substitution  is a list of second-order bindings. The result of applying the binding to the variable instance , is the term -- the second-order variable's arguments filling the holes of the second-order term.

Going back to the example, the variable P is a second order variable with arity 1, and the terms P[u] and P[v] are second-order-variable instances. Consider unfolding an instance of the left-hand side, say the term

!i: . i = 0

. Here, `` = '' is a 3 place typed equality relation. a = b T means that a and b are equal, and are both members of type T. The substitution generated by matching this against !u:T. P[u]

would be

P i.i = 0 T

and the result of applying this to

u:T. P[u] v:T. P[v] v = u T

would be

!u: . u = 0 v: . v = 0

v = u .

The matching and substitution functions used by Nuprl are a little smarter than shown above; they try to maintain names of binding variables  . So the result one would get using Nuprl would be:

!i: . i = 0 v: . v = 0

v = i .

Just as abstractions can be unfolded by applying their definition left-to-right, so instances of their right-hand sides can be folded up to be instances of their left-hand sides. Folding doesn't always work. For example, information can be lost in the unfolding process; Definitions can have variables, parameters and terms that occur on the left-hand side but that don't occur on the right-hand side .

Note that only variables and second-order variables with all first-order variable arguments are allowed as subterms of the left-hand side of abstraction definitions.

Abstractions can also contain meta-parameters  , which the matching and substitution functions treat as variables. We usually indicate that a parameter is meta, be prefixing it with a $ sign . For example, we might define an abstraction label x:t,i:n , as shown in Figure .

  
Figure: An abstraction with meta-parameters

However, note that all level-expression variables  occurring in level-expression  parameters in abstraction definitions are always treated as meta-parameters  , so there is no need to make them explicitly meta.

In general, the term on the left-hand side of an abstraction can have a mixture of normal and meta parameters. You can define a family of abstractions which differ only in the constant value of some parameter. However it is an error to make two abstraction definitions with left-hand sides which have some common instance.

A recently added feature of abstraction definitions is an optional list of conditions. A condition  is simply an alpha-numeric label associated with the abstraction. We intend abstraction conditions to be used to hold information about abstractions which would be useful to tactics and other parts of the Nuprl system. For example, abstraction conditions could be used to group abstactions into categories, and when doing a proof, one could ask for all abstractions in a given category to be treated in a particular way.

The general form of an abstraction with conditions is:

(,,):: lhs == rhs

In this section, we describe the editor support for entering abstraction definitions. Abstraction objects are created and viewed as described in Chapter 4. You can also view the abstraction for some term by using the VIEW-ABSTRACTION command. See Section .

  
Table: Editor commands for Abstraction Objects

The editor support commands are summarized in Table .

When an abstraction object is first visited, it is initialized with an uninstantiated abstraction definition term. This looks like:

[lhs] == [rhs]

If you delete the whole term in an abstraction object and then give the INITIALIZE command the object is re-initialized to this state.

The default abstraction  definition term has an empty condition sequence as a subterm. You cannot position a cursor  at this sequence because a display form hides it. Use the SELECT-TERM-OPTION command with a term cursor over the whole abstraction definition to get an abstraction definition term with an empty term slot for a condition term.

Use the INITIALIZE command with a term cursor at an empty condition sequence slot to initialize the slot with a condition term. The condition term is much like the term for variables; it has a single text slot, and otherwise no other display characters. Use OPEN-SEQ-TO-LEFT or OPEN-SEQ-TO-RIGHT to add additional slots for conditions terms.

To make a parameter into a meta-parameter, position a text cursor in the parameter's text slot and use the CYCLE-META-STATUS. If the parameter is already meta, using this twice will cycle its status back to being a normal parameter  . Note that this is not necessary with level-expression parameters. All level-expression variables are treated as meta.

Second order variable instances are entered on the left and right hand sides of the definition using the variable x:v (;;) term where x is the variable's name, and n > 0. The library display form object defining the display form for variable x:v (;;) is named so_varn so this family of names can be used to reference them. Note that abstraction objects are the only places where these second-order variable instances are used. When writing propositions, second-order variable instances are simulated  using the so_apply(n)  abstraction.