LF (logical framework)

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 summarized by:

"‘Framework = Language + Representation’".

In the case of the LF logical framework, the language is the $lambdaPi$-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 $lambdaPi$-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 representation mechanism. This is inspired by from Per Martin-Löf's development of Kant's notion of judgement. The two higher-order judgements, the hypothetical $Jvdash\; K$ and the general, $Lambda\; xin\; 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-logic's rules and proofs are seen as primitive proofs of hypothetico-general judgements $Lambda\; xin\; C.\; J(x)vdash\; K$.

An implementation of the LF logical framework is provided by 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

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.
*Samin Ishtiaq and David Pym. "A Relevant Analysis of Natural Deduction". Journal of Logic and Computation 8, 809-838, 1998.
* Samin Ishtiaq and David Pym. "Kripke Resource Models of a Dependently-typed, Bunched $lambda$-calculus". Journal of Logic and Computation 12(6), 1061-1104, 2002.
*David Pym. "A Note on the Proof Theory of the $lambdaPi$-calculus". Studia Logica 54: 199-230, 1995.
*David Pym and Lincoln Wallen. "Proof-search in the $lambdaPi$-calculus". In: G. Huet and G. Plotkin (eds), Logical Frameworks, Cambridge University Press, 1991.
*Didier Galmiche and David Pym. "Proof-search in type-theoretic languages:an introduction". Theoretical Computer Science 232 (2000) 5-53.
*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.
*David Pym. "Proofs, Search and Computation in General Logic". Ph.D. thesis, University of Edinburgh, 1990.
*David Pym. "A Unification Algorithm for the $lambdaPi$-calculus." Int. J. of Foundations of Computer Science 3(3), 333-378, 1992.