Lógica para funciones computables
Logic for Computable Functions ( LCF ) es un demostrador de teoremas automatizado interactivo desarrollado en Stanford y Edimburgo por Robin Milner y colaboradores a principios de la década de 1970, basado en la base teórica de la lógica de funciones computables propuesta 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
Los teoremas del sistema son términos de un tipo de datos abstracto especial, "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 de 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 desprende de la solidez de la implementación del tipo de datos 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 la necesidad de almacenar objetos de prueba en la memoria. El tipo de datos Theorem se puede implementar fácilmente para almacenar opcionalmente objetos de prueba, según la configuración de tiempo de ejecución del sistema, por lo que generaliza 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 desarrollar teoremas significa que, según la complejidad de los programas escritos, es posible utilizar el mismo lenguaje para escribir pruebas paso a paso, procedimientos de decisión o demostradores de teoremas.
Desventajas
Base informática confiable
La implementación del compilador ML subyacente se suma a la base informática confiable . El trabajo en CakeML [1] dio como resultado un compilador ML verificado formalmente, lo que alivió 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 exactitud ha sido ampliamente analizada. Una forma sencilla de implementar estos procedimientos en un enfoque LCF requiere que dichos procedimientos siempre deriven resultados de los axiomas, lemas y reglas de inferencia del sistema, en lugar de calcular directamente el resultado. Un enfoque potencialmente más eficiente es 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 utilizar funciones totales en lugar de parciales, lo que dio lugar a HOL , HOL Light y el asistente de pruebas Isabelle , que admite varias lógicas. A partir de 2019, el asistente de pruebas Isabelle todavía contiene una implementación de una lógica LCF, Isabelle/LCF.
Notas
- ^ "CakeML" . Consultado el 2 de noviembre de 2019 .
- ^ Boyer, Robert S; Moore, J Strother. Metafunciones: cómo demostrar que son correctas y usarlas de manera eficiente como nuevos procedimientos de prueba (PDF) (Informe). Informe técnico CSL-108, SRI Projects 8527/4079. págs. 1–111. Archivado (PDF) del original el 2 de noviembre de 2019. Consultado el 2 de noviembre de 2019 .
Referencias
- Gordon, Michael J .; Milner, Arthur J.; Wadsworth, Christopher P. (1979). LCF de Edimburgo: una lógica mecanizada de computación . Apuntes de clase sobre informática. Vol. 78. Berlín Heidelberg: Springer. doi :10.1007/3-540-09724-4. ISBN 978-3-540-09724-2. Número de identificación del sujeto 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 de 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. Apuntes de clase en informática. Vol. 74. Berlín Heidelberg: Springer. págs. 146–159. doi :10.1007/3-540-09526-8_11. ISBN 978-3-540-09526-2.
 | Este artículo relacionado con la lógica matemática es un esbozo . Puedes ayudar a Wikipedia expandiéndolo. |
