Marco lógico

En lógica , un marco lógico proporciona un medio para definir (o presentar) una lógica como una firma en una teoría de tipos de orden superior de tal manera que la demostrabilidad de una fórmula en la lógica original se reduce a un problema de habitabilidad de tipos en la teoría de tipos del marco. ^{[1] [2]} Este enfoque se ha utilizado con éxito para la demostración automatizada (interactiva) de teoremas . El primer marco lógico fue Automath ; sin embargo, el nombre de la idea proviene del más conocido Edinburgh Logical Framework, LF . Varias herramientas de prueba más recientes como Isabelle se basan en esta idea. ^[1] A diferencia de una incrustación directa, el enfoque del marco lógico permite que muchas lógicas se incrustan en el mismo sistema de tipos. ^[3]

Descripción general

Un marco lógico se basa en un tratamiento general de la sintaxis, las reglas y las demostraciones mediante un cálculo lambda de tipos dependientes . La sintaxis se trata de un modo similar al del sistema de aridades de Per Martin-Löf , pero de un modo más general .

Para describir un marco lógico, se debe proporcionar lo siguiente:

1. Una caracterización de la clase de lógica de objetos a representar;
2. Un metalenguaje apropiado;
3. Una caracterización del mecanismo mediante el cual se representan las lógicas de objetos.

Esto se resume así:

" Marco = Lenguaje + Representación ".

Si

En el caso del marco lógico LF , el metalenguaje es el λΠ-cálculo . Este es un sistema de tipos de funciones dependientes de primer orden que están relacionados por el principio de proposiciones como tipos con la lógica mínima de primer orden . Las características clave del λΠ-cálculo son que consta de entidades de tres niveles: objetos, tipos y clases (o clases de tipos, o familias de tipos). Es predicativo , todos los términos bien tipificados son fuertemente normalizantes y Church-Rosser y la propiedad de estar bien tipificado es decidible . Sin embargo, la inferencia de tipos es indecidible.

Una lógica se representa en el marco lógico LF mediante el mecanismo de representación de juicios como tipos. Esto está inspirado en el desarrollo de la noción de juicio de Kant por parte de Per Martin-Löf , en las Conferencias de Siena de 1983. Los dos juicios de orden superior, el hipotético y el general, corresponden al espacio de funciones ordinarias y dependientes, respectivamente. La metodología de los juicios como tipos es que los juicios se representan como los tipos de sus pruebas. Un sistema lógico se representa por su firma que asigna clases y tipos a un conjunto finito de constantes que representa su sintaxis, sus juicios y sus esquemas de reglas. Las reglas y pruebas de una lógica de objetos se consideran pruebas primitivas de juicios hipotético-generales . ${\displaystyle J\vdash K}$ ${\displaystyle \Lambda x\in J.K(x)}$ ${\displaystyle {\mathcal {L}}}$ ${\displaystyle \Lambda x\in C.J(x)\vdash K}$

El sistema Twelf de la Universidad Carnegie Mellon ofrece una implementación del marco lógico LF . Twelf incluye

• un motor de programación lógica
• razonamiento metateórico sobre programas lógicos (terminación, cobertura, etc.)
• Un demostrador de teoremas metalógicos inductivos

Véase también

• Marco gramatical
• Torniquete (símbolo)

Referencias

1. Bart Jacobs (2001). Lógica categórica y teoría de tipos . Elsevier. pág. 598. ISBN 978-0-444-50853-9.
2. Dov M. Gabbay, ed. (1994). ¿Qué es un sistema lógico?. Clarendon Press . p. 382. ISBN 978-0-19-853859-2.
3. Ana Bove; Luis Soares Barbosa; Alberto Pardo (2009). Ingeniería del lenguaje y desarrollo riguroso de software: Escuela de verano internacional LerNet ALFA 2008, Piriápolis, Uruguay, 24 de febrero - 1 de marzo de 2008, Revisada, Artículos seleccionados. Springer. p. 48. ISBN 978-3-642-03152-6.

Lectura adicional

• Frank Pfenning (2002). "Marcos lógicos: una breve introducción". En Helmut Schwichtenberg , Ralf Steinbrüggen (ed.). Prueba y confiabilidad del sistema (PDF) . Saltador . ISBN 978-1-4020-0608-1.
• Robert Harper , Furio Honsell y Gordon Plotkin . Un marco para definir la lógica . Revista de la Asociación de Maquinaria Computacional, 40(1):143-184, 1993.
• Arnon Avron , Furio Honsell, Ian Mason y Randy Pollack. Uso del cálculo lambda tipado para implementar sistemas formales en una máquina . Journal of Automated Reasoning, 9:309-354, 1992.
• Robert Harper. Una formulación ecuacional de LF . Informe técnico, Universidad de Edimburgo , 1988. Informe LFCS ECS-LFCS-88-67.
• Robert Harper, Donald Sannella y Andrzej Tarlecki. Presentaciones de teoría estructurada y representaciones lógicas . Anales de lógica pura y aplicada, 67(1-3):113-160, 1994.
• Samin Ishtiaq y David Pym. Un análisis relevante de la deducción natural . Journal of Logic and Computation 8, 809-838, 1998.
• Samin Ishtiaq y David Pym. Modelos de recursos de Kripke de un cálculo agrupado de tipos dependientes ${\displaystyle \lambda }$ . Journal of Logic and Computation 12(6), 1061-1104, 2002.
• Per Martin-Löf. "Sobre los significados de las constantes lógicas y las justificaciones de las leyes lógicas". "Nordic Journal of Philosophical Logic", 1(1): 11-60, 1996.
• Bengt Nordström, Kent Petersson y Jan M. Smith. Programming in Martin-Löf's Type Theory . Oxford University Press , 1990. (El libro está agotado, pero hay una versión gratuita disponible).
• David Pym. Una nota sobre la teoría de la demostración del cálculo matemático ${\displaystyle \lambda \Pi }$ . Studia Logica 54: 199-230, 1995.
• David Pym y Lincoln Wallen . Búsqueda de pruebas en el cálculo matemático ${\displaystyle \lambda \Pi }$ . En: G. Huet y G. Plotkin (eds.), Logical Frameworks, Cambridge University Press, 1991.
• Didier Galmiche y David Pym. Búsqueda de pruebas en lenguajes de teoría de tipos: una introducción . Theoretical Computer Science 232 (2000) 5-53.
• Philippa Gardner. Representación de lógicas en la teoría de tipos . Informe técnico, Universidad de Edimburgo, 1992. Informe LFCS ECS-LFCS-92-227.
• Gilles Dowek. La indecidibilidad de la tipabilidad en el cálculo lambda-pi . En M. Bezem, JF Groote (Eds.), Typed Lambda Calculi and Applications. Volumen 664 de Lecture Notes in Computer Science , 139-145, 1993.
• David Pym. Pruebas, búsqueda y computación en lógica general . Tesis doctoral, Universidad de Edimburgo, 1990.
• David Pym. Un algoritmo de unificación para el cálculo de ecuaciones diferenciales. ${\displaystyle \lambda \Pi }$ Revista internacional de fundamentos de la ciencia informática 3(3), 333-378, 1992.

Enlaces externos

• Marcos lógicos específicos e implementaciones (una lista mantenida por Frank Pfenning , pero con enlaces en su mayoría inactivos desde 1997)