A Modular Hierarchy of Logical Frameworks

Robin Adams

University of Manchester

                         robin.adams@ma.man.ac.uk

Abstract. We present a method for defining logical frameworks as a collection of features which are defined and behave independently of one another. Each feature is a set of grammar clauses and rules of deduction such that the result of adding the feature to a framework is a conservative extension of the framework itself. We show how several existing logical frameworks can be so built, and how several much weaker frameworks defined in this manner are adequate for expressing a wide variety of object logics.

1 Introduction

Logical frameworks were invented because there were a large number of differing systems of logic, with no common language or environment for their investigation and implementation. However, we now find ourselves in the same situation with the frameworks themselves. There are many systems that are used as logical frameworks, and it is often difficult to compare them or share results between them. It is often much work to discover whether two frameworks can express the same class of object logics, or whether one is stronger or weaker than the other. If we are interested in metavariables, and we compare Pientka and Pfenning’s work [1] with Jojgov’s [2], it is difficult to see which differences are due to the different handling of metavariables, and which are due to differences in the underlying logical framework.

To redress this situation somewhat, I humbly present the first steps towards a common scheme within which a surprising number of different frameworks can be fitted. We take a modular approach to the design of logical frameworks, defining a framework by specifying a set of features, each of which is defined and behaves independently of the others. Together, all the frameworks that can be built from a given set of features form a modular hierarchy of logical frameworks.

We may give an informal definition of a feature thus:

A feature F is a set of grammar clauses and rules of deduction such that, for any logical framework L, the result of adding F to L is a conservative extension of L.

(This cannot be made a formal definition, as we do not (yet) have a notion of “any logical framework”.)

It is not surprising that features exist — one would expect, for example, that adding a definitional mechanism to a typing system should yield a conservative extension. Perhaps more surprising is the fact that such things as lambdaabstraction can be regarded as features. In fact, we shall show how a logical framework can be regarded as being nothing but a set of features. More precisely, we shall define a system that we call the basic framework BF, and a number of features that can be added to it, and we shall show how a number of existing frameworks can be built by selecting the appropriate features.

We shall also show that most of these features are unnecessary from the theoretical point of view — that is, a much smaller set of features suffices to express a wide variety of object logics. These ‘unnecessary’ features may well be desirable for implementation, of course.

It may be asked why we insist that our features always yield conservative extensions. This would seem to be severely limiting; in one’s experience with typing systems, rarely are extensions conservative. For typing systems in general, this is true. But I would argue that logical frameworks are an exception. The fact that all the features presented here yield conservative extensions is evidence to this effect. And it would seem to be desirable when working with a logical framework — if we add a feature to widen the class of object logics expressible, for example, we still want the old object logics to behave as they did before.

We suggest that, if this work were taken further, it would be possible and desirable to define mechanisms such as metavariables or subtyping as features, and investigate their properties separately from one another and from any specific framework. If we did this for metavariables, for example, we would then know immediately what the properties of ELF with metavariables were, or Martin-Löf’s Theory of Types with metavariables, or …

2 Logical Frameworks

Let us begin by being more precise as to what we mean by a logical framework.

Broadly speaking, logical frameworks can be used in two distinct ways. The first is to define an object logic by means of a signature, a series of declarations of constants, equations, etc. The typable terms under that signature should then correspond to the terms, derivations, etc. of the object logic, using contexts to keep track of free variables and undischarged hypotheses. Examples include the Edinburgh Logical Framework [3] and Martin-Löf’s Theory of Types [4]. We shall call a framework used in this way a logic-modelling framework.

The second is to use the logical framework as a book-writing system, as exemplified by the AUTOMATH family of systems [5]. The most important judgement form in such a framework is that which declares a book correct; the other judgement forms are only needed as auxiliaries for deriving this first form of judgement.

These two kinds of system behave in very similar ways. Any system of one kind can be used as a system of the other, by simply reading ‘signature’ for ‘book’, or vice versa. This is a striking fact, considering the difference in use. In a system of the first kind, deriving that a signature is valid is just the first step in using an object logic; in a book-writing system, it is the only judgement form of importance. We shall take advantage of this similarity. Our features shall be written with logic-modelling frameworks in mind; it shall turn out that they are equally useful for building book-writing frameworks.

We consider a logical framework to consist of:

1. Disjoint, countably infinite sets of variables and constants.

2. A number of syntactic classes of expressions, defined in a BNF-style grammar by a set of constructors, each of which forms a member of one class from members of other classes, possibly binding variables.

