Specification logic

The specification logic is a fragment of λProlog in which the object system is described. A specification consists of a signature and a set of clauses, stored in a .sig file and a .mod file.

Specifications are executable: asking whether an atomic formula is provable corresponds to searching for a derivation using the clauses. The reasoning logic in a .thm file can refer to this notion of provability with the {...} notation, and proofs in the reasoning logic can analyze the possible derivations.

Signatures

A signature names the atomic types and constants of the specification.

eval.sig

sig eval.

kind    tm, ty                 type.

type    app                    tm -> tm -> tm.
type    abs                    (tm -> tm) -> tm.

type    arrow                  ty -> ty -> ty.

type    of                     tm -> ty -> o.
type    eval, step, nstep      tm -> tm -> o.

The declaration sig name. must match the base name of the file. The declarations are:

• kind A, B type. introduces atomic types.
• kind F type -> type. introduces a type constructor.
• type c T. introduces the constant c with type T. Several constants may share a declaration: type f, g T.

The italic letters stand for names supplied by the user, not for literal identifiers. Replace them with lowercase names: an identifier that begins with a capital letter is a variable, so using one here would change the meaning of the declaration. Do not literally use an identifier beginning with a capital letter except for type and term variables.

A constant whose target type is o is a predicate. The predicates are the atomic formulas that the clauses of the module can prove. Here of, eval, step, and nstep are predicates.

Clauses

A module gives clauses for the predicates declared in the signature.

eval.mod

module eval.

of (abs R) (arrow T U) :- pi x\ (of x T => of (R x) U).
of (app M N) T :- of M (arrow U T), of N U.

eval (abs R) (abs R).
eval (app M N) V :- eval M (abs R), eval (R N) V.

step (app (abs R) M) (R M).
step (app M N) (app M' N) :- step M M'.

nstep A A.
nstep A C :- step A B, nstep B C.

A clause is a head followed by an optional body:

head.
head :- body.
head <= body.

The body is a comma-separated sequence of formulas. The comma has the same meaning as the conjunction of goals in Prolog: to prove the head, prove each goal in order. The variant :- and <= are synonymous; both are accepted.

A module begins with module name. and may end with end. or just end at the end of the file.

Clause names

A clause may be preceded by a name annotation of the form %:name:. abella_doc uses these names in its output, and errors can refer to them:

%:abs-typing:
of (abs R) (arrow T U) :- pi x\ (of x T => of (R x) U).

The annotation has no effect on proof search.

Generic and hypothetical judgments

The specification logic has two higher-order features that make it suitable for metatheory.

Generic judgments

pi x\ G introduces a fresh, unknown constant x and then proves G. The constant is distinct from every other constant and cannot be captured by substitution. This is how specifications introduce a variable whose identity does not matter:

of (abs R) (arrow T U) :- pi x\ (of x T => of (R x) U).

The clause says that abs R has type arrow T U if, for a fresh x with type T, the term R x has type U. The name x is bound in the body and is not visible outside it.

pi is the specification-level counterpart of the reasoning-level forall. Unlike forall, it produces a constant rather than an arbitrary term, which is what makes the clause executable.

Hypothetical judgments

H => G adds H to the local context and proves G. Assumptions introduced this way are used by backchaining: when a goal is atomic, the prover may use a clause from the context in addition to the clauses of the module.

of (abs R) (arrow T U) :- pi x\ (of x T => of (R x) U).

The of x T => of (R x) U part makes the typing assumption for x available while proving that R x has type U. The assumption is scoped to the body of the clause and disappears when the clause is finished.

Modularity

A specification may be assembled from several files.

accum_sig includes the declarations of another signature:

eval.sig

sig eval.

accum_sig terms.

type eval tm -> tm -> o.

accumulate includes the clauses of another module:

eval.mod

module eval.

accumulate terms.

eval zero zero.

The two are linked: if a module accumulates another module, its signature must accum_sig the other module's signature. This guarantees that all constants used by the accumulated clauses are declared. The relation is transitive, and cyclic dependencies are rejected.

Typing restrictions

Specification logic types obey the following restrictions:

• olist and prop may not be mentioned in a specification type;
• quantification over type o is not allowed.

A signature or clause may contain free type variables, in which case it is schematic; see Schematic polymorphism.

The type olist is an abbreviation for list o. The list type constructor and the constants nil and :: are built in. The constants pi, =>, and & are also built in and cannot be redefined by a specification.

Type annotations may be needed when inference is ambiguous. A variable is annotated with x:T. An abstraction may annotate its bound variable:

pi (x : tm)\ of x T => of (R x) U

The same annotation syntax applies in reasoning-level formulas.

Provability in the reasoning logic

Inside a .thm file, the formula {G} means that the atomic specification formula G is provable from the current specification:

{eval (app (abs R) M) V}

The full form names the context of assumptions explicitly:

{L |- G}

Here L is a list of formulas of type o, and G is one formula of type o. The judgment holds when G is derivable from the clauses of the module together with the assumptions in L. The empty context may be omitted, so {G} abbreviates {nil |- G}.

When a derivation backchains on an assumption in the context rather than on a module clause, the judgment records which assumption was used:

{L, [F] |- G}

This says that G is derived by backchaining on the assumption F in L. The [F] notation is what makes it possible to reason about proofs that use an assumption directly. A typical proof step is to use a lemma to discover the shape of F, since F is usually a variable at that point.

The three forms are related:

• {G} is provability from the module alone;
• {L |- G} is provability from the module and the assumptions L;
• {L, [F] |- G} is provability from the module and L using F as the clause for the last backchaining step.

Reasoning about derivations

The specification logic is designed so that its proofs can be analyzed structurally. Case analysis on {L |- G} considers:

1. the module clause whose head matches G;
2. a generic or hypothetical rule, if the clause ends in pi or =>;
3. a backchaining step on an assumption in L.

This is why the tactics case, apply, inst, cut, and monotone are enough to carry out most metatheoretic proofs. See Tactics reference and Reasoning logic.

Example: evaluation and typing

The lambda-calculus development used in the walkthrough is the standard example. Its signature declares terms, types, and the judgments eval and of; its module gives the clauses shown above. The subject reduction theorem then reasons about the derivations of {eval E V} and {of E T}.

A larger specification may add base types and constants:

kind tm, ty type.
type i ty.
type arrow ty -> ty -> ty.

Here i is a base type and arrow builds function types. No constants of type tm need to be declared for variables, because variables are introduced by pi in the clauses that need them.