MetaPRL Inference Rules

Introduction

The MetaPRL meta-logic defines a higher order logic of Horn formulas. The logic includes a term language, described in the page on MetaPRL terms, and a meta-logic defined with a meta-implication over second-order term patterns. Each inference rule in a theory defines a set of valid inferences in the logic. At the moment, inferences are non-recursive: they have the syntax:

inference ::= term | term --> inference

A theory is defined by stating its inference rules. Some times we call an inference rule that is just a single term an axiom (axioms don't use the meta-implication). The theories are modular: each module defines a theory that contains the rules defined in the module, and in all ancestor modules. The module system is discussed in the module system page.

Interface

A module interface declares the signature of a theory; it includes declarations for each of the public inference rules. Rules are not required to be listed in an interface, but for clarity, many of the theories in MetaPRL, including Itt_theory, include the inference rule declarations in their signatures.

Inference rules are declared with the rule form. The general syntax is the following:

rule name [params] : inference

The params are extra parameters that are passed to the inference rule, including context addresses, term arguments, and new variable names. The Itt_struct module contains a basic rule:

rule hypothesis 'H 'J 'x :
   sequent ['ext] { 'H; x: 'A; 'J['x] >- 'A }

The name of the rule is hypothesis. The parameters include two context identifiers 'H and 'J, and a variable identifier 'x. The inference of this rule defines a set of sequents, containing a number of hypotheses defined by the context 'H, a single hypothesis x of type 'A, additional hypotheses defined by the context 'J['x], where the variable x may occur free, and a single conclusion 'A. The sequent also contains an extra parameter 'ext that defines the computational status in the Itt_theory. The parameter is the term squash if the sequent has no computational value, and it is a variable otherwise (in this case the variable 'ext).

The hypothesis rule defines a set of valid inferences defined by the terms that is matches. Put another way, the inference states that all substitution instances are valid formulas, where the contexts 'H and 'J['x] are replaced by lists of hypotheses, the variable 'A is replaced by a term, the variable 'x is replaced by another variable and the variable 'ext is replaced by arbitrary term. For instance, the following formulas are valid in the Itt_struct module:

sequent ['ext] { i: int; z: false >- false }
sequent [squash] { z: 1; y: 'z + 1 >- 1 }

The second example is strange because 1 is not a type. However, the semantics of sequents in the Itt_theory theory validates the truth of the expression. A hypothesis (x:'A) in the Itt theory implies two assumptions: that 'A is a type, and that 'A is true. If 'A is not a type, the assumption is false, so the sequent is trivially true.

Inference rules are also defined using the rule directive. An inference is a conditional rule; it states assumptions that must be proved in order for the conclusion to hold. Most introduction and elimination rules have this form. For example, in the Itt_logic module, the introduction rule for logical conjunction is stated as follows:

rule and_intro 'H :
   sequent ['ext] { 'H >- 'a1 } -->
   sequent ['ext] { 'H >- 'a2 } -->
   sequent ['ext] { 'H >- "and"{'a1; 'a2} }

The 'H is the context identifier used to instantiate the hypotheses, and the 'a1 and 'a2 terms are the subterms of the conjunction. The rule states that in order to prove the conjunction 'a1 & 'a2 in any context 'H, it is sufficient to prove 'a1 and 'a2 in the same context.

The metaprl/doc/private/sequents.tex file gives the formal definition of the complete rule syntax.

Implementation

Inference rules are implemented two ways: they can be derived from previous rules and they can be declared as primitive axioms of a theory. The difference between these two forms is in the way the system does logical accounting.

A primitive inference is "justified" by giving a relation on proofs with the prim form, which has the following syntax:

prim name [params] : binference = term

A binference is like an inference, but it contains bindings for the proofs. The bindings are bound in the term part of the prim form, which provides the final proof term. In constructive theories, the "proof" is usually the proof extract: a term that defines the computational content of the proof. For example, the following definition gives an implementation of the and_intro rule declared above:

prim and_intro 'H :
   ('t1 : sequent ['ext] { 'H >- 'a1 }) -->
   ('t2 : sequent ['ext] { 'H >- 'a2 }) -->
   sequent ['ext] { 'H >- "and"{'a1; 'a2} } =
   pair{'t1; 't2}

The pair term is the proof term of the proof: if 't1 is a proof of 'a1, and 't2 is a proof of 'a2, then pair{'t1; 't2} is a proof of 'a1 & 'a2. The proof term is especially useful in constructive theories; in classical theories the proof term may just be a canonical proof term, indicating the truth of the proof statement without any computational value.

The system automatically constructs proof terms for complete proofs, using the constructions provided by the prim form in the theory. Inferences can also be derived from previous rules in a theory. Derived rules are declared with the following form:

interactive name : [params] : inference

The interactive form has exactly the same form as an rule, and it introduces a proof obligation. The proof is constructed with the proof editor.

Tactics

When an rule is declared, the system creates a tactic that can be used to apply the rule. Tactics are the general reasoning mechanism used for interactive proving. Tactics are ML programs, and they can be combined with the tacticals in the system description to provide automated proving.

Each inference rule declaration also provides a tactic declaration. The exact form of the tactic depends on the types of its parameters. A context parameter requires an address argument, a variable parameter requires a string, and a term argument requires a term. For instance, the ML definitions provided by the rules above are the following:

val hypothesis : address -> address -> string -> tactic
val and_intro : address -> tactic
  

For more informations about MetaPRL tactics refer to