3. Three syntactic classes that are distinguished as being the classes of signature declarations, context declarations and judgement bodies. Each signature declaration is specified to be either a declaration of a particular constant, or of none. Similarly, each context declaration is specified to be either a declaration of a particular variable or of none. We now define a signature to be a finite sequence of signature declarations, such that no two declarations are of the same constant. The domain of the signature Σ, dom Σ, is then defined to be the sequence consisting of the constants declared in Σ, in order. Similarly, we define a context to be a finite sequence of context declarations, no two of the same variable, and we define its domain similarly. Finally, we define a judgement to be a string of one of two forms: either

Σ sig

or

Γ ⊢_{Σ} J

where Σ is a signature, Γ a context, and J a judgement body.

4. A set of defined operations and relations on terms. Typically, these shall include one or more relations of reducibility and convertibility.

5. The final component of a logical framework is a set of rules of deduction which define the set of derivable judgements.

2.1 The Basic Framework BF

As is to be expected, BF is a very simple system. It allows: the declaration of variable and constant types; the declaration of variables and constants of a previously declared type; and the assertion that a variable or constant has the type with which it was declared, or is itself a type.

The grammar of BF is as follows:

Term a ::= x | c
Kind A ::= Type | El(a)
Signature Declaration δ ::= c : A of c
Context Declaration γ ::= x : A of x
Judgement Body J ::= valid | A kind | a : A

The rules of deduction of BF are given in Figure 1.

⟨⟩ sig  {⊢_{Σ} A kind \atop Σ, c : A sig} (c ∉ dom Σ)
Σ sig ; ⊢_{Σ} valid

Γ ⊢_{Σ} A kind

Γ, x : A ⊢_{Σ} valid

(x ∉ dom Γ)

{Γ ⊢_{Σ} valid \atop Γ ⊢_{Σ} c : A} (c : A ∈ Σ) {Γ ⊢_{Σ} valid \atop Γ ⊢_{Σ} x : A} (x : A ∈ Γ)
Γ ⊢_{Σ} valid
Γ ⊢_{Σ} Type kind

Γ ⊢_{Σ} a : Type

Γ ⊢_{Σ} El(a) kind

Fig. 1. The basic framework BF

3 Features and the Modular Hierarchy

A feature that depends on the logical framework L consists of any number of new entities: new syntactic classes, new constructors, new defined operations and relations and new rules of deduction. The new constructors may take arguments from new classes or those of L, bind new variables or those of L, and return expressions in new classes or those of L. In particular, they may create new signature declarations, context declarations and judgement bodies. Likewise, the new defined operations and relations should be defined on both old and new expressions, and the new rules of deduction may use both old and new judgement forms.

A feature may also introduce redundancies. A redundancy takes an old constructor and declares that it is to be replaced by a certain expression. That is, the constructor is no longer part of the grammar; wherever it appeared in a defined operation or relation or a rule of deduction, its place is to be taken by the given expression.

Now, if L′ is any logical framework that extends L, we define the logical framework L′ + F in the obvious manner.

It should be noted that these rules of deduction are assumed to automatically extend themselves when future features are added. For example, if a feature contains the rule of deduction

{Γ ⊢_{Σ} M : A \atop Γ ⊢_{Σ} M = M : A}

and we later introduce a new constructor for terms M, this rule is assumed to hold for the new terms M as well as the old.

(Formally defining features in such a way that this is possible requires explicitly defining classes of meta-expressions in the manner of [6]. We shall not go into such details here.)

Finally, we define:

Definition 1. A feature F that depends on the set of features {F_{1}, F_{2}, …} is a feature that depends on the logical framework

BF + F_{1} + F_{2} + · · · .

Thus, if F depends on {F_{1}, F_{2}, …}, we can add F to any framework in the hierarchy that contains all of F_{1}, F_{2}, …. Note that we do not stipulate in this definition whether the set {F_{1}, F_{2}, …} is finite or infinite.

3.1 Parametrization

The first, and most important, of our features are those which allow the declaration of variables and constants with parameters. This mechanism is taken as fundamental by the systems of the AUTOMATH [5] family as well as PAL^{+} [9], but can be seen as a subsystem of almost all logical frameworks. Parametrization provides a common core, above which the different forms of abstraction (λ-abstraction with typed or untyped domains, and with β- or βη-conversion, as well as PAL^{+}-style abstraction by let-definition) can be built as conservative extensions.

