Matching and Substitution

Nuprl has complex matching routines, which allow for automatic instantiation  of universal formulae in a variety of cases. Given a pattern term P and instance term I, we say that I matches P,  if there exists a substitution   such that . For many purposes, R is equality, but on some occasions it is useful to use a slightly weaker R. The weaker R allows level expressions in I and to be related by an order relation rather than an equivalence relation. The weaker R also can allow I and to differ by the folding or unfolding of soft abstractions.

Since matching is all about guessing substitutions, we describe first the possible kinds of substitution.

1. First Order Term
   We replace a variable term free in P by some other term. For example, if P = x + y and , then I = 3 + y. We call such substitution first order  because in , each variable is bound to a first-order term rather than a higher-order term. (See next item).

2. Second Order Term
   Second-order terms  are a generalization of terms. They can be thought of as `terms with holes', terms with zero or more subtrees missing. A second-order term can be represented as a pair of a variable list and a first-order term, the first-order term being generated from the second-order term by filling the holes with variables from the variable list. Naturally the hole-filling variables need to be distinct from any other variables in the term to avoid confusion. We will write a second-order term as .

   A second-order variable instance  has form , where v is the variable itself, and are its arguments. A second-order substitution  is a list of second-order bindings , pairs of second-order variables and the second-order terms they are bound to. 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.

   Second order substitution is useful for instantiating pattern terms involving binding structure. For example the second-order substitution applied to the pattern yields the instance .

3. Parameter
   Nuprl terms can be parameterized by families of objects such as natural numbers and tokens. When defining abstractions using such parameters, one replaces an instance of a parameter by a parameter variable. Such parameter variables are replaced by parameter constants using parameter substitution.

4. Level Expression
   Level expression substitution involves replacing level expression  variables within level expression parameters by other level expressions.

5. Bound Variable
   Such substitutions are useful for alpha-conversion  of terms.

Matching involves recursively comparing the structure of an instance term 

against that of a pattern term  . For a match to possibly succeed, the structures must only disagree at positions where there is some kind of variable in the pattern. Each disagreement must generate or confirm a binding for that variable.

The kinds of matches of instance parts to some sort of variable are:

1. Term to First-Order Variable Term
   For example, the instance 2 + 2 matches the pattern x + x giving the first-order term binding . In general, since instance terms also contain variable terms, the match routine distinguishes between variable terms in the pattern which can and cannot take part in matching. The variable terms which do take part are called meta-variables. In the example above, the variable x is considered a meta-variable. If a meta-variable  occurs more than once, then all matches for it must be alpha-equal.

2. Term to Second-Order Variable Term
   In addition to making distinction between meta and non-meta variable terms, the match routines distinguishes between active second-order  variables and passive second-order variables . Active second-order variables generate bindings. Passive second-order variables are used to confirm matches generated by other active second-order variables.

   For example, with P a second-order meta-variable, the instance matches the pattern , giving the second-order term binding .

3. Parameter Constant to Parameter Variable
   For example, the instance term apple{cox:tok} matches the pattern term apple{$x:tok} giving the parameter binding $x cox.

4. Bound Variable to Bound Variable
   For example, the instance term matches the pattern term , giving the bound variable binding .

5. Level Expression to Level Expression
   This kind of matching is rather complex, since we sometimes desire that the pattern, when instantiated with the result of the match, be related to the instance by an order relation rather than an equality. For example, the instance might match the the pattern giving a level expression substitution of . The directions of the inequalities between level expressions in the instance and instantiated pattern are dependent on the position of the level expressions in the terms. They are usually chosen such that there is a certain inclusion relation between the instance and the instantiated pattern when each is considered as a type.

Second-order variable instances cannot appear in Nuprl sequents, nor can second-order terms. Instead, we simulate them using respectively application, and lambda abstraction. Specifically, we define families of abstract terms with so_apply  and so_lambda . (We need families to cope with the different possible arities.)

Often, when we match against the consequent of a lemma, we cannot obtain all the bindings to instantiate the lemma directly from the match. In these cases, we try to extend the match by inferring types  of right-hand sides of existing bindings, and matching those inferred types against the type declarations  in the lemma of the left-hand-sides of the bindings. For example, the typing lemma for the length function is:

Consider the goal . A match of the concl of this goal against the consequent of the pattern gives the binding , but doesn't give a binding for A. However, we can get the binding by matching the inferred type of which is , against the declaration type of l, which is . Similarly, by inferring the universe which inhabits, we can get a binding for the universe level i.

For convenience, we inject the different kinds of bindings into the single type var # term. A pair of this type is interpreted according to the first entry in the following table which it matches. (Equating ML objects of type var and the objects of type tok they are isomorphic to.)

Most tactics which do matching, take an optional sub argument which can be used to provide bindings which the match fails to find, or to override matches which are found.