Logical framework

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.[1][2] 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 are based on this idea.[1] Unlike a direct embedding, the logical framework approach allows many logics to be embedded in the same type system.[3]

Overview

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:

  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’.

LF

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 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 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-logic's rules and proofs are seen as primitive proofs of hypothetico-general judgements \Lambda x\in C. J(x)\vdash K.

An implementation of the LF logical framework is provided by the Twelf system at Carnegie Mellon University. Twelf includes

See also

References

  1. 1 2 Bart Jacobs (2001). Categorical Logic and Type Theory. Elsevier. p. 598. ISBN 978-0-444-50853-9.
  2. Dov M. Gabbay, ed. (1994). What is a logical system?. Clarendon Press. p. 382. ISBN 978-0-19-853859-2.
  3. Ana Bove; Luis Soares Barbosa; Alberto Pardo (2009). Language Engineering and Rigourous (sic) Software Development: International LerNet ALFA Summer School 2008, Piriapolis, Uruguay, February 24 - March 1, 2008, Revised, Selected Papers. Springer. p. 48. ISBN 978-3-642-03152-6.

Further reading

External links

This article is issued from Wikipedia - version of the Friday, October 16, 2015. The text is available under the Creative Commons Attribution/Share Alike but additional terms may apply for the media files.