We define a series of features: SPar (1), SPar (2), SPar (3), …, and also LPar (1), LPar (2), LPar (3), …. These extend one another in the manner shown in Figure 2.

[figure: LPar (1); ⊂; LPar (2); ⊂; ⋯; ⊂; LPar (ω)]

[figure: BF; ⊂; SPar (1); ∪; ⊂; SPar (2); ∪; ⊂; ⋯; ⊂; SPar (ω); ∪]

Fig. 2. The initial fragment of the modular hierarchy

BF already allows the declaration of constants in kinds: c_{1} : A.

LPar (1) allows the declaration of constants in first-order kinds: c_{2} : (x_{1} : A_{1}, …, x_{n} : A_{n})A. This declaration indicates that c is a constant that takes parameters x_{1} of kind A_{1}, …, x_{n} of kind A_{n}, and returns a term c_{2}[x_{1}, …, x_{n}] of kind A.

LPar (2) allows the parameters themselves to have parameters: c_{3} : (x_{1} : (x_{11} : A_{11}, …, x_{1k_{1}} : A_{1k_{1}})A_{1}, …, x_{n} : (x_{n1} : A_{n1}, …, x_{nk_{n}} : A_{nk_{n}})A_{n})A. LPar (3) allows these second-order parameters to have parameters, and so on. Similarly for declaration of variables.

We also define the feature LPar (ω) to be the union of all these features, allowing any level of parametrization.

The sequence of features SPar (n) is similar; the only difference is that, in SPar (n), every parameter must be in a small kind; that is, each A_{i}, A_{ij}, … above must be of the form El(a); it cannot be Type. (In SPar (n), A itself, the rightmost kind, can be Type in the declaration of a constant, but not in a declaration of a variable.)

The full details of these features are as follows:

Parameters in Small Kinds, SPar (n)

Grammar Before we can introduce the new grammar constructors, we need to make a few definitions.

We define an m-th order pure context by recursion on m as follows. An m-th order pure context is a string of the form

(x_{1} : (Δ_{1}) El(a_{1}), …, x_{k} : (Δ_{k}) El(a_{k}))

where each x_{i} is a variable, all distinct, Δ_{i} a pure context of order < m, and a_{i} a term. Its domain is (x_{1}, …, x_{k}).

We define an abstraction to be a string of the form

[x]M

where x is a sequence of distinct variables, and M a term. We take each member of x to be bound within M in this abstraction, and we define free and bound variables and identify all our expressions up to α-conversion in the usual manner. We writeˆ M,ˆ N, … for arbitrary abstractions. It is important to note that these are not first-class objects of every framework that contains SPar (n).

Now, we add the following clause to the grammar:

z[ˆ M]

is a term, where z is a variable or constant, andˆ M a sequence of abstractions.. This clause subsumes the grammar of BF, for x() and c() are terms when x is a 0-ary variable and c a 0-ary constant.

We also allow declarations of the form

c : (Δ)A

in the signature, where c is a constant, Δ a pure context of order ≤ n, and A a kind; and those of the form

x : (Δ) El(a)

in the context, where x is a variable, Δ a pure context of order ≤ n, and a a term. Again, these subsume those of BF.

Defined Operations We define the operation of instantiation as follows. This operation takes the place of substitution; we cannot substitute for a variable of kind (Δ)A, as we have no first-class objects in such a kind — indeed, we have no such kind yet. But it is possible define a term

{ˆ M_{1}/x_{1}, …,ˆ M_{m}/x_{m}}M

where M is a term, and, for i = 1, …, m, ˆ M_{i} ≡ [y_{i}]M_{i} is an abstraction, and x_{i} a variable, in such a way that first-class abstractions are never needed. They can, later, be added as a conservative extension. It may aid the understanding of the definition of instantiation to note that, once abstractions are added,

{ˆ M_{1}/x_{1}, …,ˆ M_{m}/x_{m}} is the normal form of [ˆ M_{1}/x_{1}, …,ˆ M_{m}/x_{m}]

The definition is as follows:

{ˆ M/x}z(ˆ N) ≡ z({ˆ M/x}ˆ N)

(if z is a constant or a variable not in x)

{ˆ M/x}x_{i}(ˆ N) ≡ {{ˆ M/x}ˆ N/y_{i}}M_{i}

We also need a defined judgement form. If ˆ M is an abstraction sequence, and Δ a pure context, we define a set of judgements

