Lógica para funciones computables

Lógica para funciones computables (LCF) es un probador 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 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 prueba de teoremas, tipos de datos algebraicos compatibles, polimorfismo paramétrico, tipos de datos abstractos y excepciones.

Idea básica

Los teoremas en el sistema son términos de un "teorema" especial; tipo de datos abstractos. El mecanismo general de los tipos de datos abstractos de ML asegura que los teoremas se deriven utilizando 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 dichos programas, sino que se deriva de la solidez de la implementación del tipo de datos abstractos y la corrección del compilador 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 Teorema se puede implementar fácilmente para almacenar objetos de prueba opcionalmente, según la configuración de tiempo de ejecución del sistema, por lo que generaliza el enfoque básico de generación de prueba. 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 resultó en un compilador de ML verificado formalmente, lo que alivió 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 los algoritmos de demostración de teoremas, cuya corrección se ha analizado ampliamente. Una forma sencilla de implementar estos procedimientos en un enfoque LCF requiere que dichos procedimientos siempre obtengan 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 usar la reflexión para demostrar que una función que opera en fórmulas siempre da un resultado correcto.

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 llevó a HOL, HOL Light y al asistente de prueba Isabelle que admite varias lógicas. A partir de 2019, el asistente de prueba de Isabelle todavía contiene una implementación de una lógica LCF, Isabelle/LCF.