Glosario
- Asistente de pruebas
- Programa que verifica mecánicamente cada paso de una demostración contra un núcleo lógico pequeño y de confianza. En esta guía se usa Lean 4.
- Cálculo lambda
- Formalismo de la computación basado en la abstracción (λ) y la aplicación de funciones; sustrato de los lenguajes funcionales y de la teoría de tipos.
- Teoría de tipos
- Fundamento alternativo a la teoría de conjuntos en el que todo objeto tiene un tipo; base sobre la que se construyen los asistentes de pruebas modernos.
- Correspondencia de Curry–Howard
- Identificación entre proposiciones y tipos, y entre pruebas y términos (programas). Hace que verificar una prueba se reduzca a comprobar el tipo de un término.
- CoC (Cálculo de Construcciones)
- Sistema de tipos con productos dependientes y polimorfismo de orden superior; vértice del cubo-λ.
- CIC (Cálculo de Construcciones Inductivas)
- El CoC extendido con tipos inductivos. Es el motor formal de Lean: de una declaración por constructores genera constructores, recursor, principio de inducción y reglas de cómputo.
- Tipo inductivo
- Tipo definido enumerando sus constructores; el sistema genera automáticamente su eliminador (recursor) y su principio de inducción.
- Recursor (eliminador)
- Operador, generado con cada tipo inductivo, que define funciones por recursión y, en su forma dependiente, realiza el principio de inducción.
- Deducción natural
- Sistema de demostración con reglas de introducción y eliminación por conectivo, en el que las hipótesis se descargan a lo largo de la derivación.
- Valuación
- Asignación de valores de verdad a las variables proposicionales; determina la semántica clásica de tablas de verdad.
- Tautología
- Fórmula verdadera bajo toda valuación.
- Solidez
- Propiedad de un sistema deductivo: todo lo demostrable es semánticamente válido (Γ ⊢ φ implica Γ ⊨ φ).
- Completitud
- La recíproca de la solidez: todo lo semánticamente válido es demostrable (Γ ⊨ φ implica Γ ⊢ φ).
- Lema de Kalmár
- Resultado constructivo según el cual, a partir de la tabla de verdad de una tautología, se ensambla efectivamente una derivación de ella.
- Recursión bien fundamentada
- Técnica que justifica la terminación de una función probando que una medida decrece en cada llamada recursiva, aun cuando la recursión no sea estructural.
- Auditoría de axiomas
- Comprobación, mediante #print axioms, de los axiomas lógicos de los que depende un teorema formalizado.
- Forma normal
- Término del cálculo lambda sin redexes: no admite más pasos de β-reducción. Es el «resultado» de un cómputo.