Γ ⊩_{Σ} ˆ M :: Δ

(read: under signature Σ and context Γ, ˆ M satisfies Δ). The definition is as follows. Let

Δ ≡ x_{1} : (Δ_{1}) El(a_{1}), …, x_{m} : (Δ_{m}) El(a_{m})

and let

ˆ M_{i} ≡ [y_{i}]M_{i} .

We take Γ ⊩_{Σ} ˆ M :: Δ to be defined only when y_{i} ≡ Δ_{i} for all i.

Γ ⊩_{Σ} ˆ M :: Δ

is the following set of judgements:

Γ, Δ_{1} ⊢_{Σ} M_{1} : El(a_{1})
Γ, {ˆ M_{1}/x_{1}}Δ_{2} ⊢_{Σ} M_{2} : El({ˆ M_{1}/x_{1}}a_{2})
Γ, {ˆ M_{1}/x_{1},ˆ M_{2}/x_{2}}Δ_{3} ⊢_{Σ} M_{3} : El({ˆ M_{1}/x_{1},ˆ M_{2}/x_{2}}a_{3})
⋮
Γ, {ˆ M_{1}/x_{1}, …,ˆ M_{m−1}/x_{m−1}}Δ_{m} ⊢_{Σ} M_{m} : El({ˆ M_{1}/x_{1}, …,ˆ M_{m−1}/x_{m−1}}a_{m})

In the case m = 0, we take Γ ⊩_{Σ} ˆ M :: Δ (i.e. Γ ⊩_{Σ} ⟨⟩ :: ⟨⟩) to be the single judgement

Γ ⊢_{Σ} valid .

Rules of Deduction The rules of deduction in SPar (n) are as follows:

Δ ⊢_{Σ} valid
\overline{(c ∉ dom Σ)}
Σ, c : (Δ)Type sig

Δ ⊢_{Σ} a : Type
\overline{(c ∉ dom Σ)}
Σ, c : (Δ) El(a) sig
Γ, Δ ⊢_{Σ} a : Type
\overline{(x ∉ dom Γ)}
Γ, x : (Δ) El(a) ⊢_{Σ} valid

Γ ⊩_{Σ} ˆ M :: Δ
\overline{(c : (Δ)A ∈ Σ)}
Γ ⊢_{Σ} c[ˆ M] : {ˆ M/ dom Δ}A
Γ ⊩_{Σ} ˆ M :: Δ
\overline{(x : (Δ) El(a) ∈ Γ)}
Γ ⊢_{Σ} x[ˆ M] : El({ˆ M/ dom Δ}a)

Finally, SPar (ω) is defined to be the union of all the features SPar (n).

Parameters in Large Kinds, LPar (n) The features LPar (n) and LPar (ω) are defined in exactly the same manner as SPar (n) and SPar (ω), with only two differences. The first is the definition of pure context, which now allows Type to appear:

An m-th order pure context is a string of the form

(x_{1} : (Δ_{1})A_{1}, …, x_{k} : (Δ_{k})A_{k})

where each x_{i} is a variable, all distinct, Δ_{i} is a pure context of order < m, and A_{i} is either Type or El(a_{i}) for some term a_{i}.

The second is that large kinds are permitted in context declarations as well as signature declarations; that is, we allow declarations of the form x : (Δ)A in the context, where x is a variable, Δ a pure context of appropriate order, and A either Type or El(a) for some term a.

3.2 Lambda Abstraction

We can now, if we wish, build in traditional λ-abstraction. It should be noted that this does not change the class of object theories that can be expressed by the framework.

We can make these abstractions typed or untyped (i.e. explicitly include the domain or not), and we can choose to use β or βη-conversion. These two choices lead to four features that can be added to a framework. We shall denote them λ_{β}^{t}, λ_{β}^{ut}, λ_{βη}^{t}, λ_{βη}^{ut}. We shall give here the details of λ_{β}^{t}; the others are very similar.

We shall describe here a feature λ_{β}^{t} to be built on top of BF + LPar (ω). It would be easy to change the details to give a feature that could be added to BF + LPar (n), BF + SPar (n), or BF + SPar (ω).

We add the following clauses to the grammar:

Term M ::= ⋯ | [x : A]M | M[M]
Kind A ::= ⋯ | (x : A)A

There are two redundancies in the feature λ_{β}^{t}. The first: let c be a constant, where Let

c : (x_{1} : (Δ_{1})A_{1}, …, x_{m} : (Δ_{m})A_{m})A

