nLab
logical framework

Context

Deduction and Induction

Type theory

natural deduction metalanguage, practical foundations

  1. type formation rule
  2. term introduction rule
  3. term elimination rule
  4. computation rule

type theory (dependent, intensional, observational type theory, homotopy type theory)

syntax object language

computational trinitarianism = propositions as types +programs as proofs +relation type theory/category theory

logiccategory theorytype theory
trueterminal object/(-2)-truncated objecth-level 0-type/unit type
falseinitial objectempty type
proposition(-1)-truncated objecth-proposition, mere proposition
proofgeneralized elementprogram
cut rulecomposition of classifying morphisms / pullback of display mapssubstitution
cut elimination? for implicationcounit for hom-tensor adjunctionbeta reduction
introduction rule for implicationunit for hom-tensor adjunctioneta conversion
conjunctionproductproduct type
disjunctioncoproduct ((-1)-truncation of)sum type (bracket type of)
implicationinternal homfunction type
negationinternal hom into initial objectfunction type into empty type
universal quantificationdependent productdependent product type
existential quantificationdependent sum ((-1)-truncation of)dependent sum type (bracket type of)
equivalencepath space objectidentity type
equivalence classquotientquotient type
inductioncolimitinductive type, W-type, M-type
higher inductionhigher colimithigher inductive type
completely presented setdiscrete object/0-truncated objecth-level 2-type/preset/h-set
setinternal 0-groupoidBishop set/setoid
universeobject classifiertype of types
modalityclosure operator, (idemponent) monadmodal type theory, monad (in computer science)
linear logic(symmetric, closed) monoidal categorylinear type theory/quantum computation
proof netstring diagramquantum circuit
(absence of) contraction rule(absence of) diagonalno-cloning theorem
synthetic mathematicsdomain specific embedded programming language

homotopy levels

semantics

Foundations

Contents

Idea

A logical framework is a formal metalanguage for deductive systems, such as logic, natural deduction, type theories?, sequent calculus, etc. Of course, like any formal system, these systems can be described in any sufficiently stong metalanguage. However, all logical systems of this type share certain distinguishing features, so it is helpful to have a particular metalanguage which is well-adapted to describing systems with those features.

Much of the description below is taken from (Harper).

Overview

The sentences of a logical framework are called judgments. It turns out that in deductive systems, there are two kinds of non-basic forms that arise very commonly, which we may call

  • hypothetical judgments: one judgment is a logical consequence of some others.
  • generic judgments: a judgment that is made generally for all values of some parameters, each ranging over a “domain” or “syntactic category”.

These two forms turn out to have many parallel features, e.g. reflexivity and transitivity of hypothetical judgments correspond to variable-use and substitution in generic judgments. Appealing to the propositions as types principle, therefore, it is convenient to describe a system in which they are actually both instances of the same thing. That is, we identify the notion of evidence for a judgment with the notion of object of a syntactic category.

This leads to a notion that we will call an LF-type. Thus we will have types such as

  • The LF-type of evidence for some judgment.
  • The LF-type of objects of a syntactic category.

We will also have some general type-forming operations. Perhaps surprisingly, it turns out that

are all that we need.

There is a potential confusion of terminology, because these LF-types in a logical framework (being itself a type theory) are distinct from the objects that may be called “types” in any particular logic we might be talking about inside the logical framework. Thus, for instance, when formalizing Martin-Lof type theory in a logical framework, there is an “LF-type” which is the type of objects of the syntactic category of MLTT-types. This is furthermore distinct from a type of types, which is itself an object of the syntactic category of MLTT-types, i.e. a term belonging to the LF-type of such.

Once we have set up the logical framework as a language, there are then two ways to describe a given logic inside of it. See (Harper), and the other references, for more details.

Synthetic presentations

In a synthetic presentation, there is an LF-type for every judgment of the object theory. Thus, if the object theory is a type theory, then in LF we have things like:

  • an LF-type tptp of object-theory types
  • an LF-type tmtm of object-theory terms
  • a dependent LF-type of:tmtpTypeof : tm \to tp \to Type, where Type denotes the LF-kind of LF-types. That is, for each object-theory type aa and each object-theory type AA, we have an LF-type of(a,A)of(a,A) expressing the judgment “a:Aa:A” that aa is of type AA.

