LF (logical framework)

From Wikipedia, the free encyclopedia

You have new messages (last change).

In type theory, the LF logical framework provides a means to define (or present) logics. It is based on a general treatment of syntax, rules and proofs by means of a dependently typed lambda calculus. Syntax is treated in a style similar to, but more general than Per Martin-Löf's system of arities.

To describe a logical framework, one must provide the following:

1. A characterization of the class of object-logics to be represented;

2. An appropriate meta-language;

3. A characterization of the mechanism by which object-logics are represented.

This is summarised by:

‘Framework = Language + Representation’.

In the case of the LF logical framework, the language is the λΠ-calculus. This is a system of first-order dependent function types which are related by the Propositions as types principle to first-order minimal logic. The key features of the λΠ-calculus are that it consists of entities of three levels: objects, types and families of types. It is predicative, all well-typed terms are strongly normalizing and Church-Rosser and the property of being well-typed is decidable. However, type inference is undecidable.

A logic is represented in the LF logical framework by the judgements-as-types encoding. This originates from Per Martin-Löfs development of Kant's notion of judgement. The two higher-order judgements, the hypothetical J\vdash K and the general, \Lambda x\in J. K(x), correspond to the ordinary and dependent function space, respectively. The methodology of judgements-as-types is that judgements are represented as the types of their proofs. A logical system {\mathcal L} is represented by its signature which assigns kinds and types to a finite set of constants that represents its syntax, its judgements and its rule schemes. An object-logics rules and proofs are seen as primitive proofs of hypothetico-general judgements \Lambda x\in C. J(x)\vdash K.

The LF logical framework is implemented in the Twelf system at Carnegie Mellon University. Twelf includes

  • a logic programming engine
  • meta-theoretic reasoning about logic programs (termination, coverage, etc.)
  • an inductive meta-logical theorem prover

[edit] References

  • Robert Harper, Furio Honsell and Gordon Plotkin. A Framework For Defining Logics. Journal of the Association for Computing Machinery, 40(1):143-184, 1993
  • Arnon Avron, Furio Honsell, Ian Mason and Randy Pollack. Used Typed Lambda Calculus to Implement on a Machine. Journal of Automated Reasoning, 9:309-354, 1992.
  • Robert Harper. An Equational Formulation of LF. Technical Report, University of Edinburgh, 1988. LFCS report ECS-LFCS-88-67.
  • Robert Harper, Donald Sannella and Andrzej Tarlecki. Structured Theory Presentations and Logic Representations. Annals of Pure and Applied Logic, 67(1-3):113-160, 1994.
  • Philippa Gardner. Representing Logics in Type Theory. Technical Report, University of Edinburgh, 1992. LFCS report ECS-LFCS-92-227.
  • Gilles Dowek. The undecidability of typability in the lambda-pi-calculus. In M. Bezem, J.F. Groote (Eds.), Typed Lambda Calculi and Applications. Volume 664 of Lecture Notes in Computer Science, 139-145, 1993.
Retrieved from "http://en.wikipedia.org../../../l/f/_/LF_%28logical_framework%29_1b90.html"
In other languages