be in the signature, where

Δ_{i} ≡ (x_{i1} : (Δ_{i1})A_{i1}, …, x_{ik_{i}} : (Δ_{ik_{i}})A_{ik_{i}})A_{i} .

Then we identify the term

c[[x_{1}]M_{1}, …, [x_{m}]M_{m}]

with the base term

c[[x_{11} : (Δ_{11})A_{11}] ⋯ [x_{1k_{1}} : (Δ_{1k_{1}})A_{1k_{1}}]M_{1}] ⋯
[[x_{m1} : (Δ_{m1})A_{m1}] ⋯ [x_{mk_{m}} : (Δ_{mk_{m}})A_{mk_{m}}]M_{m}]

The second is a similar redundancy for terms beginning with a variable.

We define the relations of β-reduction, β-conversion, etc. on our classes of terms in the usual manner, based on the contraction

([x : (Δ)A]M)[N] ⇝_{β} [N/x]M .

The rules of deduction in λ_{β}^{t} are now:

Γ, x : A ⊢_{Σ} B kind
Γ ⊢_{Σ} (x : A)B kind

⊢_{Σ} A kind ; \overline{(c ∉ dom Σ)} ; Σ, c : A sig Γ ⊢_{Σ} A kind

\overline{(x ∉ dom Γ)}
Γ, x : A ⊢_{Σ} valid
{Γ, x : A ⊢_{Σ} M : B \atop Γ ⊢_{Σ} [x : A]M : (x : A)B}  {Γ ⊢_{Σ} M : (x : A)B Γ ⊢_{Σ} N : A \atop Γ ⊢_{Σ} M[N] : [N/x]B}
Γ ⊢_{Σ} M : A Γ ⊢_{Σ} B kind
\overline{(A =_{β} B)}
Γ ⊢_{Σ} M : B

3.3 Other Features

We present a summary of other features in Figures 3 and 4. Each of these features depends on SPar (ω). It would be easy enough to write a version dependent on SPar (n) for some finite n.

3.4 Conservativity Results

The guiding principle behind the modular hierarchy is that the features are defined, and behave, independently of one another. The formal result that corresponds to this principle is:

Theorem 1. If L is a logical framework in the hierarchy, and F a feature such that every feature on which F depends is present in L, then L + F is a conservative extension of L.

This theorem can be proven for the finitely many features we have presented in this paper. We prove that, if J is a judgement of L derivable in L + F, then J is derivable in L, by direct induction on the derivation of J in L + F. The only non-trivial cases are the conversion rules; these require the Church-Rosser property to be proven for the set of typable terms. This is never too demanding; even the case of βη-conversion can be handled using, for example, the techniques of [7], because the frameworks, as type systems, are very simple: there is a single predicative universe and no reflection.

Global Definition of Constants, cdef Depends on SPar (ω).

Signature Declaration γ ::= ⋯ | c^{α}[Δ^{α}] := M : A

If c[Δ] := M : A is in the signature, the following is a reduction rule:

c[ˆ N] ⇝_{δ_{c}} {ˆ N/ dom Δ}

Δ ⊢_{Σ} M : A ; \overline{(c ∉ dom Σ)} ; Σ, c[Δ] := M : A sig  Γ ⊢_{Σ} M : A Γ ⊢_{Σ} B kind ; \overline{(Γ ⊢_{Σ} A =_{δ_{c}} B)} ; Γ ⊢_{Σ} M : B
Γ ⊩_{Σ} ˆ N :: Δ

\overline{(c[Δ] := M : A ∈ Σ)}

Γ ⊢_{Σ} c[ˆ N] : {ˆ N/ dom Δ}A

Global Definition of Variables, vdef Depends on SPar (ω).

Context Declaration δ ::= ⋯ | x^{α}[Δ^{α}] := M : A

If x^{α}[Δ^{α}] := M^{β} : A^{β} is in the context, the following is a reduction rule:

x[ˆ N] ⇝_{δ_{v}} {ˆ N/ dom Δ}M

Γ, Δ ⊢_{Σ} M : A
\overline{(x ∉ dom Γ)}

Γ, x[Δ] := M : A ⊢_{Σ} valid

Γ ⊢_{Σ} M : A Γ ⊢_{Σ} B kind ; \overline{(Γ ⊢_{Σ} a =_{δ_{v}} b)} ; Γ ⊢_{Σ} M : B

