Hispanopedia WikiLógica para funciones computables ( LCF ) es un demostrador de teoremas interactivo y automatizado desarrollado en Stanford y Edimburgo por Robin Milner y sus colaboradores a principios de la década de 1970, basado en los fundamentos teóricos de la lógica de funciones computables propuestos previamente por Dana Scott . El trabajo en el sistema LCF introdujo el lenguaje de programación de propósito general ML para permitir a los usuarios escribir tácticas de demostración de teoremas, admitiendo tipos de datos algebraicos , polimorfismo paramétrico , tipos de datos abstractos y excepciones .
Idea básica
En este sistema, los teoremas son términos de un tipo de dato abstracto especial denominado "teorema" . El mecanismo general de los tipos de datos abstractos de ML garantiza que los teoremas se deriven utilizando únicamente las reglas de inferencia proporcionadas por las operaciones del tipo abstracto "teorema". Los usuarios pueden escribir programas de ML de complejidad arbitraria para calcular teoremas; la validez de los teoremas no depende de la complejidad de dichos programas, sino que se deriva de la solidez de la implementación del tipo de dato abstracto y de la corrección del compilador de ML.
Ventajas
El enfoque LCF proporciona una confiabilidad similar a la de los sistemas que generan certificados de prueba explícitos, pero sin necesidad de almacenar objetos de prueba en memoria. El tipo de datos Theorem se puede implementar fácilmente para almacenar opcionalmente objetos de prueba, según la configuración de ejecución del sistema, generalizando así el enfoque básico de generación de pruebas. La decisión de diseño de utilizar un lenguaje de programación de propósito general para el desarrollo de teoremas implica que, según la complejidad de los programas escritos, es posible usar el mismo lenguaje para escribir demostraciones paso a paso, procedimientos de decisión o demostradores de teoremas.
Desventajas
Base de computación confiable
La implementación del compilador ML subyacente contribuye a la base de computación confiable . El trabajo en CakeML [ 1 ] dio como resultado un compilador ML formalmente verificado, lo que mitiga algunas de estas preocupaciones.
Eficiencia y complejidad de los procedimientos de prueba
La demostración de teoremas suele beneficiarse de procedimientos de decisión y algoritmos de demostración de teoremas, cuya corrección ha sido ampliamente analizada. Una forma directa de implementar estos procedimientos en un enfoque LCF requiere que dichos procedimientos siempre deriven los resultados de los axiomas, lemas y reglas de inferencia del sistema, en lugar de calcular directamente el resultado. Un enfoque potencialmente más eficiente consiste en utilizar la reflexión para demostrar que una función que opera sobre fórmulas siempre da un resultado correcto. [ 2 ]
Influencias
Entre las implementaciones posteriores se encuentra Cambridge LCF. Los sistemas posteriores simplificaron la lógica para usar funciones totales en lugar de parciales, lo que dio lugar a HOL , HOL Light y el asistente de pruebas Isabelle , que admite diversas lógicas. A fecha de 2019, el asistente de pruebas Isabelle todavía incluye una implementación de la lógica LCF, Isabelle/LCF.
Notas
- ↑ "CakeML" . Consultado el 2 de noviembre de 2019 .
- ↑ Boyer, Robert S; Moore, J Strother. Metafunciones: Demostración de su corrección y uso eficiente de las mismas como nuevos procedimientos de prueba (PDF) (Informe). Informe técnico CSL-108, Proyectos SRI 8527/4079. págs. 1–111 . Archivado (PDF) del original el 2 de noviembre de 2019. Recuperado el 2 de noviembre de 2019 .
Referencias
- Gordon, Michael J .; Milner, Arthur J.; Wadsworth, Christopher P. (1979). Edinburgh LCF: A Mechanised Logic of Computation . Lecture Notes in Computer Science. Vol. 78. Berlín Heidelberg: Springer. doi : 10.1007/3-540-09724-4 . ISBN 978-3-540-09724-2. S2CID 21159098 .
- Gordon, Michael JC (2000). «De LCF a HOL: una breve historia». Prueba, lenguaje e interacción . Cambridge, Massachusetts: MIT Press. pp. 169–185 . ISBN 0-262-16188-5. Consultado el 11 de octubre de 2007 .
- Loeckx, Jacques; Sieber, Kurt (1987). Los fundamentos de la verificación de programas (2ª ed.). Vieweg+Teubner Verlag. doi : 10.1007/978-3-322-96753-4 . ISBN 978-3-322-96754-1.
- Milner, Robin (mayo de 1972). Lógica para funciones computables: descripción de una implementación en máquina (PDF) . Universidad de Stanford.
- Milner, Robin (1979). «Lcf: Una forma de hacer demostraciones con una máquina». En Bečvář, Jiří (ed.). Fundamentos matemáticos de la informática 1979. Lecture Notes in Computer Science. Vol. 74. Berlín Heidelberg: Springer. pp. 146–159 . doi : 10.1007/3-540-09526-8_11 . ISBN 978-3-540-09526-2.
- Lógica en informática
- Asistentes de corrección
- Fragmentos de lógica matemática