El clculo lambda de Alonso Church y la nocin de computabilidad
El clculo lambda, pensado originalmente para facilitar la fundamentacin de la aritmtica, es
una notacin especial para representar funciones. Antes de que Church hiciera su presentacin,
ya varios lgicos venan emprendiendo investigaciones que iban conduciendo a resultados
similares.
Schnfinkel (1924) desarroll una teora de funciones con el objeto de reducir el nmero de
primitivas en un sistema lgico como el presentado por Russell y Whitehead (1910 - 1913). En el
sistema de Schnfinkel, que llam Funktionenkalkl (clculo de funciones, en espaol), slo hay
una operacin para formar trminos complejos, que se escribe fx, representa la aplicacin de
una funcin f a un argumento x, y se define para todos los trminos. Para trabajar con funciones
de ms de un argumento, Schnfinkel emple un mtodo ya usado por Frege (1891), para reducir
funciones de ms de un argumento a funciones de un argumento. Este mtodo supone ampliar la
idea de funcin para que las funciones puedan ser argumentos y valores de otras. Entonces, es
posible pasar el valor de cada funcin g para algn argumento x, como argumento a otra funcin
f. Para esto, se usa una notacin donde es comn escribir fxyz para ((fx)y)z. Si Fxy es una
funcin F de dos argumentos x e y, se reemplaza por una funcin f de un argumento tal que fa es
la funcin de y dada por Fay, y fab es Fab. Por ejemplo, si Fxy es x y, entonces f 2 = 2 y, y f
2 3 = 2 3 = 1. Esta operacin que permite eliminar funciones de diverso nmero de variables
se llama aplicacin. Schnfinkel introdujo varios operadores para representar la aplicacin de
una funcin a sus argumentos y los llam combinadores, porque forman combinaciones como
funciones de las variables que contienen. Schnfinkel introdujo cinco combinadores: I, C, T, Z, S
(que luego fueron formulados en la lgica combinatoria de Curry (1967) como respectivamente:
I, K, C, B, S) y mostr que las frmulas lgicas podan expresarse sin variables por medio de S
y K (S y K en el sistema de Curry).
A finales de la dcada de 1920, Haskell B. Curry, como l mismo lo comenta en Curry (1967,
pags. 20 21), realiz investigaciones que lo llevaron a lo que en esencia sera el mismo sistema
de Schnfinkel: leyendo los Principia de Whitehead y Russell, not que en la lgica
proposicional haban dos reglas, el modus ponens, que era muy simple en su estructura formal, y
una regla de sustitucin de cualquier frmula por una variable proposicional, que era compleja.
Seldin (1998a) afirma que a mediados de 1920, Curry decidi tratar de dividir esta regla de
sustitucin en reglas ms simples y, luego, en 1926 encontr que poda hacerlo con un
formalismo que en esencia era el mismo que el de Schnfinkel, y lo llam lgica combinatoria.
Al mtodo de tratar funciones de ms de un argumento en trminos de funciones de un
argumento, usado por Frege y que Curry tom de Schnfinkel, se le llam
curryng (currificacin), en honor al trabajo realizado por Curry.
De forma independiente y casi simultneamente al trabajo de Curry, Alonzo Church se propuso
construir una modificacin del sistema de Frege en la que se evitara el uso de variables libres.
Segn Seldin (1998a), una de sus metas fue que toda combinacin de smbolos perteneciente a
nuestro sistema, si representa una proposicin, representara tambin una proposicin particular
sin ambigedad y sin la adicin de explicaciones verbales. Tambin propuso evitar paradojas de
la teora de conjuntos y de la lgica restringiendo la ley del tercero excluido, siguiendo en esta
restriccin a la tendencia intuicionista de Brouwer. Church adopt el tratamiento de funciones de
Frege, que ya hemos mencionado, como la estrategia de formacin bsica de este sistema, en el
sentido de que los trminos fueran formados a partir de variables usando dos operaciones:
(1) Aplicacin: denotada por MN, como en los trabajos de Schnfinkel y Curry, que
representa la aplicacin de una funcin M a un argumento N y que est definida para
cualesquiera dos trminos M y N
(2) Abstraccin: denotada por x.M y definida en el sistema original de Church para cualquier trmino M y para cualquier variable x que aparezca libre en M.
El sistema de Church tambin contena la implicacin. Las reglas de inferencia de Church eran
dos: la regla y la regla . La regla permita la sustitucin de variables: los trminos que difieren slo en los nombres de sus variables ligadas estn identificados en el nivel sintctico, de
manera que:
x.x = y.y.Las variables ligadas son aquellas sobre las que acta el operador ; por ejemplo, en x.xy, x es una variable ligada e y una variable libre. La regla era empleada para el clculo de valores de una funcin:
(x.M)N puede ser reemplazada por el resultado de sustituir x por N en M.
Como en Curry, en el sistema de Church las conectivas lgicas pueden ser reemplazadas por
constantes atmicas.
Como resultado de la definicin de las operaciones de aplicacin y abstraccin, tenemos que la
teora de Church tambin tena combinadores y, por tanto, coincida en muchos aspectos con las
investigaciones de Schnfinkel y Curry. La relacin exacta entre las teoras de Curry y la de
Church qued establecida por Rosser (1935), un discpulo de Church, en su trabajo de tesis, A
Mathematical Logic without variables. Para establecer esta relacin, Rosser construy una teora
de combinadores que era equivalente a la de Church. Luego mostr que una teora reforzada de
la conversin lambda, que es el proceso de transformar frmulas del sistema de Church por la
aplicacin de sus reglas de inferencia, es equivalente a la teora sinttica de Curry. Desde
entonces qued claro que una teora de combinadores puede ser expresada como una teora de la
conversin lambda y viceversa, como ratifica Curry (1967, pag. 28). Podemos coincidir entonces
con Feys y Fitch (1980, pag. 90) cuando afirman que el clculo lambda pertenece a la lgica
combinatoria, entendida sta como el estudio de los procesos de aplicacin y de abstraccin de
funciones.
Church (1936) demostr luego, basndose en un teorema sobre las propiedades del clculo
lambda, que siempre que consideremos un sistema equivalente a la lgica de predicados de
primer orden, tomado en su totalidad, es imposible resolver el problema de la decisin. Como
resultado de un trabajo de representacin de la aritmtica en el sistema original de Church,
Kleene (1936), discpulo de Church, descubri una gran cantidad funciones que pueden ser
representadas por trminos lambda. Puesto que un trmino lambda que representa una funcin
calcula sus valores usando un procedimiento mecnico (reduccin aplicando la regla ), cualquier funcin que pueda ser representada por un trmino lambda debera ser efectivamente
calculable, es decir, calculable siguiendo un procedimiento mecnico. Estos resultados llevaron
a Church a la conjetura de que las funciones efectivamente computables de nmeros naturales
pueden ser representadas por trminos lambda. Esta conjetura es el origen de la famosa Tesis de
Church, publicada en Church (1936) en el marco de su demostracin de que hay problemas
irresolubles de la teora elemental de nmeros. La forma ms usual de esta tesis es que todas las
funciones efectivamente computables son recursivas parciales, y es una consecuencia de una
prueba en Kleene (1936) de que una funcin es recursiva si, y slo si, puede ser representada por
un trmino lambda.
Para su demostracin, Church (1936) plantea el problema de la decisin en trminos del
problema de los invariantes de conversin, que grosso modo puede ser planteado de la siguiente
manera: dadas dos frmulas cualesquiera Y1 e Y2 de un sistema como el clculo lambda es
posible determinar de manera efectiva si Y1 se puede convertir Y2 o no? La respuesta positiva a
esta cuestin nos dara un procedimiento efectivo para determinar un sistema completo de
invariantes de conversin, es decir, un sistema de frmulas que permanecen invariantes respecto
de toda conversin. Sin embargo, Church concluye que no existe un sistema completo de
invariantes de conversin que sea efectivamente calculable. Para ello comienza aplicando el
mtodo de aritmetizacin de Gdel (1931) al clculo de conversin lambda. Este mtodo permite
realizar una codificacin que asocia a cada frmula bien construida de un sistema formal un
nmero, llamado nmero de Gdel, de manera tal que dos expresiones bien formadas no pueden
tener asociado el mismo nmero. Luego identifica la nocin de calculabilidad efectiva con la
nocin de funcin recursiva general:
[] esta definicin de calculabilidad efectiva puede ser establecida en dos maneras
equivalentes, (1) que una funcin de enteros positivos ser efectivamente calculable si es
definible en el clculo lambda [], (2) que una funcin de enteros positivos ser llamada
calculable efectivamente si es recursiva (Church, 1936, pag. 347).
Al hacer equivalentes las funciones calculables efectivamente con las funciones recursivas,
Church podr vincular la recursin con el problema de la decisin: para cualquier funcin
recursiva de enteros positivos hay un algoritmo con el cual cualquier valor particular requerido
de la funcin puede calcularse efectivamente (Church, 1936, pag. 351). Define algoritmo como:
un mtodo por el cual, dado cualquier nmero entero n, puede obtenerse una secuencia de
expresiones (en alguna notacin) En1, En2, Enr; donde En1 es efectivamente calculable
cuando se da n; donde Eni es efectivamente calculable cuando se dan n y las expresiones
Enj , j < i; y donde, cuando se dan n y todas las expresiones Eni hasta incluir Enr, el hecho
de que el algoritmo haya terminado llega a conocerse efectivamente y el valor de F(n) es
calculable efectivamente (Church, 1936, pag. 356).
Church (1936, pag. 351) define una funcin recursiva proposicional de enteros como una
funcin recursiva cuyo valor es 2 o 1 dependiendo de si la funcin proposicional es verdadera o
falsa. Entonces plantea el problema siguiente: hallar una funcin recursiva F de dos argumentos
tal que de F Y1 Y2 (donde Y1 Y2 son los nmeros de Gdel correspondientes a los trminos Y1 e
Y2 respectivamente) sea 2 o 1 segn que Y1 sea convertible en Y2 o no. Este problema es
equivalente al de encontrar una funcin recursiva G de un argumento que dependa del nmero de
Gdel de una frmula Y3, tal que el valor de G Y3 sea 2 o 1 segn que Y3 tenga una frmula
normal o no. Una frmula del clculo lambda tiene forma normal si es una frmula bien formada
y no contiene ninguna parte de la forma x(M)N y B es la forma normal de A si B est en forma normal y A es convertible en el clculo lambda a B. Cuando un trmino est en forma normal, no
se le puede aplicar la reduccin .
Finalmente Church demuestra el teorema siguiente, el teorema XIII del artculo:
Dada una frmula Y1, no existe funcin recursiva G de un argumento tal que el valor de
G Y1 sea 2 o 1, segn que Y1 tenga una forma normal (Church, 1936, pag. 360).
Es decir, la propiedad de ser una frmula en forma normal no es recursiva. De lo que se sigue el
teorema XIX del artculo:
No hay funcin recursiva de dos frmulas Y1 e Y2, cuyo valor es 2 o 1 de acuerdo a si Y1
es convertible en Y2 (Church, 1936, pag. 363)
Como corolario a este teorema, Church establece que el Entscheidungproblem es irresoluble en
un sistema formal que sea -coherente1 en sentido fuerte y que permita ciertos procedimientos simples de definicin y demostracin, como el sistema de Principia Mathematica:
En un sistema como ste, sera expresable la proposicin acerca de dos enteros positivos
a y b que son representaciones gdelianas (nmeros de Gdel) de frmulas A y B tal que
A es inmediatamente convertible en B. Ya que la conversin en el clculo lambda es una
secuencia finita de conversiones intermedias inmediatas, la proposicin (a, b) expresara que a y b son representaciones gdelianas de frmulas A y B tal que A es
convertible en B. Adems si A es convertible en B y a y b son representaciones
gdelianas de frmulas A y B respectivamente, la proposicin (a, b) podr ser demostrada en el sistema, a travs de una prueba que afirma exhibir, en trminos de
representaciones gdelianas, una secuencia finita particular de conversiones inmediatas
1 Supongamos que n es una variable sintctica para expresiones de n-simo tipo y expresiones correspondientes a propiedades del n-simo tipo; es una variable sintctica para variables individuales; K es una variable para proposiciones indecididibles cuya existencia es demostrada gracias a la teora de predicados de Kleene. Un sistema formal L de segundo orden que incluye constantes individuales que corresponden a enteros, es -coherente en sentido fuerte si para todo predicado 2 [predicado de orden 2] de L se da que: si las proposiciones (E ) 2 () [Existe algn individuo , tal que tiene la propiedad de segundo tipo ] es derivable en L, al menos una de las proposiciones ~ 2K [El predicado de segundo tipo indecidible en el sistema de Kleene] no es derivable en L.
que conduce de A a B; y si A no es convertible en B, la -consistencia del sistema significar que (a, b) no es demostrable en l. Si el problema de la decisin para el sistema fuera resoluble, habra medios para determinar efectivamente si cualquier
proposicin (a, b) se puede demostrar y, por lo tanto, habra algn medio para determinar efectivamente para todo par de frmulas A y B si A es convertible en B, lo que
estara en contradiccin con el teorema XIX 2 (Church 1936, pag. 363).
De esta manera Church prueba que hay clases de la forma P(n) para cada nmero natural n tal
que no hay un algoritmo general que, dado n, produzca una solucin para P(n). No hay pues
algoritmo que decida si una formula dada del clculo de predicados de primer orden es un
teorema, un resultado que coincide con los de Turing (1936).
Ya hemos comentado que Turing (1937), demostr que una funcin numrica puede ser
computada por una mquina de Turing si y slo si es recursiva parcial. Tambin Turing demostr
que las funciones computables por una mquina de Turing son idnticas a las funciones lambda-
definibles de Church y a las funciones recursivas generales debidas a Herbrand y Gdel y
desarrolladas por Kleene. Estos resultados le permitieron a Turing (1937) afirmar la posibilidad
de reemplazar las 'mquinas' que generan funciones computables por definiciones ms
convenientes en el clculo lambda. Podemos entonces pensar que la definibilidad lambda
representa una manera particular de definir la computabilidad que, como hemos visto, tiene un
fundamento an ms abstracto que el de Turing: una operacin matemtica precisamente
llamada abstraccin.
2 El teorema XIX, que ya hemos citado arriba, dice textualmente: No hay funcin recursiva de dos frmulas A y B cuyo valor es 2 o 1 de acuerdo a si A es convertibe en B o no. Dado que una funcin recursiva suministra un procedimiento efectivo, este teorema plantea que no es posible dar un procedimiento efectivo para decidir si una frmula A es convertible en otra B.
Maquinas de Turing y clculo lambda
Turing y Church, casi simultneamente e independientemente uno de otro, demostraron que
cualquier operacin computable por una mquina de Turing puede expresarse usando
expresiones del clculo lambda de Church, y viceversa.
Kleene (1936) lleg a los siguientes resultados:
1. Toda funcin recursiva primitiva es recursivamente general.
2. Toda funcin recursiva general es lambda-definible
3. Toda funcin lambda-definible, definida para todos los sistemas de sus valores de sus
argumentos, es recursiva general.
Basado en teorema de Kleene (1938) sobre recursividad parcial, Church enunci la tesis
siguiente:
Toda funcin parcialmente recursiva es lambda-definible y viceversa.
Turing (1937) estableci
1. Toda funcin lambda-definible es computable.
2. Toda funcin computable es recursiva general.
Por consiguiente, las siguientes nociones son equivalentes:
(a) Funcin recursiva general.
(b) Funcin computable.
(c) Funcin lambda-definible, para todos los sistemas de valores de sus argumentos.
Tambin se da la equivalencia entre:
(a) Funcin parcialmente recursiva.
(b) Funcin lambda-definible (sin restriccin).
De acuerdo a la tesis de Church, la clase de las funciones recursivas parciales pueden ser
computadas por cualquier dispositivo que ejecute procesos algortmicos. Las funciones
computables por mquinas de Turing son iguales a las funciones recursivas parciales. Si una
mquina de Turing no puede resolver un problema, entonces ningn dispositivo mecnico de
cmputo puede hacerlo, porque no existe ningn algoritmo ni procedimiento para obtener su
solucin. Las limitaciones de indecidibilidad para el cmputo de funciones no son de orden
tecnolgico, sino intrnsecas a limitaciones esenciales de los procesos computacionales. No
importa cun poderosa sea una computadora en cuanto a memoria y velocidad de ejecucin de
sus operaciones, no existe la posibilidad ni el procedimiento para computar ciertas clases de
funciones.
Reglas del clculo lambda
El clculo lambda es un formalismo para expresar funciones. Trabaja con un conjunto de
smbolos cada uno de los cuales representa una operacin matemtica o funcin, cuyos
argumentos son otras cosas del mismo tipo, es decir, funciones. Una funcin al actuar sobre
otra, da como resultado una nueva funcin. Por ejemplo, al escribir:
a = bc
decimos que a es el resultado de hacer que la funcin b acte sobre la funcin c. A la accin de
una funcin sobre sus argumentos la llamamos aplicacin.
Adems de la aplicacin, Church propuso otro tipo de operacin: la abstraccin, designada por
la letra griega . Para expresar la abstraccin de una funcin, se coloca la letra y se le hace seguir inmediatamente por la letra que representa una de las funciones, por ejemplo x, que
llamamos variable muda; luego seguir un punto y despus una expresin, donde cada
aparicin de la variable x se tratar como un espacio (placeholder) en el que puede sustituirse
cualquier cosa que siga a la expresin completa. Podemos entonces escribir:
x.fxpara expresar la funcin que, al actuar sobre un objeto, como a, produce como resultado fa:
(x.fx)a = fa.
Podramos decir que la abstraccin es una operacin para nombrar de forma precisa una funcin
en s misma. Entendiendo funcin como una correspondencia por la que a cada elemento x de un
conjunto X se hace corresponder un nico elemento y de un conjunto Y, encontramos dos
significados para la expresin de funciones f(x):
1. La funcin misma, en tanto que la correspondencia entre los elementos de un
conjunto X y los elementos de un conjunto Y.
2. El valor de la funcin: un miembro y del conjunto Y, cuando x es un objeto de un
dominio X, o un valor ambiguo de la funcin, si no est especificado el valor de x.
Mediante la notacin para la abstraccin lambda, se puede representar la funcin f como distinta
de su valor ambiguo. En este sentido, la expresin x.fx, es simplemente un nombre para la funcin f:
x.fx = f.
Vemos que cuando se aplica el operador lambda a una forma funcional como fx, se asla la
funcin de sus argumentos, dando como resultado el nombre de la funcin asociada a la forma.
Tenemos entonces que mientras una expresin como (x + 1) designa el sucesor de x, en cambio
la expresin x (x +1) designa la funcin sucesor en s misma.
Llamamos conversin lambda a una serie finita de aplicaciones de las operaciones del clculo
lambda, que son aplicacin y abstraccin. Si una frmula Y puede obtenerse por conversin, a
partir de otra frmula Z, decimos que Y es convertible en Z. La convertibilidad es una relacin
simtrica, reflexiva y transitiva, y el clculo lambda se dedica al estudio de las propiedades de la
conversin lambda.
Una expresin est expresada en forma normal si est bien construida y no contiene ninguna
parte de la forma (x.Y)Z, donde las variables ligadas de Y son distintas de las variables ligadas de Z. En una expresin en forma normal no es posible aplicar a ninguna de sus partes la
operacin de reduccin.
Las funciones de nmeros enteros que se pueden representar mediante el clculo lambda se
denominan funciones lambda-definibles:
Una funcin de enteros f de una variable es lambda-definible si se puede encontrar una
frmula Y del clculo lambda tal que si fa = b y si a y b son las frmulas del clculo
lambda que representan los enteros a y b, respectivamente, la expresin lambda Ya es
convertible en b.
El clculo de la conversin lambda est en correspondencia con el clculo de valores de una
funcin segn el esquema:
fa clculo bYa conversin b
Hay, pues, como lo presenta (Ladrire, 1965, pag. 205), una correspondencia donde la frmula Y
del clculo lambda corresponde a una funcin de enteros f, la frmula a del clculo lambda
corresponde al entero a, y las expresiones lambda Ya o b corresponden a las expresiones fa o b
de la aritmtica.
1. Alfabeto del clculo lambda
El alfabeto del clculo lambda est constituido por:
Smbolo para la operacin de abstraccin: .Smbolos para variables: a, b, c, , z y las mismas letras con ndices, por ejemplo: a0,
a1, ...
Smbolos auxiliaries:
De agrupacin: parntesis: ), (.
De separacin: ..
2. Convenciones para variables y trminos:
Los trminos del clculo lambda se llaman trminos lambda;
M, N,... son smbolos sintcticos para trminos lambda; en todo caso M, N, son
expresiones del metalenguaje para referir trminos cualesquiera;
x, y, z,... son smbolos sintcticos para variables lambda arbitrarias.
= es un smbolo del metalenguaje denota igualdad sintctica.
M N denota que M y N son el mismo trmino o que N puede ser obtenido a partir de M
mediante un cambio de nombre en las variables ligadas en M.
3. Reglas de formacin
Los trminos lambda son definidos inductivamente:
Toda variable es un trmino.
Si M, N son trminos, entonces MN tambin lo es,
Si M es un trmino y x una variable, entonces x.M es un trmino.
4. Convenciones de asociacin
Asociacin a la izquierda: M1 M2 M3 ... Mn se reserva para ((...(M1 M2) M3) ... Mn) ;
Asociacin a la derecha: x1, x2,...xn.[M] se reserva para x1 (x2 (...(xn M))...).
5. Variables libres
Intuitivamente, una variable aparece libre en un trmino M si x no est en el alcance de
x; si es de otra manera, x aparece ligada. El conjunto de variables libres de un trmino lambda M, que expresaremos con la notacin FV (M), que significa Free Variables of
M o variables libres de M, se define inductivamente por las siguientes reglas,
expuestas en Barendregt y Barendsen (2000, pag. 10):
FV (x) = {x};
FV (MN) = FV(M) FV(N);
FV (x. M) = FV(M) {x}.M es un trmino lambda cerrado o combinador si FV (M) = conjunto vaco.
6. Reglas de transformacin
Regla de sustitucin o regla alfa =
Los trminos que difieren slo en los nombres de sus variables ligadas estn identificados
en el nivel sintctico, as que:
x. M = y. [y/x]M.donde [y/x] indica la sustitucin de x por y. Este cambio de nombre, que expresamos por
el smbolo =, es lo que llamamos conversin alfa. Esta regla tiene la restriccin de
que y no puede aparecer libre en M, pues entonces la y que aparece libre en M resultara
ligada una vez hecha la sustitucin. Por ejemplo si M fuera xy, tendramos:
x. xy = y. yylo que nos dara una expresin cuyos dos lados no tienen el mismo sentido. A este
fenmeno se le llama colisin de variables.
Regla de reduccin o regla beta Toda expresin que representa una aplicacin, que tiene la forma (x. f x) M, puede ser
reemplazada o reducida a la frmula f M:
(x. f x) M f MA esta transformacin se le conoce como reduccin beta () y la expresaremos usando el smbolo
.
Regla de expansin o abstraccin beta M [x/N] denota el resultado de sustituir toda aparicin libre de la variable x en M por el
trmino N. Una expresin de la forma M [x/N] puede ser reemplazada por una frmula
con la forma (x.M) N, siempre que las variables ligadas de Y sean distintas de x y de las variables de N:
M [x/N] (x. M) NUsaremos el smbolo para representar la expansin beta.
Representaremos tanto la reduccin beta como la expansin o abstraccin beta por el
smbolo = que significar lo que llamaremos conversin beta.
Conversin lambda
Se denomina conversin lambda a una serie finita de aplicaciones de estas tres reglas:
conversin , reduccin y abstraccin . Si una frmula puede obtenerse por conversin lambda, decimos que esa frmula es lambda convertible . Expresaremos la
convertibilidad en el clculo lambda usando el smbolo ; entonces la expresin:
M N
significa M es convertible a N por aplicacin de las reglas de conversin del clculo
lambda.
3.4.7. Forma Normal en el Clculo Lambda
Una frmula est expresada en forma normal si est construida de acuerdo a las reglas de
formacin del clculo y no contiene ninguna forma del tipo (x. M) N, siendo las
variables ligadas de M distintas de las variables de N. Esto significa que una frmula
est en forma normal si no es posible aplicarle la regla de reduccin beta.
El resultado de sustituir N por las apariciones libres de x en M que, como dijimos al
explicar la regla de expansin, se expresa por la notacin M [x / N], se define por los
siguientes esquemas, tomados de Barendregt (2000, pag 10):
x [x / N] = N;
y [x / N] = y, si x y;
M1 M2 [x / N] = (M1 [x / N]) (M2 [x / N]);
(y. M1) [x / N] = y. (M1 [x / N]).
3.4.8. Caracterizacin de la conversin lambda
Si asumimos aqu la convencin de usar el smbolo para significar implica,
podemos caracterizar la conversin lambda por los siguientes esquemas axiomticos y
reglas:
() x. M = y. [y/x]M (Conversin alfa)() (x. M)N M [x / N] (Reduccin beta) () M M (Reflexividad)()M N N M (Simetra) () M N, N L M L (Transitividad)() M N ZM ZN (Monotona de la aplicacin 1)() M N MZ NZ (Monotona de la aplicacin 2)() M N x.M x.N (Monotona de la abstraccin)
Barendregt y Barendsen (2000) llaman a las reglas , y reglas de igualdad y a las reglas , y reglas de compatibilidad. Como puede observarse, la convertibilidad lambda , que es una generalizacin de la conversin alfa, la reduccin beta y la expansin beta, es una relacin
de equivalencia, pues satisface las propiedades reflexiva, simtrica y transitiva.
Combinadores
Ya hemos visto que Schfinkel (1924), interesado en eliminar variables de la lgica, introdujo un
tipo de operadores llamados combinadores, los cuales representan combinaciones como
funciones de las variables que contienen (tal vez junto con otras variables) (Curry y Feys, 1967,
pag. 24). Tales combinaciones se forman a partir de las variables y por medio de una operacin
postulada en correspondencia a la aplicacin de una funcin a un argumento. El siguiente lema
(&), tomado de Barendregt (2000, pag. 1) permite representar combinadores por letras simples:
en el clculo lambda podemos demostrar
(x1, , xn. M) y1 yn M [x1 / y1] [xn / yn]. (&)
Prueba:
Por el axioma 1, la reduccin beta, tenemos:
(x1. M) y1 M [x1 / y1]
Entonces el lema (&) se sigue por induccin sobre n.
Si definimos los siguientes combinadores [Barendregt, 12]:
I x. x;
K xy. x;
K* xy. y;
S xyz.xz(y z).
Como puede observarse, a cada combinador simple hay asociada una regla de reduccin. Esto
significa que cuando el combinador es aplicado a una serie finita de variables obtenemos una
combinacin que se reduce a una determinada combinacin de tales variables. Tal reduccin se
seguir del lema (&):
I M M;
K MN M;
K* M N N;
S M N L M L (N L).
Tenemos aqu que I es el operador ms sencillo, el cual expresa una variable como funcin de s
misma. A este combinador se llama identificador elemental. El combinador K expresa un
trmino M como funcin de N, mientras que K* expresa un trmino N como funcin de M. A
estos dos combinadores se les llama canceladores elementales. El combinador S permite
expresar dos trminos M y N (que podran ser dos funciones f y g) que dependen de un mismo
trmino L (que podra ser una variable x). Schfinkel (1924) demostr que las frmulas lgicas
pueden expresarse sin variables por medio de S y K.
Teoremas Church Rosser
Los teoremas de Church y Rosser (1936) demuestran la consistencia del clculo lambda . El
siguiente teorema, conocido como el teorema ChurchRosser I, responde de forma afirmativa a
la cuestin de si hay ms de una estrategia de reduccin que conduzcan a la misma forma
normal:
Para cualquier expresiones lambda E, F y G, si E F y F G, hay una expresin lambda Z tal que F Z y G Z (Slonneger, 1995, pag. 153).
Corolario: Para cualquier expresiones lambda E, M, y N, si E N, estando M y N en forma normal, M y N son variantes una de otra. Esto significa que M y N seran equivalentes por
reduccin alfa.
El siguiente teorema, llamado teorema Church Rosser II, responde a la pregunta de si hay una
estrategia de reduccin que garantice que se produzca una expresin en forma normal?
Para cualquier expresiones lambda E y N, si E N, estando N en forma normal, hay un orden normal de reduccin de E a N (Slonneger, 1995, pag. 154).
El orden normal de reduccin siempre reduce primero la primera frmula beta-reducible que
est en el extremo izquierdo (Slonneger, 1995, pag. 152). El orden normal de reduccin puede
tener una de los siguientes resultados:
1. Alcanza una sola expresin en forma normal.
2. Nunca termina.
Como slo existe una forma normal nica para una reduccin que conduzca a una forma normal,
el clculo lambda es consistente. Sin embargo, no hay algoritmo o procedimiento mecnico para
determinar si alguna expresin lambda va a producir algunos de los dos resultados mencionados
(Slonneger, 1995, pag. 154).
Aplicaciones del clculo lambda
Hemos comentado que el clculo lambda fue pensado originalmente para una formalizacin de
la aritmtica. En esta aplicacin, el clculo lambda no result satisfactorio, pues el sistema que
Church ide para tales efectos demostr ser inconsistente. Sin embargo, como expusimos antes,
Church aplic el clculo lambda con xito en una definicin de procedimiento efectivo que ha
demostrado ser equivalente a otras definiciones de computabilidad: es posible usar el clculo
lambda como un formalismo para representar funciones de nmeros enteros, es posible. De
hecho, se llaman funciones lambda-definibles a las funciones de nmeros enteros que se pueden
representar en el clculo lambda.
La tesis de Church, segn la cual las funciones efectivamente computables sobre enteros
positivos son las funciones lambda definibles, supone que en el clculo lambda hay una manera
de definir enteros positivos. Tal definicin sera una definicin computacional o algortmica de
estos objetos. La definicin de los enteros positivos a travs del clculo lambda se conoce como
numerales de Church.
1. Numerales de Church
Recordemos que en el clculo lambda estamos interesados en un universo de objetos denotados
por variables, cada uno de los cuales representa una operacin matemtica o funcin. En este
clculo podemos formar expresiones a partir de las operaciones elementales del sistema,
aplicacin y abstraccin. Por ejemplo, la expresin:
f. f(fx),
es la funcin que, cuando se aplica a una funcin g, produce g aplicada dos veces sobre x:
(f. f(fx) g g (gx)
Tambin podemos aplicar la expansin lambda o abstraccin a f. f(fx) y obtener:
(f. f(fx) f. x. f(fx) fx. f(fx)
Es la funcin que aplicada sobre g, produce g aplicada sobre s misma, o g iterada dos veces.
Church emple este tipo de construcciones para definir nmeros enteros a travs del clculo
lambda. De hecho, la funcin fx.f(fx) identificara el nmero natural 2. A los nmeros naturales definidos por este procedimiento se le llaman numerales de Church:
0 = fx. x
1 = fx. fx
2 = fx. f(fx)
3 = fx. f(f(fx))
4 = fx. f(f(f((fx)))
etc.
Cualquier aplicacin de estas expresiones lambda sobre una funcin arbitraria f hace iterar sta
tantas veces como lo indica el numeral. Por ejemplo, la aplicacin de 3f sobre y sera:
(3f)y f(f(f(y))).
2. Operaciones bsicas de la aritmtica
De acuerdo a la tesis de Church, debe ser posible definir las operaciones aritmticas bsicas a
travs del clculo lambda, en especial la funcin de sucesor, que permite generar los nmeros
enteros positivos.
La funcin sucesor, la funcin adicin aritmtica, la funcin multiplicacin aritmtica y la
funcin potencia se pueden expresar en el clculo lambda respectivamente as:
Suc = n f x. f (n f x) Sucesor
Add = m n f x. m f (n f x) Adicin
Mul = m f x. m (f x) Multiplicacin
Pot = m f. m f Potencia
Como ejemplo, apliquemos la funcin sucesor a 2:
Suc 2 (n f x. f (n f x)) 2
f n. f (2 f x)
f n. f (g y. g (g y) f x)
f n. f ( y. f (f y) x)
f n. f ( f (f x)) = 3
3. Constructor y selector
Para definir funciones binarias en el clculo lambda, necesitamos definir previamente un
constructor y un selector.
A continuacin presentamos la representacin en clculo lambda de una funcin para construir
pares, que llamaremos par. Tambin presentaremos las representaciones de dos funciones
binarias selectoras, fst (first: primero) y snd (second: segundo), que se corresponden a los
combinadores que ya presentamos K y K*, respectivamente:
par := x y f. f x yfst := p. p (x y. x)snd := p. p (x y. y)
Aqu empleamos el smbolo := para significar se define como
Veamos un ejemplo que ilustra como operan estas funciones:
fst par p q (p. p (x y. x) a b f. f a b) p q (a b f. f a b (x y. x)) p q ( b f. f p b (x y. x)) q f. f p q (x y. x) (x y. x) p q (y. p) q
p
Con estas funciones simples, podemos definir otras compuestas. Como ejemplo, crearemos la
funcin swap:
swap := z. snd z fst z
A continuacin una ilustracin de cmo se comporta la funcin swap:
swap par p q (z. snd z fst z) ((x y f. f x y) p q) (z. snd z fst z) ( f.f p q) (z. snd z fst z) p q (snd p q) (fst p q)
(p. p (x y. y) p q) (p. p (x y. x) p q)) (p. p ( y. y) q) (p. p (x y. x) p q)) (p. p q) (p. p (x y. x) p q) (p. p q) (p. p ( y. p) q) (p. p q) (p. p p) q (p. p p) q p
4. Constantes y operaciones booleanas
Dado que muchas funciones emplean el condicional en sus definiciones, necesitamos constantes
y operaciones booleanas.
Para expresar los valores verdad (True) y falso (False) en clculo lambda usamos:
T = tf. tF = tf. f
El condicional podemos expresarlo de la siguiente manera: si B es una expresin que evala
verdad o falsedad, es decir, si es un booleano, entonces podemos definir una funcin test, que
evala sus argumentos de la siguiente manera:
Si B entonces P sino Q
Esta evaluacin puede ser representada por:
test := cxy. c x yde manera que, por ejemplo:
test T v w = (cxy. c x y) T v w
T v w = (tf.t) v w v
5. El clculo lambda como un lenguaje de programacin
Con este conjunto de definiciones bsicas numerales de Church, operaciones aritmticas
bsicas, constructor y selector, constantes y operaciones booleanas tenemos una base para
definir nuevas funciones y representar cmputos aritmticos en el clculo lambda. Bajo este
punto de vista, el clculo lambda puede ser considerado como un lenguaje de programacin
donde todos los objetos son definidios como funciones computables y donde las mismas
funciones pueden ser usadas como argumentos de otras funciones: de hecho, operaciones sobre
enteros positivos, como la funcin sucesor o la funcin suma, en el clculo lambda, donde hemos
representado estos nmeros a travs de numerales de Church, son funciones que reciben
funciones como argumentos. Por eso puede considerarse al clculo lambda como un lenguaje de
programacin funcin funcional.
De hecho, el clculo lambda ha inspirado el diseo de lenguajes de programacin usados
ampliamante en la prctica computacional como Lisp, diseado por John McCarthy en la dcada
de 1950, el primer lenguaje de programacin concebido para desarrollo de inteligencia artificial.
Adems, algunos lenguajes funcionales de programacin son en realidad el clculo lambda con
un conjunto de agregados y extensiones, llamadas frecuentemente azcar sintctica, que
facilitan y aligeran las tareas prcticas. El primer lenguaje enfocado en esta direccin fue ISWIM
(If you See What I Mean), propuesto por Landin (1966). Se trata del cculo lambda puro con
algunas construcciones de control como expresiones condicionales, y la clausula where como
mecanismo para definir funciones y asignar valores a variables. En realidad ISWIM no lleg a
implantarse en la prctica, pero si fue muy influyente en el desarrollo subsiguiente de lenguajes
funcionales de programacin como ML y Haskell. Despus de ISWIM, apareci Scheme, un
dialecto de Lisp diseado por Sussman y Steele (1975), que es una de las primeras realizaciones
prcticas del clculo lambda todava en amplio uso.
Estos lenguajes de programacin, que tienen en comn estar basados en el clculo lambda,
conforman una clase de lenguajes de programacin: los lenguajes de programacin funcionales.
Ms detalles sobre cmo el clculo lambda constituye el ncleo fundamental de los lenguajes
funcionales de programacin y sobre los mecanismos de implementacin usados se pueden
encontrar, por ejemplo, en Gordon (1988) y Paulson (1995).
El clculo lambda con tipos: origen y reglas
Church (1940) presenta una versin del clculo lambda que inclua asignacin de tipos para los
trminos lambda. Curiosamente, este sistema con asignacin de tipos para los trminos del
clculo lambda ha facilitado el descubrimiento de la correspondencia entre demostraciones
lgicas y programas, conocida como isomorfismo Curry-Howard. El objetivo de Church con este
clculo era dar una formulacin de la teora de tipos, sugerida independientemente por Leon
Chwistek y F. P. Ramsey, como una alternativa a la teora ramificada de tipos de Russell y
Whitehead, que incorporara ciertos rasgos de la conversin lambda.
El clculo lambda y el uso de tipos tienen su origen comn en la lgica. Posiblemente la primera
nocin de tipos se encuentra ya en Frege (1891), donde se revela la diferencia conceptual entre
objetos y predicados y se considera la jerarqua que se construye sobre estas nociones: en el nivel
inferior tenemos una coleccin de objetos bsicos, luego tenemos las propiedades de estos
objetos, despus tenemos propiedades de estas propiedades, etc.
Russell y Whitehead (1910 1913) introdujeron la teora ramificada de tipos como una manera
de evitar una paradoja descubierta en el sistema originalmente ofrecido por Frege (1893) como
fundamentacin de la aritmtica, conocida como paradoja de Russell. Originalmente, Church
pens que era posible evitar esta paradoja sin introducir tipos, pero slo mantenindose dentro de
una lgica intuicionista que use solamente alguna forma limitada de la ley del tercero excluido.
Sin embargo, dos estudiantes de Church, Kleene y Rosser (1935), demostraron que este sistema
es inconsistente. Church (1940) present luego una formulacin de lgica usando el clculo
lambda con asignacin de tipos simples, que puede concebirse como una simplificacin del
sistema de tipos usado en Principia Mathematica.
Una teora de tipos supone que en un sistema simblico no slo tratamos con objetos, como
trminos, frmulas y demostraciones. Tambin tratamos con tipos de objetos. El clculo lambda
con asignacin de tipos incluye tipos generados a partir de una base tipo 0 usando una
"flecha" () para representar un espacio de funcin A B, un nmero infinito de variables de cada tipo y trminos lambda construidos a partir de variables y las operaciones de aplicacin y
abstraccin. Las frmulas de este clculo son ecuaciones entre trminos del mismo tipo. Los
axiomas y reglas de inferencia son las versiones restringidas de las reglas de transformacin del
clculo lambda sin asignacin de tipos.
El sistema de Church tena dos tipos atmicos: para el tipo de proposiciones, para el tipo de individuos. Los tipos compuestos son del tipo de funciones desde a , que ahora
generalmente se denota como , pero que Church denotaba ( ). Las funciones
(proposicionales) de primer orden de Russell corresponden a trminos del tipo , sus
funciones (proposicionales) de segundo orden corresponden a trminos del tipo ( )
, etc.
En general, los tipos son objetos de naturaleza sintctica y pueden ser asignados a trminos
lambda. Si M es un trmino del clculo lambda y se le asigna un tipo , entonces decimos M tiene tipo ; la notacin que usaremos para esto es M : . Si M es una funcin, entonces tendr un tipo de funcin de la forma , y lo denotaremos M : 3. Curry llama argumento al
trmino lambda M en una expresin de la forma M : , y llama predicado a la parte que representa el tipo.
Los tipos vienen a solucionar tambin un cuestionamiento que se haca al clculo lambda: los
trminos del este clculo no representaban la nocin de funcin tal como los matemticos
acostumbraban a usar en la teora de conjuntos, la cual incluye un dominio y un rango dados
como parte de la definicin de funcin (Hindley y Seldin, 1996, pag. 159). En este sentido, cada
tipo atmico denota un conjunto particular, como el conjunto de los nmeros naturales, y cada tipo compuesto, de la forma , que se denota alguna funcin de a , representa funciones cuyo rango es un conjunto denotado por y cuyo rango es un subconjunto denotado por . A lo que refieran exactamente los tipos atmicos o el conjunto de funciones definidas por tipos
compuestos depender en todo momento del uso para el cual est destinada la teora de tipos
formal que se va a desarrollar. Cuando se especifica, por ejemplo, un conjunto de funciones,
como las funciones representables en algn modelo dado, todo tipo va a denotar un conjunto de
individuos o funciones especficos. Ms all de esto, los tipos son simples objetos sintcticos.
La inclusin de tipos en un sistema lgico como medio para evitar paradojas se debe a que ellos,
al definir algn conjunto para algn trmino o al establecer un dominio y un rango para un
3 Church empleaba superndices para la asignacin de tipos, de manera que si M es un trmino de tipo a escriba: M ; y si M es una funcin de tipo a , se escriba M a .
conjunto de funciones, limitan la informacin de los trminos. Por ejemplo, a travs de la
asignacin de tipos a trminos se pueden poner restricciones a la operacin de aplicacin: para
aplicar M a N, el tipo de N debe ser y el tipo de M debe ser ; entonces la aplicacin MN tendr el tipo . En el caso de la abstraccin, si x es una variable de tipo y M es un trmino
de tipo , entonces el trmino x.M, que denota una funcin, tendr el tipo .
En el caso de los combinadores, tenemos que, por ejemplo, el identificador simple I, definido por
la expresin x.x, designa una funcin que proyecta o asocia consigo mismo un trmino de tipo , por lo tanto: I: ( ). Esto significa que si x es el argumento de I y x tiene el tipo , entonces el valor I x es de tipo .
En general, tenemos que:
es el tipo de funciones del tipo al tipo .
La expresin x1 : 1, , xn : n t : , es un juicio sobre tipos, donde se dice que t tiene el tipo si cada xi tiene el tipo i. Usaremos letras griegas maysculas, como y , para designar listas de pares variable : tipo, a las que llamaremos contextos. As que si, en la expresin x1 :
1, , xn : n t : hacemos x1 : 1, , xn : n= , entonces podemos decir tambin que la expresin t : significa que t tiene el tipo en el contexto , donde el contexto no es sino una secuencia de trminos lambda con tipos asignados con la forma xi : i.
El clculo lambda con asignacin de tipos, tal como lo concibi Church (1940), incluye dos
reglas de transformacin o inferencia: una introduce la flecha de tipos y otra la elimina. Entonces
enunciamos las reglas de inferencia siguientes para el clculo lambda con asignacin de tipos:
(1) regla de abstraccin:
Si , x: M : , entonces (x.M): , si x no aparece libre en (2) regla de aplicacin:
Si M: y N: , entonces MN:.
Como puede notarse, la regla de abstraccin introduce flecha de tipos y la regla de aplicacin la
elimina. Se podr notar que hay una similaridad estructural con las reglas propuestas por
Gentzen (1934) para el fragmento condicional del clculo de deduccin natural, es decir, el
clculo lgico que slo incluye dos reglas de inferencia para el condicional, una que lo introduce
y otra que lo elimina. Esta circunstancia permite expresar en el estilo de la deduccin natural las
reglas del clculo lambda con asignacin de tipos.
Usemos ahora letras latinas maysculas para designar tipos. Enunciemos la regla de aplicacin
en el clculo lambda con tipos:
Sea t una funcin de tipo B a tipo A bajo las suposiciones en el contexto ; y sea u un trmino de tipo B bajo las suposiciones en el contexto . Podemos concluir entonces que t(u) es un trmino de tipo A bajo la combinacin de las suposiciones en los contextos
, .
Expresado formalmente:
t : B A u : B ( E), t(u) : A
Enunciemos ahora la regla de abstraccin:
Sea t un trmino de tipo B bajo las suposiciones en el contexto ; y sea u un trmino de tipo A bajo las suposiciones en el contexto . Podemos concluir entonces que x.t es un trmino de tipo B A bajo la las suposiciones en el contexto .
Expresado formalmente:
, t : B u : A ( I) x. t : B A
Algunas versiones del clculo lambda con tipos incluye explcitamente el siguiente axioma:
___________ Idx : A x : A
que expresa la reflexividad de las expresiones en este clculo. Este esquema es equivalente al
siguiente, si se considera que en l se tom el contexto como vaco: Id
, x : A x : AEntonces, si tomamos a = , x : A, podemos plantear el esquema Id de la siguiente forma:
Id x : A
Si, y slo si. (x : A) est en el contexto .
Tenemos entonces una regla para trminos que son variables, la regla que hemos llamado Id. Las
dems reglas, aplicacin y abstraccin, actan sobre funciones. De estas reglas, una, la
abstraccin, introduce el tipo de funciones y la otra, la aplicacin, lo elimina. Por este motivo
designamos estas dos reglas por ( I) y ( E), respectivamente. Reglas del clculo lambda con tipos de Church
____________x : A x : A
Id
, x : B t : A x. t : B A
I t : B A u : B
, t u : AE
A partir de estas reglas puede decidirse si a algn trmino corresponde cierto tipo en este clculo.
Como ejemplo, efectuaremos tres demostraciones para tipos cualesquiera A, B y C.
Demostraremos primero que para el tipo A que la siguiente expresin es vlida en este clculo:
(x. x ) : A ADemostracin:
(x: A) ( x: A) (Id) (x. x ) : A A (I)Demostremos ahora que la siguiente expresin pertenece al clculo lambda con tipos:
(x y. x ) : A B ADemostracin:
(x: A), (y: B) ( x: A) (Id) (x: A) (y . x) : (B A) (I)
(x y. x ) : A B A (I)
Finalmente, demostraremos la expresin ms compleja:
(x y z. x z (y z) ) : (A B C) (A B) (A C)
Demostracin:
x : (A B C) x : (A B C) z : A z : A y : (A B) y : (A B) z : A z : A x : (A B C), z : A x z (B C) y : (A B), z : A y z : B x : (A B C), y : (A B), z : A x z ( y z ): C x : (A B C), y : (A B) z. x z ( y z ): (A C) x : (A B C) yz. x z ( y z ) : (A B) (A C) xyz. x z ( y z ) : (A B C) (A B) (A C)
Ntese que las expresiones que hemos demostrado aqu, si le suprimiramos los tipos asignados,
tendramos las definiciones de los combinadores:
I x. x;
K xy. x;
S xyz.xz(y z).
Lo que quiere decir que a estos combinadores corresponden los siguientes tipos:
I : A A
K : A B A
S : (A B C) (A B) (A C)
Curiosamente, puede notarse que las expresiones a la derecha de los dos puntos, son muy
similares formalmente a los esquemas axiomticos del fragmento implicacional de la lgica
proposicional estilo Hilbert que presentamos en el primer captulo: los tipos correspondientes a
K y S son estructuralmente idnticos a los esquemas H1 y H2, respectivamente. Es esta
similaridad estructural la que estudiaremos en el siguiente captulo: pareciera que los trminos
lambda fueran el cmputo o la construccin efectiva de demostraciones del clculo
proposicional.
Veamos ahora qu ocurre con los tipos de los trminos del clculo lambda cuando se aplican las
conversiones propias de este clculo. La conversin en el clculo lambda con asignacin de
tipos, que representaremos aqu con el signo , queda caracterizada por los siguientes
esquemas y reglas, que encontramos en Hindley y Seldin (1996, pag. 162):
() (x. M ) : A B y. [y : A / x : A] M : B() ( (x. M ) : A B ) N : A [N : A / x : A] M : B() M : A M : A() M : A P : A (N : A B) M : A (N : A B) P : A
() M : A B P : A B (M : A B) N : A (P : A B) N : A() M : B P : B (x. M : B ) : A B (x. P : B ) : A B () M : A N : A, N : A P : A M : A P : A
Como en el clculo lambda sin inclusin de tipos, se denomina redex (reduction expression, en
espaol, expresin reducible) a toda expresin de la forma:
( (x. M ) : A B ) N : APor ejemplo, la reduccin de la expresin ( x.xz : A B) y : A, que aplica una funcin M del tipo A B, definida por xz, a un trmino N de tipo A, definido por y, nos da, por la regla (), la expresin yz : B. Esto tiene una particular importancia en al deduccin de tipos, pues una
deduccin de la forma:
x : A x : A D1(x)
D2 M : B (I) (x. M ) : A B N : A (I) (x. M ) N : B
D3
Se reduce a la forma:
D2 N : A
D1(N) [N / x : A] M : B
D3
Donde D3 se obtiene a partir de D3 reemplazando las apariciones de (x. M )N por [N/x] M.
Al hacer este paso de reduccin ocurre una contraccin en el sujeto (el trmino lambda M en la
expresin M : A). Adems, si suprimimos todos los sujetos de ambas deducciones, veremos que
este paso de reduccin se corresponde con el paso de reduccin de la implicacin en el clculo
de deduccin natural, tal como expusimos en el segundo captulo de este trabajo, en el apartado
Normalizacin. Obsrvese que, en la primera derivacin, el punto donde ocurre lo que sera
equivalente a la frmula de corte en un desvo en una derivacin en deduccin natural, aparece
aqu una expresin reducible con la forma:
( (x. M ) : A B ) N : A
Todas las propiedades de la conversin lambda del sistema sin asignacin de tipos se mantienen
en el sistema con asignacin de tipos. Pero, adems, los sistemas con asignacin de tipos tienen
una propiedad extra que no tienen los sistemas sin tipos, y que juega un rol esencial en todas sus
aplicaciones: las expresiones con tipos asignados son normalizables en sentido fuerte. Quiere
decir que para este sistema con tipos vale el siguiente teorema:
En el clculo lambda con tipos no hay reducciones- infinitas.A diferencia de lo que ocurre en el clculo lambda sin tipos, donde es posible encontrar
estrategias de reduccin de un trmino t dado que no conducen a una forma normal, en el clculo
lambda con asignacin de tipos todas las estrategias de normalizacin son buenas, en el sentido
de que siempre conducen a una forma normal y, por lo tanto, siempre terminan. El problema en
el clculo lambda sin tipos es que, a pesar de que en l para todo trmino siempre hay alguna
estrategia de normalizacin, el procedimiento de reduccin no es un algoritmo determinista,
siendo posibles muchas conversiones para un mismo trmino t dado. Si la normalizacin dbil
nos da un procedimiento para elegir en cada paso una expresin reducible apropiada que ha de
conducir a una forma normal, es decir, un trmino u que es irreducible, en el caso el clculo
lambda con tipos la normalizacin para cualquier trmino t dado es fuerte, pues no hay secuencia
de reduccin infinita que comience con este trmino t. Por supuesto, esta propiedad del clculo
lambda con tipos tiene relevancia desde el punto de vista del problema de la detencin, que
mencionamos al comienzo de este captulo.
Se atribuye a Tait (1967), la demostracin de que la reduccin beta en el clculo lambda con
tipos es fuertemente normalizable. Girard (2003, pags. 31 45) tambin presenta una versin de
la demostracin del teorema de normalizacin fuerte para el clculo lambda con tipos, todava
basada en la nocin de reducibilidad empleada por Tait. Esta demostracin de normalizacin
fuerte debera extenderse al fragmento implicacional de la lgica intuicionista por la
correspondencia Curry-Howard.
Ya hemos visto que existen similaridades estructurales entre la lgica proposicional y el clculo
lambda con asignacin de tipos:
1. El tipo que corresponde a los combinadores I, K y S son similares a los axiomas del
fragmento implicacional de la lgica proposicional estilo Hilbert.
2. La reduccin beta de una expresin del clculo lambda con tipos es similar a la reduccin
o contraccin del desvo o eliminacin de un corte en una derivacin en el clculo de
deduccin natural a travs del paso de reduccin para .
No es de extraar que los investigadores comenzaran a sealar estas correspondencias entre el
clculo lambda con asignacin de tipos y los sistemas de lgica proposicional. Una de las
primeras observaciones al respecto, y que ya hemos sealado aqu, la encontramos en Curry
(1967, pag. 388): existe correspondencia entre el los tipos asignados a trminos lambda y las
frmulas en un sistema axiomtico de lgica intuicionista proposicional, estilo Hilbert. En esta
correspondencia, los trminos lambda se corresponderan con las demostraciones de las frmulas
de la lgica intuicionista. Posteriormente, despus que Dag Prawitz (1965) demostrara los
teoremas de forma normal y de normalizacin para el clculo de deduccin natural estilo
Gentzen, Howard (1969) estableci la existencia de la correspondencia entre el clculo lambda
con asignacin de tipos y el clculo de deduccin natural para la lgica intuicionista, no slo
para el fragmento implicacional de la lgica proposicional, sino tambin para la lgica de primer
orden, destacando tambin la correspondencia entre reduccin de demostraciones y reduccin
lambda; a estas correspondencias se le conocen en la actualidad como isomorfismo Curry-
Howard o principio de frmulas-como-tipos.
Como veremos en el siguiente captulo, por este isomorfismo, entre otras cosas, podemos usar el
clculo lambda con asignacin de tipos como una notacin natural para las demostraciones en el
clculo de deduccin natural: el clculo lambda con tipos representa una manera natural de
codificar las demostraciones del clculo de deduccin natural. Adems, por este isomorfismo, los
resultados del clculo lambda pueden ser traducidos a un marco de demostraciones de deduccin
natural. Considerando que los cmputos que se hacen en el clculo lambda se corresponden con
algoritmos, se pueden ver programas como demostraciones, donde su especificacin (lo que el
programa debe hacer) sera como el teorema probado por la demostracin, y la ejecucin de un
programa sera como la normalizacin de una demostracin.