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 propuesto 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 "teorema" especial . El mecanismo general de tipos de datos abstractos de ML asegura que los teoremas se deriven usando solo las reglas de inferencia dadas por las operaciones del tipo abstracto de teorema. Los usuarios pueden escribir programas ML arbitrariamente complejos para calcular teoremas; la validez de los teoremas no depende de la complejidad de tales programas, sino que se deriva de la solidez de la implementación del tipo de datos abstractos y de la corrección del compilador ML.
Ventajas
El enfoque LCF proporciona una confiabilidad similar a 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 del teorema se puede implementar fácilmente para almacenar opcionalmente objetos de prueba, dependiendo de la configuración del 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 usar un lenguaje de programación de propósito general para desarrollar teoremas significa que, dependiendo de la complejidad de los programas escritos, es posible usar el mismo lenguaje para escribir pruebas paso a paso, procedimientos de decisión o probadores 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] resultó en un compilador ML verificado formalmente, lo que alivia algunas de estas preocupaciones.
Eficiencia y complejidad de los procedimientos de prueba.
La demostración de teoremas a menudo se beneficia de los procedimientos de decisión y de los algoritmos de demostración de teoremas, cuya corrección 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 con 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 funciones parciales, lo que llevó a un asistente de prueba HOL , HOL Light e Isabelle que admite varias lógicas. A partir de 2019, el asistente de pruebas de 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: demostrar que son correctas y usarlas de manera eficiente como nuevos procedimientos de prueba (PDF) (Informe). Informe técnico CSL-108, Proyectos SRI 8527/4079. págs. 1-111 . Consultado el 2 de noviembre de 2019 .
Referencias
- Gordon, Michael J .; Milner, Arthur J .; Wadsworth, Christopher P. (1979). Edimburgo LCF: una lógica mecanizada de la computación . Apuntes de conferencias en Ciencias de la Computación. 78 . Berlín Heidelberg: Springer. doi : 10.1007 / 3-540-09724-4 . ISBN 978-3-540-09724-2.
- Gordon, Michael JC (2000). "De LCF a HOL: una breve historia". Prueba, lenguaje e interacción . Cambridge, MA: MIT Press. págs. 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 la implementación de una máquina (PDF) . Universidad Stanford.
- Milner, Robin (1979). "Lcf: Una forma de hacer pruebas con una máquina". En Bečvář, Jiří (ed.). Fundamentos matemáticos de la informática 1979 . Apuntes de conferencias en Ciencias de la Computación. 74 . Berlín Heidelberg: Springer. págs. 146-159. doi : 10.1007 / 3-540-09526-8_11 . ISBN 978-3-540-09526-2.