Note that we do not have to explicitly carry around an ambient context, as we sometimes do when presenting type theories in a more explicit style of a deductive system. This is because the notions of hypothetical and generic judgments are built into the logical framework and handled automatically by its contexts.

Synthetic presentations are very flexible, but do not make maximal use of the framework in the case when the object-theory is also a type theory whose judgments are “analytic”.

Analytic presentation

An analytic presentation is only possible for certain kinds of object-theories, generally those which are type theories similar to LF itself. In this case, we represent object-theory types by LF-types themselves. Thus instead of the LF-type tmtm of terms and the dependent LF-type ofof above, we have

  • a dependent LF-type el:tpTypeel : tp \to Type

which assigns to each object-theory type, the LF-type of its elements.

In an analytic presentation of a logic, in addition to merely giving “axioms” such as tptp and elel, we must give equations representing the rules of the object-theory as equalities in the logical framework. For instance, we must have a beta-reduction rule such as

app A B (lam A B F) M = F M

This need to specify equations makes it more difficult to implement analytic presentations on a computer. For instance, Twelf can only handle synthetic presentations.

Higher-order abstract syntax

In both synthetic and analytic presentations, we use higher-order abstract syntax? (HOAS). Roughly, this means that variables in the object-theory are not terms of some LF-type, but are represented by actual LF-variables. For instance, when describing a type theory containing function types synthetically, we would have

  • an LF-term arr:tptptparr : tp \to tp \to tp, where for object-theory types A:tpA:tp and B:tpB:tp, the term arr(A,B):tparr(A,B):tp represents their function-type
  • an LF-term app:tmtmtmapp : tm \to tm \to tm, where app(f,a)app(f,a) represents the function application f(a)f(a)
  • an LF-term lam:(tmtm)tmlam : (tm \to tm) \to tm, representing lambda abstraction.

The point is that the argument of lamlam (the “body” of the lambda abstraction) is not a “term containing a free variable xx” but rather an LF-function from object-theory terms to object-theory terms. This is intended to be the function “substitute” which knows about the body of the lambda-abstraction, and when given an argument it substitutes it for the variable in that body and returns the result.

This approach completely avoids dealing with the problems of variable binding and substitution in the object language, by making use of the binding and substitution in the metalanguage LF. One might say that the variables in LF are the “universal notion of variable” which is merely reused by all object-theories.

The power of weak frameworks

It may be tempting to think of the LF-types such as tptp and tmtm as inductively defined by their specified constructors (such as arrarr for tptp, and appapp and lamlam for tmtm). However, this is incorrect; LF does not have inductive types. In fact, this weakness is essential in order to guarantee “adequacy” of the HOAS encoding.

Suppose, for instance, that tmtm were inductively defined inside of LF. Then we could define a function tmtmtm\to tm by pattern-matching on the structure of tmtm, doing one thing if tmtm were a lambda-abstraction and another thing if it were a function application. But such a function is definitely not the sort of thing that we want to be able to pass to the LF-function lamlam! By disallowing such matching, though, we can guarantee that the only functions tmtmtm\to tm we can define and pass to lamlam correspond to “substituting in a fixed term” as we intended.

It’s worth noting that this design choice essentially renders LF incapable of representing object-theory variables in any other way than with HOAS. For ordinary usage of variables requires the ability to compare “variables” for equality and disequality, and since LF has no inductive types, we cannot define therein any type that could function as “variables” in this way.

Implementations

One of the uses of a logical framework is that as a type theory itself, it can be implemented in a computer. This provides a convenient system in which one can “program” the rules of any other specific type theory or logic which one wants to study.

For a list of logical framework implementations, see Specific logical Frameworks and Implementations.

Historically, the first logical framework implementation was Automath. The goal of the Automath project was to provide a tool for the formalization of mathematics without foundational prejudice. Many modern logical frameworks carry influences of this.

Then inspired by the development of Martin-Löf dependent type theory was the Edinburgh Logical Framework (ELF). The logic and type theory-approaches were later combined in the Elf language. This gave rise to Twelf.

References

Revised on January 14, 2014 07:47:45 by Urs Schreiber (89.204.138.142)