Jason Hickey, Aleksey Nogin
MetaPRL System Description
MetaPRL
is implemented as an extended OCaml compiler. Modules in MetaPRL
can be plain programs, or they can be extended to additional logical
definitions and syntax. The architecture of the system is summarized
in the diagram at the right. The complete system contains these
parts:
- The refiner implements
logical operations and accounting. The refiner associates an
accounting object called a sentinal with each module.
The sentinal defines the valid set of logical inferences, syntax
definitions, computational equivalences, and programs in a module.
The sentinal is passed between refiners during distributed computation
to localize the context of a refinement.
- The module compiler is
used to compile MetaPRL modules into two parts: an ML module
that defines the computation in the module, and a sentinal that
expresses the logical content. The module compiler is right above
the refiner; it has no knowledge of proofs, whether they be automated
or interactive. The compiler simply compiles logical content,
to be used later by the module editor.
- The refiner defines an abstract logical interface. The distributed prover implements
the same interface, but the logical operations are spread across
multiple machines. The distributed prover contains a scheduler
to hand out logical goals, and a failure recovery algorithm to
handle refiner failures.
- The forward chainer
implements proof caching and forward chaining. Currently, forward
chaining is restricted to forward rules with a finite forward
closure. Once again, the forward chainer reimplements the refiner
interface.
- The tactic definitions
implement the tactic combinator language over the refiner. Logical
proofs use basic combinators: each logical definition in a module
defines a tactic, and the tactic module provide tactic combinators
that are used for automation.
- The OCaml syntax is defined
as a logical module containing syntax definitions and an operational
semantics for the OCaml definitions in a module. The module
compiler compiles ML programs to logical terms; the OCaml
syntax module defines the logical properties and semantics of
the programs.
- The logic definition module
defines properties shared by many logics. For example, the MetaPRL
framework has no knowledge of sequents, but many logics use sequents
to express their inference rules. The basic logic module defines
sequents. In addition, the basic logic module defines tactics
for automation, including automation of introduction and elimination
rules, equality reasoning, and general tactic-based search.
- The logics currently defined include the
Nuprl type theory,
Aczel's set theory, first order logic, and a partial implementation
of the Edinburgh logical framework (LF).
- The module editor
provides interactive support, including a module navigator, a
proof editor, and context-sensitive toploop language.