Next: Nuprl Conversions Up: Rewriting Previous: Concise Rewriting Tactics

## Introduction to Conversions

This section presents a simplified implementation of conversions and conversionals  to convey the general ideas. Later sections describe the actual conversions that are implemented. Note however that the conversionals introduced here have the same names and same behaviours as those in the actual system.

Let convn be an ML concrete type alias for the type of conversions. In this section, assume that convn is an alias for the type term -> term, where term is a type of terms that we want to rewrite. Later on, I describe the type that convn is actually an alias for. If c is of type convn, then we can use c to rewrite t of type term by simply running the ML evaluator on the application .

For the purposes of the section only, let me introduce a basic conversion called RuleC : term -> convn. The conversion RuleC   expects its term argument to be of form a = b where the free variables of b are a subset of those in a. If the conversion RuleC 'a = b' is applied to a term t, RuleC tries to find a substitution such that . If it succeeds, it returns the term . If a substitution cannot be found, RuleC raises an exception  . The conversion RuleC 'a = b' therefore rewrites instances of a to corresponding instances of b. For example:

RuleC 'x + 0 = x'

when applied to the term yields the term .

RuleC cannot by itself rewrite subterms of a term; if

RuleC 'x + 0 = x' is applied to the term , it fails. There are a variety of higher-order conversions that map a conversion such as RuleC over all subterms of a term. An example of a conversional is SweepUpC : convn -> convn . If c is a conversion, then SweepUpC c is also a conversion. if

SweepUpC c is applied to some term t, an attempt is made to apply c once to each subterm of t working from the leaves of term t up to its root. SweepUpC c only fails every every application of c fails. So if

SweepUpC  (RuleC 'x + 0 = x')

is applied to term , it succeeds and returns the term .

The basic conversion for sequencing conversions is ANDTHENC  : convn -> convn -> convn. In , we reserve all-capital names for infix functions so a normal application of ANDTHENC to conversions and has form ANDTHENC . When applied to a term t, ANDTHENC first applies to t. If succeeds, returning a term , then is applied to and the result is returned. If either or fails, then

ANDTHENC also fails. By analogy with tacticals being higher-order tactics, ANDTHENC is called a conversional.

The ORELSEC  : convn -> convn -> convn conversional is for combining alternative conversions. When ORELSEC is applied to a term t, it first tries applying to t, and if this succeeds returns the result. If the application of fails, then it tries applying to t, failing if fails.

The definition for SweepUpC is:

SubC  : convn -> convn when applied to a conversion c and a term t, applies c to each of the immediate subterms of t. It fails only when c fails on every immediate subterm  . Hence, it always fails when t is a leaf node and has no immediate subterms. ORTHENC is similar to ANDTHENC in that it first tries and then . However ORTHENC only fails if both and fail. So, a call of SweepUpC c on argument t first tries to apply SweepUpC c to the immediate subterms of t and then then tries to apply c to t itself. Note that without the t argument on the left and right sides of the definition, SweepUpC in ML's call-by-value evaluation scheme would recurse indefinitely.

The definition for ORTHENC is:

let c1 ORTHENC c2 = (c1 ANDTHENC TryC c2) ORELSEC c2   where TryC c is defined as c ORELSE IdC and IdC: convn, when applied to any t, always returns t.

Other conversionals that are commonly used in the work described in this thesis are:

• FirstC : convn list -> convn   which is an n-ary version of ORELSEC,
• RepeatC : convn -> convn   which repeatedly tries applying a conversion till no further progress is made,
• HigherC : convn -> convn   which applies a conversion to only nodes higher in a term tree. What I mean by `higher' is probably best understood by studying the definition of HigherC:

• SweepDnC : convn -> convn   which sweeps a conversion down over a term tree from the root towards the leaves. Its definition is:

• NthC int -> convn -> convn.   NthC tries c on each node in t in pre-order order, but only on the ith success of c does it go through with the rewrite that c suggests. This is very useful during interactive proof when for example you want to unfold one instance of a definition but not any others.

Next: Nuprl Conversions Up: Rewriting Previous: Concise Rewriting Tactics

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