Γ ⊩_{Σ} ˆ N :: Δ
\overline{(x[Δ] := M : A ∈ Γ)}
Γ ⊢_{Σ} x[ˆ N] : {ˆ N/ dom Δ}A

Local Definitions, let Depends on vdef.

Term M ::= ⋯ | let x^{α}[Δ^{α}] := M : A in M
Kind A ::= ⋯ | let x^{α}[Δ^{α}] := M : A in A

let v[Δ] = M : A in N ⇝_{δ} {[dom Δ]M/v}N
let v[Δ] = M : A in K ⇝_{δ} {[dom Δ]M/v}K

Γ, v[Δ] = M : A ⊢_{Σ} K kind
Γ ⊢_{Σ} let v[Δ] = M : A in K kind

Γ ⊢_{Σ} M : A Γ ⊢_{Σ} B kind ; \overline{(A =_{δ} B)} ; Γ ⊢_{Σ} M : B

Γ, v[Δ] = M : A ⊢_{Σ} N : K

Γ ⊢_{Σ} let v[Δ] = M : A in N : let v[Δ] = M : A in K

Fig. 3. Miscellaneous features

Judgemental Equality, eq Depends on SPar (ω).

Judgement body  J ::= ⋯ | M = M : A | A = A
Signature declaration δ ::= ⋯ | (Δ)(M = M : A)

Γ ⊢_{Σ} M : A Γ ⊢_{Σ} N : A ; \overline{(M = N)} ; Γ ⊢_{Σ} M = N : A Γ ⊢_{Σ} A kind Γ ⊢_{Σ} B kind

Γ ⊢_{Σ} A = B

{Δ ⊢_{Σ} M : A Δ ⊢_{Σ} N : A \atop Σ, (Δ)(M = N : A) sig}

Γ ⊩_{Σ} ˆ P :: Δ
\overline{((Δ)(M = N : A) ∈ Σ)}

Γ ⊢_{Σ} {ˆ P/ dom Δ}M = {ˆ P/ dom Δ}N : {ˆ P/ dom Δ}A

{Γ ⊢_{Σ} M = N : A \atop Γ ⊢_{Σ} N = M : A}  {Γ ⊢_{Σ} M = N : A Γ ⊢_{Σ} N = P : A \atop Γ ⊢_{Σ} M = P : A}

{Γ ⊢_{Σ} A = B \atop Γ ⊢_{Σ} B = A}  {Γ ⊢_{Σ} A = B Γ ⊢_{Σ} B = C \atop Γ ⊢_{Σ} A = C}

{Γ ⊢_{Σ} M : A Γ ⊢_{Σ} A = B \atop Γ ⊢_{Σ} M : B}  {Γ ⊢_{Σ} M = N : A Γ ⊢_{Σ} A = B \atop Γ ⊢_{Σ} M = N : B}

Fig. 4. Miscellaneous features

4 Existing Logical Frameworks

We show here how several existing logical frameworks are equivalent to systems that are built out of the features we have introduced. As well as the frameworks we have already mentioned, we deal with Luo’s frameworks LF [8].

PAL = BF + LPar (1) + cdef
AUT-68 ≃ BF + SPar (ω) + λ_{β}^{t} + LPar (1) + cdef
AUT-QE ≃ BF + LPar (ω) + λ_{β}^{t} + cdef
ELF = BF + SPar (ω) + λ_{β}^{t}
Martin-Löf’s Theory of Types = BF + LPar (ω) + λ_{βη}^{ut} + eq
LF = BF + LPar (ω) + λ_{βη}^{t} + eq

(Note: in the second line, the version of λ_{β}^{t} included is built on top of SPar (ω) only, not LPar (1). AUT −68 allows the declaration of constants with first-order parameters, but does not allow such lambda-abstractions to be formed.)

The notion of equivalence with which we are working is the possiblity of defining a translations between the members of the syntactic classes of the two frameworks, such that the translate of each rule of deduction of one is admissible in the other, and which are inverses of one another up to the relevant notion of convertibility within each framework.

For the lines in which we have used an equality sign, such translations can be given; the correspondence between the existing framework and the one produced by the hierarchy is fairly close. For the first two ‘AUT-’ frameworks, the correspondence is not nearly as neat. There is a correspondence between the hierarchy framework and a variant of the AUTOMATH framework. This variant removes the distinction between, for example, the constant defined by

(0, x, −, A), (x, c, PN, B)

(defining c with parameter x : A inside the kind B) and that defined by

(0, c, PN, [x : A]B)

