cálculo lambda-mu

Ampliación del cálculo lambda

En lógica matemática e informática , el cálculo lambda-mu es una extensión del cálculo lambda introducido por Michel Parigot. ^[1] Introduce dos nuevos operadores: el operador μ (que es completamente diferente tanto del operador μ que se encuentra en la teoría de computabilidad como del operador μ del cálculo modal μ ) y el operador de corchetes. Teóricamente demostrable , proporciona una formulación bien comportada de la deducción natural clásica .

Uno de los principales objetivos de este cálculo extendido es poder describir expresiones correspondientes a teoremas de la lógica clásica . Según el isomorfismo de Curry-Howard , el cálculo lambda por sí solo puede expresar teoremas en lógica intuicionista únicamente, y varios teoremas de lógica clásica no se pueden escribir en absoluto. Sin embargo, con estos nuevos operadores se pueden escribir términos que tengan el tipo, por ejemplo, de la ley de Peirce .

Semánticamente estos operadores corresponden a continuaciones , que se encuentran en algunos lenguajes de programación funcionales .

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:

1. V , una variable , donde V es cualquier identificador .
2. λV.E , una abstracción , donde V es cualquier identificador y E es cualquier expresión lambda.
3. (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 subtérminos arbitrarios, lo que nos permite luego abstraer esos nombres. El conjunto de términos contiene términos sin nombre (todas las expresiones lambda tradicionales son de este tipo) y con nombre . Los términos que se suman mediante el cálculo lambda-mu son de la forma:

1. [α]t es un término con nombre, donde α es una variable μ y t es un término sin nombre.
2. (μ α. 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

${\displaystyle (\lambda x.u)v\;\triangleright _{c}\;u[v/x]}$

reducción estructural

${\displaystyle (\mu \beta .u)v\;\triangleright _{c}\;\mu \beta .u\left[[\beta ](wv)/[\beta ]w\right]}$, donde las sustituciones deben realizarse para todos los subtérminos de la forma . ${\displaystyle u}$ ${\displaystyle [\beta ]w}$

renombrar

${\displaystyle [\alpha ]\mu \beta .u\;\triangleright _{c}\;u[\alpha /\beta ]}$

el equivalente de η-reducción

${\displaystyle \mu \alpha .[\alpha ]u\;\triangleright _{c}\;u}$, para α que 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

• Sistemas clásicos de tipo puro para generalizaciones tipificadas de cálculos lambda con control.

Referencias

1. Michel Parigot (1992). λμ-Cálculo: una interpretación algorítmica de la deducción natural clásica . Apuntes de conferencias sobre informática. vol. 624, págs. 190-201. doi :10.1007/BFb0013061. ISBN 3-540-55727-X.

enlaces externos

• Discusión relevante de Lambda-mu sobre Lambda the Ultimate.