En lógica matemática e informática , el cálculo lambda-mu es una extensión del cálculo lambda introducido por M. Parigot. [1] Introduce dos nuevos operadores: el operador μ (que es completamente diferente tanto del operador μ que se encuentra en la teoría de la computabilidad como del operador μ del cálculo μ modal ) y el operador de corchetes. En teoría , proporciona una formulación bien educada de la deducción natural clásica .
Uno de los principales objetivos de este cálculo extendido es poder describir expresiones correspondientes a teoremas en lógica clásica . Según el isomorfismo de Curry-Howard , el cálculo lambda por sí solo puede expresar teoremas solo en lógica intuicionista , y varios teoremas lógicos clásicos no pueden escribirse en absoluto. Sin embargo, con estos nuevos operadores se pueden escribir términos que tienen el tipo de, por ejemplo, la ley de Peirce .
Semánticamente, estos operadores corresponden a continuaciones , que se encuentran en algunos lenguajes de programación funcional .
Definicion formal
Podemos aumentar la definición de una expresión lambda para obtener una en el contexto del cálculo lambda-mu. Las tres expresiones principales que se encuentran en el cálculo lambda son las siguientes:
- V , una variable , donde V es cualquier identificador .
- λV.E , una abstracción , donde V es cualquier identificador y E es cualquier expresión lambda.
- (EE ′) , una aplicación , donde E y E ' ; son expresiones lambda.
Para más detalles, consulte el artículo correspondiente .
Además de las variables λ tradicionales, el cálculo lambda-mu incluye un conjunto distinto de variables μ. Estas variables μ se pueden usar para nombrar o congelar subterráneos arbitrarios, permitiéndonos luego abstraer esos nombres. El conjunto de términos contiene términos sin nombre (todas las expresiones lambda tradicionales son de este tipo) y términos con nombre . Los términos que se agregan mediante el cálculo lambda-mu son de la forma:
- [α] t es un término con nombre, donde α es una variable μ y t es un término sin nombre.
- (μ α. E) es un término sin nombre, donde α es una variable μ y E es un término con nombre.
Reducción
Las reglas básicas de reducción utilizadas en el cálculo lambda-mu son las siguientes:
- reducción lógica
- reducción estructural
- renombrar
- el equivalente de η-reducción
- , para α no ocurre libremente en u
Estas reglas hacen que el cálculo sea confluente . Se podrían agregar más reglas de reducción para proporcionarnos una noción más sólida de forma normal, aunque esto sería a expensas de la confluencia.
Ver también
Referencias
- ^ Michel Parigot (1992). "Λμ-Cálculo: una interpretación algorítmica de la deducción natural clásica". λμ-Calculus: Una interpretación algorítmica de la deducción natural clásica . Apuntes de conferencias en informática. 624 . págs. 190–201. doi : 10.1007 / BFb0013061 . ISBN 3-540-55727-X.
enlaces externos
- Discusión relevante sobre Lambda-mu sobre Lambda the Ultimate.