(defining c with no parameters inside the kind [x : A]B). It also replaces AU-TOMATH’s system of declaring variables with a more orthodox system of contexts.

It is possible to make the correspondence in these two cases better; and it is also possible to tighten the other four, so that the translations are inverses up to identity (that is, α-conversion), not just convertibility. However, doing so requires a large number of features to be defined, with hair-splitting distinctions being made between them. It is not at all clear that the advantages are worth this cost.

To build PAL^{+} in the hierarchy, there are two possibilities. Firstly, we could write a feature that introduces classes of α-ary terms and kinds for every arity α, in a similar manner to λ_{β}^{t}, but the only such terms are the α-ary variables and constants. Then we could build on top of this a features similar to vdef and let, but allowing global and local definitions of any arity term and kind. Putting these three features on top of BF + LPar (ω) + eq yields a framework equivalent to PAL^{+}.

Alternatively, we could build features similar to vdef and let on top of BF+LPar (ω)+eq+λ_{βη}^{t}, including a redundancy that identifies [x_{1} : A_{1}] ⋯ [x_{n} : A_{n}]M with let v[x_{1} : A_{1}, …, x_{n} : A_{n}] = M : A in v, where A is an inferred kind for M.

5 Use of Frameworks

Note that all the existing frameworks we have considered (with the notable exception of PAL) use either SPar (ω) or LPar (ω). This is natural if one is approaching frameworks from the point of view of the lambda calculus; these are the easiest features to define as (say) PTSs. However, it is overkill. For:

Theorem 2. – The grammar of propositional logic, and Hilbert-style rules of

inference, are representable in BF + SPar (1).

– The grammar of predicate logic, and natural deduction-style rules of inference, are representable in BF + SPar (2).

– Martin-Löf’s Theory of Sets is representable in BF + LPar (2) + eq.

We only have space here to partially justify a few of these claims. We shall show how to build an arbitrary first-order theory in BF + SPar (2), and how W-types are built within BF + LPar (2) + eq.

For a first-order theory in BF + SPar (2), the signature consists of:

term : Type
F : (x_{1} : El(term), …, x_{n} : El(term)) El(term)

for each n-ary function symbol F in the language

prop : Type
P : (x_{1} : El(term), …, x_{n} : El(term)) El(prop)

for each n-ary predicate symbol P in the language

→ : (x : El(prop), y : El(prop)) El(prop)
∀ : (p : (x : El(term)) El(prop)) El(prop)
Prf : (x : El(prop))Type
→ I : (p, q : El(prop), H : (x : El(Prf[p])) El(Prf[q])) El(Prf[→ [p, q]])
→ E : (p, q : El(prop), H_{1} : El(Prf[→ [p, q]]), H_{2} : El(Prf[p])) El(Prf[q])
∀I : (p : (x : El(term)) El(prop), H : (x : El(term)) El(Prf[p[x]])) El(Prf[∀[p]])
∀E : (p : (x : El(term)) El(prop), t : El(term), H : El(Prf[∀[p]])) El(Prf[p[t]])

Theorem 3. 1. There is a bijection ρ between the terms with free variables among x_{1}, …, x_{n} in the first-order language, and the terms M such that

x_{1} : El(term), …, x_{n} : El(term) ⊢_{Σ} M : El(term)

2. There is a bijection σ between the formulas with free variables among x_{1}, …, x_{n} in the first-order language, and the terms M such that

x_{1} : El(term), …, x_{n} : El(term) ⊢_{Σ} M : El(prop)

3. Let ϕ, ψ_{1}, …, ψ_{m} be formulas with free variables among x_{1}, …, x_{n}. Then ϕ is provable from hypothese ψ_{1}, …, ψ_{m} iff there is a term M such that

x_{1} : El(term), …, x_{n} : El(term), y_{1} : El(Prf[σ(ψ_{1})]), …, y_{m} : El(Prf[σ(ψ_{m})])

⊢_{Σ} M : El(Prf[σ(ϕ)])

Notice that the correspondance between the entities of the object logic and the terms of the logical framework is a bijection up to identity (that is, αconversion), not up to convertibility; indeed, in a framework whose only features are SPar (n) and LPar (n), there is no such thing as convertibility. This theorem is much easier to prove than most adequacy theorems, because the correspondence between the framework and the object logic is so much closer than in a traditional logical framework.

We now show how to build W -types within BF + LPar (2) + eq. In the following, we shall suppress instances of El, and use η-contractions; e.g. we write W [A, B] for W [A, [x : A]B[x]].

