MetaPRL Conversionals

The word "conversion" is used to describe rewriting rules. Like a "tactical," a "conversional" is an operation on conversions. A conversion is created in a module whenever a rewrite rule is defined. For example, the following definition of beta reduction defines a conversion called beta:

rewrite beta : (lambda{x. 'b['x]} 'a) <--> 'b['a].

The ML conversion has the following type:

val beta : conv

Conversion application

A conversion is applied to the current goal by using the rw function:

topval rw : conv -> int -> tactic

The rw function assumes the conversion is being applied in a sequent calculus, and the number passed to the rw function is the number of the sequent clause to be rewritten. There is an additional function rwh to perform rewriting on the "higher" occurrences of subterms.

topval rwh : conv -> int -> tactic

For example, beta conversion is performed in the following proof fragment:

Goal: sequent { 'H; x: (lambda{x. 'x} 1) < 0) >- false }
BY rwh beta 2
Subgoal 1: sequent { 'H; x: 1 < 0 >- false }

Simple conversions

There are several simple conversions:

topval idC : conv
topval failC : conv

The idC conversion is the identity: when idC is applied to a term, the result of the rewriting is the argument, unchanged. The failC conversion always fails.

Simple conversionals

There are several standard conversionals:

topval prefix_thenC : conv -> conv -> conv
topval prefix_orelseC : conv -> conv -> conv
topval addrC : int list -> conv -> conv
topval foldC : term -> conv -> conv
topval makeFoldC : term -> conv -> conv
topval cutC : term -> conv
val funC : (env -> conv) -> conv

The thenC conversional is for sequencing: the conversion (rw1 thenC rw2) applies rewrite rw1 and follows it by applying rw2 to the resulting term. The orelseC is for conditional application: the conversion (rw1 orelseC rw2) first tries applying the conversion rw1. If the rewrite succeeds, rw2 is not applied. Otherwise, rw2 is applied to the initial argument.

The conversion addrC applies a rewrite to a subterm of the goal. The foldC conversion is for reversing a rewrite. For example, the following proof fragment reverses a beta reduction:

Goal: sequent { 'H; x: 1 < 0 >- false }
BY rwh (foldC << lambda{x. 'x} 1 >> beta) 2
Subgoal: sequent { 'H; x: (lambda{x. 'x} 1) < 0 >- false }

The makeFoldC conversional performs the same operation as foldC, but it performs a (relatively expensive) preprocessing step. The makeFoldC conversional is typically used at the top level of a module to define standard reversed rewriting.

The cutC conversion replaces the current goal with a new goal, producing a rewriting subgoal. The following proof fragment illustrates its use:

Goal: sequent { 'H >- ('x + 1) - 1 }
BY rw (cutC << 'x >>) 0
Subgoal 1: sequent { 'H >- 'x }
Subgoal 2: sequent { 'H >- 'x <--> ('x + 1) - 1 }

The funC conversional produces an environment for a conversion. The current goal can be accessed with the following functions:

val env_term : env -> term
val env_goal : env -> term

The env_term function returns the term that the rewriting is to be performed on, and the env_goal returns the entire goal (so, for instance, the results will be different if rewriting is being performed on a subterm of the goal with addrC).

Search conversionals

Typically, rewriting is performed by search. For example, it is often useful to reduce all beta redices in the goal. The following conversionals provide search strategies.

topval someSubC : conv -> conv
topval allSubC : conv -> conv

These two conversions apply their arguments to the immediate subterms of the current goal. The (someSubC conv) conversion applies conv to subterms from left-to-right, succeeding when the first rewrite succeeds. The (allSubC conv) applies conv to all subgoals; all rewrites must succeed.

topval higherC : conv -> conv
topval lowerC : conv -> conv

The higherC conversion searches for the outermost terms where a rewrite is successful. It may defined by recursion:

let higherC conv = conv orelseC (allSubC (higherC conv))

Since higherC conversional is used very often, MetaPRL provides a highly tuned efficient implementation of rewriting using higherC conversionals

The lowerC conversion searches for the innermost terms:

let lowerC conv = (allSubC (lowerC conv)) orelseC conv

The repeatC conversion applies a conversion until a fixpoint is reached:

topval repeatC : conv -> conv