MetaPRL Refiner

The MetaPRL refiner uses the term rewriter to implement four kinds of formal objects:

  1. Computational rewrites,
  2. Conditional rewrites,
  3. Axioms: true statements in a logic,
  4. Inference rules: relations between the provable statements.

Computational Rewrites

Computational rewrites represent equivalences between terms that hold in any context. For example, in our currently implemented logics, beta-equivalence holds in every context:

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

This rewrite may not hold in logics that formalize computational complexity, or in logics that allow effects or require an explicit evaluation order.

Conditional Rewrites

Conditional rewrites are defined specifically for sequent calculi. An example of a conditional rewrite is a rewrite for division:

rewrite one : ('x <> 0) --> ('x / 'x) --> 1

The application of this rewrite requires a proof that the term being divided is not zero.

Axioms

Axioms are a degenerate form of inference rules that represent true statements of a logic. An axiom is usually just a term that represents a valid proposition. For instance:

rule true_ax : true
rule identity_ax : int -> int

The second axiom states that the proposition int -> int is true. This would be a valid axioms in the propositions-as-types interpretation: it would be proved by any function over the integers.

Inference Rules

Inference rules are used to specify "conditional" axioms. Most logical statements have the form of a rule. An example in a sequent calculus is the rule for implication introduction:

rule imp_intro 'H 'x :
    sequent { 'H; x: 'A >- 'B } -->
    sequent { 'H >- 'A => 'B }

This is the standard rule: the proposition 'A implies the proposition 'B if 'B can be proved by assuming 'A. The arguments 'H and 'x represent parameters of the rewrite. Given a goal term matching sequent { 'H >- 'A => 'B }, the application of the imp_intro rule produces a subgoal of the form sequent { 'H; x: 'A >- 'B }. The parameters 'H and 'x are necessary arguments to enable the application: 'H represents the list of hypotheses of the sequent, and the 'x parameter provides the new variable name used in the subgoal.

Refiner types

Refiners are constructed recursively as objects of type refiner. The null_refiner value is the empty refiner containing no rewrites, and no rules. The following types are related to the refiner:

type rewrite
type tactic
type sentinal
type extract

The rewrite type is used to represent both simple and conditional rewrites. The tactic type is used to represent axioms and inference rules. The extract type is used to provide accounting information for applications of rules. The sentinal type is a condensed representation of the refiner that includes the collection of all valid rewrites and rules in the refiner.

The objects in the refiner are constructed through four functions, one for each object type. These functions have the following types:

val create_rewrite : refiner -> rewrite args -> rewrite
val create_cond_rewrite : refiner -> cond rewrite args -> rewrite
val create_axiom : refiner -> axiom args -> tactic
val create_rule : refiner -> rule args -> tactic

Several operations are defined on rewrites:

val rwaddr : rewrite -> address -> rewrite
val andthenrw : rewrite -> rewrite -> rewrite
val orelserw : rewrite -> rewrite -> rewrite
val rwhigher : rewrite -> rewrite
val rwtactic : rewrite -> tactic

The rwaddr function applies the rewrite to a subterm of the goal. The andthenrw provides sequencing: when the rewrite (andthenrw rw1 rw2)is applied, the rewrite rw1 is first applied, and it is immediately followed by applying the rewrite rw2. The orelserw is similar for handling failures. When the rewrite (orelserw rw1 rw2) is applied, the rewrite rw1 is applied to the goal. If rw1 succeeds, the rewrite completes without applying rw2. Otherwise, if rw1 fails (by raising a RefineError exception), the rewrite is restarted by applying rw2. When the (rwhigher rw) rewrite is applied, the rewrite rw is allied to all the outermost subterms of the goal where rw may be applied successfully (without raising a RefineError exception). Finally he rwtactic function converts a rewrite to a tactic, so that the tactic mechanism can be used to apply the rewrite.

Tactics are applied with the refine function, with this simplified type:

val refine : sentinal -> tactic -> term -> term list * extract

The refine function takes a sentinal that is used to check that the tactic performs a valid logical inference; it takes a tactic that describes the logical operation to be performed, and it produces a list of subgoals that results from the application of the rewrites and inference rules defined by the tactic. A successful refinement also returns an extract that summarizes the logical operation. In constructive logics, the extract may be used to compute the computational content of a proof. The extract is also used to construct proof trees with the function compose:

val compose : extract -> extract list -> extract

If extract1 is the extract of a refinement, and extracts2 is a list of extracts for refinements of each of the subgoals, then (compose extract1 extracts2) is a valid extract for the composed proof. As defined, extracts always represent valid proofs. However, for untrusted distributed refinement, or for proof-carrying code, a checker is implemented as the function:

val term_of_extract : extract -> term

The term_of_extract function checks that the extract is valid, and it also produces the computational contents for constructive proofs.

The final important operation of the refiner is the sentinal computation. A sentinal is essentially a summary of all the formal objects in a refiner. The sentinal is used during refinement to check for valid applications of rules and rewrites. The function sentinal_of_refiner computes the summary for a refiner.

val sentinal_of_refiner : refiner -> sentinal