W : (A : Type, B : (A)Type)Type,
sup : (A : Type, B : (A)Type, a : A, b : (B[a])W [A, B])W [A, B]
E_{W} : (A : Type, B : (A)Type, C : (W [A, B])Type,
f : (x : A, y : (B[x])W [A, B],
g : (v : B[x])C[y[v]])C[sup[A, B, x, y]],
z : W [A, B])C[z],

(A : Type, B : (A)Type, C : (W [A, B])Type, f : (x : A, y : (B[x])W [A, B], g : (v : B[x])C[y[v]])C[sup[A, B, x, y]], a : A, b : (B[a])W [A, B]) E_{W} [A, B, C, f, g, sup[A, B, a, b]] = f[a, b, [v : B[x]]E_{W} [A, B, C, f, g, y[v]]]

: C[sup[A, B, a, b]]

6 Conclusion

We have given a modular method for defining logical frameworks, and shown that it captures, up to a reasonable notion of equivalence, several existing logical frameworks. It has revealed common subsystems between these frameworks that may not otherwise have been found — it is doubtful, for example, that one would have discovered the fact that there is a system BF + SPar (ω) which can be conservatively embedded in both ELF and Martin-Löf’s Theory of Types without this work. It has revealed much weaker frameworks than we are accustomed to using, that may prove advantageous for theoretical work, such as proving adequacy theorems. And, finally, it may yet provide a method for defining features in a generic manner such that they can be added to any logical framework, and their properties studied independently of any framework.

Future and Related Work

The only work of a similar nature of which I am aware is the Tinkertype system [10]. There are striking similarities between the two systems. However, I believe this work is different in character. Tinkertype’s features cannot be defined separately, and do not behave independently; they certainly do not always yield conservative extensions. While this would not be a desideratum for type systems in general, as with which Tinkertype deals, I believe it is important for logical frameworks.

In the future, as well as the obvious matters of defining more features, capturing more aspects of logical frameworks, and exploring the properties of features independently of one another, it would be interesting to see if we could lay down general conditions C_{1}, C_{2}, … on features, and prove results such as:

Any feature with conditions C_{1}, C_{2}, … yields a conservative extension of any framework composed solely of features that satisfy conditions C_{1}, C_{2}, …

It would also be interesting to see if we could prove generalised adequacy results using the hierarchy, and give general definitions of semantics for an object theory and prove generalised soundness and completeness results.

References

1. Pientka, B., Pfenning, F.: Optimizing higher-order pattern unification (2003)

2. Jojgov, G.I.: Holes with binding power. In: Types for Proofs and Programs: International Workshop, TYPES 2002, Berg en Dal, The Netherlands, April 24-28, 2002. Selected Papers. Volume 2646 of LNCS., Springer-Verlag Heidelberg (2003) 162 – 181

3. Harper, R., Honsell, F., Plotkin, G.: A framework for defining logics. In: Proceedings 2nd Annual IEEE Symp. on Logic in Computer Science, LICS’87, Ithaca, NY, USA, 22–25 June 1987, New York, IEEE Computer Society Press (1987) 194–204

4. Nordström, B., Petersson, K., Smith, J.: Programming in Martin-Löf’s Type Theory: an Introduction. Oxford University Press (1990)

5. Nederpelt, R.P., Geuvers, J.H., Vrijer, R.C.D., eds.: Selected Papers on AU-TOMATH. Number 133 in Studies in Logic and the Foundations of Mathematics. North-Holland (1994)

6. Klop, J.W., van Oostrom, V., van Raamsdonk, F.: Combinatory reduction systems: introduction and survey. Theoretical Computer Science 121 (1993) 279–308

7. Ghani, N.: Eta-expansions in dependent type theory — the calculus of constructions. In de Groote, P., Hindley, J.R., eds.: Proceedings of the Third International Conference on Typed Lambda Calculus and Applications (TLCA’97), Nancy, France, Springer-Verlag LNCS 1210 (1997) 164–180

8. Luo, Z.: Computation and Reasoning: A Type Theory for Computer Science. Number 11 in International Series of Monographs on Computer Science. Oxford University Press (1994)

9. Luo, Z.: PAL^{+}: a lambda-free logical framework. Journal of Functional Programming 13 (2003) 317–338

10. Levin, M.Y., Pierce, B.C.: Tinkertype: A language for playing with formal systems. Technical report (2000)