LF (logical framework)
Encyclopedia
In logic
, a logical framework provides a means to define (or present) a logic as a signature in a higher-order type theory
in such a way that provability of a formula in the original logic reduces to a type inhabitation problem in the framework type theory. This approach has been used successfully for (interactive) automated theorem proving
. The first logical framework was Automath, however the name of the idea comes from the more widely known Edinburgh Logical Framework, LF. Several more recent proof tools like Isabelle (theorem prover) are based on this idea. Unlike a direct embedding, the logical framework approach allows many logics to be embedded in the same type system.
A logical framework 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:
This is summarized by:
‘Framework = Language + Representation’.
-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 representation mechanism. This is inspired by Per Martin-Löf
's development of Kant
's notion of judgement, in the 1983 Siena Lectures. The two higher-order judgements, the hypothetical
and the general, 
, 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 
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 
.
An implementation of the LF logical framework is provided by the Twelf
system at Carnegie Mellon University
. Twelf includes
Logic
In philosophy, Logic is the formal systematic study of the principles of valid inference and correct reasoning. Logic is used in most intellectual activities, but is studied primarily in the disciplines of philosophy, mathematics, semantics, and computer science...
, a logical framework provides a means to define (or present) a logic as a signature in a higher-order type theory
Type theory
In mathematics, logic and computer science, type theory is any of several formal systems that can serve as alternatives to naive set theory, or the study of such formalisms in general...
in such a way that provability of a formula in the original logic reduces to a type inhabitation problem in the framework type theory. This approach has been used successfully for (interactive) automated theorem proving
Automated theorem proving
Automated theorem proving or automated deduction, currently the most well-developed subfield of automated reasoning , is the proving of mathematical theorems by a computer program.- Decidability of the problem :...
. The first logical framework was Automath, however the name of the idea comes from the more widely known Edinburgh Logical Framework, LF. Several more recent proof tools like Isabelle (theorem prover) are based on this idea. Unlike a direct embedding, the logical framework approach allows many logics to be embedded in the same type system.
A logical framework 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
Per Martin-Löf
Per Erik Rutger Martin-Löf is a Swedish logician, philosopher, and mathematical statistician. He is internationally renowned for his work on the foundations of probability, statistics, mathematical logic, and computer science. Since the late 1970s, Martin-Löf's publications have been mainly in...
's system of arities.
To describe a logical framework, one must provide the following:
- A characterization of the class of object-logics to be represented;
- An appropriate meta-language;
- A characterization of the mechanism by which object-logics are represented.
This is summarized by:
‘Framework = Language + Representation’.
LF as example
In the case of the LF logical framework, the meta-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 decidableDecidability (logic)
In logic, the term decidable refers to the decision problem, the question of the existence of an effective method for determining membership in a set of formulas. Logical systems such as propositional logic are decidable if membership in their set of logically valid formulas can be effectively...
. However, type inference
Type inference
Type inference refers to the automatic deduction of the type of an expression in a programming language. If some, but not all, type annotations are already present it is referred to as type reconstruction....
is undecidable
Decidability (logic)
In logic, the term decidable refers to the decision problem, the question of the existence of an effective method for determining membership in a set of formulas. Logical systems such as propositional logic are decidable if membership in their set of logically valid formulas can be effectively...
.
A logic is represented in the LF logical framework by the judgements-as-types representation mechanism. This is inspired by Per Martin-Löf
Per Martin-Löf
Per Erik Rutger Martin-Löf is a Swedish logician, philosopher, and mathematical statistician. He is internationally renowned for his work on the foundations of probability, statistics, mathematical logic, and computer science. Since the late 1970s, Martin-Löf's publications have been mainly in...
's development of Kant
KANT
KANT is a computer algebra system for mathematicians interested in algebraic number theory, performing sophisticated computations in algebraic number fields, in global function fields, and in local fields. KASH is the associated command line interface...
's notion of judgement, in the 1983 Siena Lectures. The two higher-order judgements, the hypothetical
and the general, , 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 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 .An implementation of the LF logical framework is provided by the Twelf
Twelf
Twelf is an implementation of the logical framework LF. It is used for logic programming and for the formalization of programming language theory.-Introduction:...
system at Carnegie Mellon University
Carnegie Mellon University
Carnegie Mellon University is a private research university in Pittsburgh, Pennsylvania, United States....
. Twelf includes
- a logic programming engine
- meta-theoretic reasoning about logic programs (termination, coverage, etc.)
- an inductive meta-logical theorem prover
Further reading
- Robert HarperRobert Harper (computer scientist)Robert "Bob" William Harper, Jr. is a computer science professor at Carnegie Mellon University who works in programming language research. He made major contributions to the design of the Standard ML programming language and the LF logical framework....
, Furio Honsell and Gordon PlotkinGordon PlotkinGordon D. Plotkin, FRS, FRSE is a Scottish computer scientist.Gordon Plotkin is best-known for his introduction of structural operational semantics and his work on denotational semantics. In particular, his notes on A Structural Approach to Operational Semantics of 1981 were very influential...
. 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. Using typed lambda calculus to implement formal systems 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
-calculus. Journal of Logic and Computation 12(6), 1061-1104, 2002. - Per Martin-Löf. "On the Meanings of the Logical Constants and the Justifications of the Logical Laws." "Nordic Journal of Philosophical LogicNordic Journal of Philosophical LogicThe Nordic Journal of Philosophical Logic was an international journal of philosophy started in May 1996. The journal considered submissions in any of the areas associated with Philosophical Logic and with the application of logic in conceptual analysis. The journal was edited at the Department of...
", 1(1): 11-60, 1996. - Bengt Nordström, Kent Petersson, and Jan M. Smith. Programming in Martin-Löf's Type Theory. Oxford University Press, 1990. (The book is out of print, but a free version has been made available.)
- David Pym. A Note on the Proof Theory of the
-calculus. Studia Logica 54: 199-230, 1995. - David Pym and Lincoln Wallen. Proof-search in the
-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
-calculus. Int. J. of Foundations of Computer Science 3(3), 333-378, 1992.
External links
- Specific Logical Frameworks and Implementations (a list maintained by Frank PfenningFrank PfenningFrank Pfenning is a professor of computer science, and adjunct professor in the department of philosophy, at Carnegie Mellon University. He received his Ph.D. from the Carnegie Mellon University Department of Mathematics in 1987, for his dissertation entitled Proof Transformations in Higher-Order...
)