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