MetaPRL Module System

Logics are defined in MetaPRL as modules. Logic modules can be expressed as extensions of previous modules, forming an object-oriented logical contruction, and logics can be related using the module system.

Each logical module defines syntax, display, computational rewriting, and logical inference, defined in the previous pages. Logics are extended and related with the include directive, discussed here. The include directive is the logical equivalent of the open directive in OCaml. The include directive "opens" the logical namespace, and it establishes a logical dependence between modules. The general form form of the include directive is as follows:

include module-path

Multiple include directives may appear in interfaces and implementations, establishing multiple dependencies that establish a logical inheritance graph. For example, the following module uses the basic logical definitions, and reasoning about numbers to express a well-known problem in number theory:

include Itt_logic
include Itt_int

interactive fermat 'H : :
    sequent ['ext] { 'H >- 
       all i: nat. (i >= 3) =>
          not (exst a: nat. exst b: nat. exst c: nat.
             power{a; i} + power{b; i} = power{c; i} in nat)

The included modules Itt_logic and Itt_int provide the logical context. Itt_logic provides logical defiitions for all and exst, implication, and the Itt_int modules provides reasoning about numbers. These modules have include directives of their own. The Itt_logic module contains the following logical dependencies:

include Itt_equal
include Itt_rfun
include Itt_dfun
include Itt_fun
include Itt_dprod
include Itt_prod
include Itt_union
include Itt_void
include Itt_unit
include Itt_struct

Each of the modules used in Itt_logic are recursively included in the Fermat theory. In general, an include recursively opens all ancestors of the module included.

The include directive performs the following operations for each included module:

• All syntax declarations defined with declare are inherited.
• All display forms are inherited.
• All computational rewrites, axioms, and inference rules are inherited.

The include does not open the ML namespace. That operation must be performed separately for ML content, including tactics and conversions.

Naming conflicts

Modules may define operators with the same name. For example, two theories (say A and B) may both declare a conjunction

declare "and"{'a; 'b}

and they may impose different logical interpretations of the "and" term. The general rule for solving conflicts is the following:

• unqualified operator names refer to the most recent theory that defines the operator,
• operators names can be qualified to refer to other definitions.

A logic that relates the theories A and B must refer to both terms. Qualified names are expressed by module paths composed with the ! symbol. Here is an example, showing an interpretation of A.and as the "conditional" form of B.and. (The "and" operator is quoted because it is an ML keyword.)

include A
include B

rewrite a_and_interp : (A!"and"{'a; 'b}) <--> (B!"and"{'a; B!implies{'a; 'b}})