Resumen

  • Una táctica de Edinburgh LCF proponía subobjetivos y devolvía una validación. El resultado solo adquiría forma de teorema cuando esa validación recomponía teoremas aceptados mediante las reglas primitivas.
  • El tipo abstracto thm reducía el código con autoridad directa para construir teoremas; no demostraba que la lógica fuera consistente, la especificación fiel ni el compilador, el entorno de ejecución y el hardware infalibles.
  • El desarrollo fue colectivo: la lógica provenía de Dana Scott; Stanford LCF llegó antes; Michael Gordon, Christopher Wadsworth, Lockwood Morris, Malcolm Newey y una comunidad más amplia contribuyeron al sistema y a ML.

Buscar no equivale a aceptar

Una demostración interactiva suele avanzar hacia atrás. Se parte de una meta y una táctica sugiere condiciones más pequeñas que, si llegan a demostrarse, bastarían para resolverla. El recorrido puede incluir reescritura, elección, repetición y retroceso. Nada impide que ese software se equivoque.

LCF no intentó convertir toda esa búsqueda en código incuestionable. La táctica entregaba también una validación: una función que esperaba los teoremas correspondientes a los subobjetivos y debía construir con ellos el teorema original. La búsqueda terminaba de verdad cuando esa función podía recorrer el camino hacia delante usando la interfaz protegida.

Así, borrar un objetivo de la pantalla no era suficiente. Una táctica que devolviera una lista vacía de subobjetivos aún necesitaba una validación capaz de producir el teorema sin premisas ficticias. Si la validación estaba mal, el proceso fallaba. La táctica no recibía por ello un constructor alternativo.

La decisión arquitectónica fue encapsular los teoremas en un tipo abstracto, habitualmente thm. Los axiomas y reglas primitivas eran las funciones autorizadas para producir valores de ese tipo. El resto del programa podía combinar tácticas y manipular metas, pero la abstracción de tipos impedía fabricar directamente la representación privada de un teorema.

De Stanford a Edimburgo, con varios autores

Milner documentó en 1972 un comprobador implementado para la Logic for Computable Functions de Dana Scott. Aquella experiencia en Stanford mostró el valor de la mecanización y también sus límites prácticos: las pruebas largas eran tediosas y costosas de conservar. El trabajo en Edimburgo, desde 1973, buscó un sistema programable.

La genealogía no admite una atribución individual simplista. El libro Edinburgh LCF de 1979 tiene como autores a Michael J. C. Gordon, Robin Milner y Christopher P. Wadsworth. El artículo de 1978 sobre el metalenguaje incluye además a Lockwood Morris y Malcolm Newey. Las historias de Larry Paulson y Michael Gordon explican la transición posterior hacia Cambridge LCF, HOL e Isabelle.

ML nació como “Meta Language” para escribir procedimientos de prueba. Su tipado polimórfico se convirtió después en una contribución independiente; el trabajo de Milner de 1978 presentó resultados de solidez semántica y sintáctica y un algoritmo de inferencia ya utilizado en Edinburgh LCF. El premio Turing de 1991 reconoció el peso de LCF, ML y CCS en la obra de Milner, sin convertir por ello la historia de cada tecnología en obra de una sola persona.

Las reglas primitivas avanzaban desde teoremas previos hasta uno nuevo. Las tácticas retrocedían desde una meta hasta subobjetivos. Las validaciones unían ambas direcciones. Los “tacticals” componían tácticas por secuencia, repetición o alternativas; ampliaban el lenguaje de búsqueda, no el catálogo de axiomas.

Un núcleo pequeño sigue teniendo supuestos

La ventaja del tipo abstracto era concentrar la revisión. Los desarrolladores podían añadir automatización sin añadir, a la vez, nuevas formas directas de crear teoremas. El volumen de código inteligente podía crecer fuera de la frontera de aceptación.

Pero la reducción de superficie no elimina la confianza. Las reglas primitivas deben ser correctas para la lógica elegida. La implementación de ML, el compilador y el entorno deben preservar la abstracción. Las funciones inseguras o un fallo de hardware pueden romperla. Un analizador o impresor incorrecto puede mostrar al usuario una fórmula distinta de la almacenada. El núcleo es una raíz de confianza más estrecha, no una demostración de todo el sistema informático.

También conviene separar solidez y consistencia. Decir que un valor solo se construye con ciertas funciones describe su procedencia. No demuestra por sí solo que las funciones representen inferencias válidas. Tampoco un teorema sobre un modelo demuestra que el modelo refleje fielmente una planta industrial, una norma o una intención humana. La verificación responde a la pregunta formal que recibió; no corrige una pregunta mal formulada.

La validación como recibo de construcción

La validación puede entenderse como una obligación aplazada. Cuando una táctica propone subobjetivos, promete que los teoremas de esos subobjetivos bastarán para el objetivo inicial. Más tarde debe cumplir esa promesa mediante las reglas aceptadas.

Los tacticals mantienen la obligación mientras combinan búsquedas. Una secuencia aplica una táctica y luego otra; una repetición continúa mientras haya progreso. Al mismo tiempo se componen las validaciones. Por eso un control sofisticado no borra el camino hasta las reglas primitivas.

La lección no es que un registro de actividad carezca de valor. Es que el registro, el guion y la señal verde no poseen la misma autoridad que el objeto admitido. LCF separó evidencia de actividad y poder de aceptación.

HOL, Isabelle y otros descendientes heredaron partes de esta idea, pero no forman una arquitectura uniforme. Paulson explica que Isabelle representa reglas y estados de prueba con principios distintos de los de LCF clásico. Otros sistemas conservan términos de prueba o exportan certificados. Coq y los asistentes basados en teoría de tipos tienen fronteras diferentes. Usar tácticas no basta para identificar un núcleo LCF.

Fuentes y límites

Este texto es historia y análisis arquitectónico, no una auditoría de un demostrador actual ni una medición de líneas de código. La lectura según la cual una regla común puede ser mínima y verificable mientras la búsqueda futura permanece abierta se inspira editorialmente en el principio de especificación inicial mínima de Lu Heng; no se atribuye a Milner como postura institucional.