Lambda Cálculo

Introducción

El cálculo lambda es un formalismo para representar funciones introducido por Alonzo Church en los años treinta.

El cálculo lambda trabaja con objetos llamados lambda-términos, que son cadenas de símbolos de una de las formas siguientes:

  • v
  • λv.E1
  • (E1 E2)

donde v es un nombre de variable tomado de un conjunto infinito predefinido de nombres de variables, y E1 y E2 son lambda-términos. Los términos de la forma λv.E1 son llamadas abstracciones. La variable ν se llama el Parámetro formal  de la abstracción, y E1 es el cuerpo de la abstracción.

El término λv.E1 representa la función que, si es aplicada a un argumento, liga el parámetro formal v al argumento y entonces computa el valor resultante de E1--- esto es, retorna E1, con cada ocurrencia de ν sustituido por el argumento.

Los términos de la forma (E1 E2) son llamados aplicaciones. Las aplicaciones modelan la invocación o ejecución de una función: La función representada por E1 es invocada, con E2 como su argumento, y se computa el resultado. Si E1 (a veces llamado el aplicando) es una abstracción, el término puede ser reducido: E2, el argumento, se puede sustituir en el cuerpo de E1 en lugar del parámetro formal de E1, y el resultado es un nuevo término lambda que es equivalente al antiguo. Si un término lambda no contiene ningún subtérmino de la forma (λv.E1 E2) entonces no puede ser reducido, y se dice que está en forma normal.

La expresión E[a/v] representa el resultado de tomar el término E y sustituir todas las ocurrencias libres de v por a:

(λv.E a) => E[a/v] 

por convención tomamos (a b c d ... z) como abreviatura para (... (((a b) c) d)... z). (Regla de asociación por la izquierda).

La motivación para esta definición de la reducción es que captura el comportamiento esencial de todas las funciones matemáticas. Por ejemplo, considérese la función que computa el cuadrado de un número. Se puede escribir el cuadrado de x es x*x (usando "*" para indicar la multiplicación.) x aquí es el parámetro formal  de la función. Para evaluar el cuadrado para un argumento particular, digamos 3, lo insertamos en la definición en lugar del parámetro formal:

El cuadrado de 3 es 3*3

para evaluar la expresión que resulta 3*3, tendríamos que recurrir a nuestro conocimiento de la multiplicación y del número 3. Puesto que cualquier cómputo es simplemente una composición de la evaluación de funciones adecuadas con argumentos primitivos adecuados, este principio simple de sustitución es suficiente para capturar el mecanismo esencial del cómputo. Por otra parte, en el cálculo lambda, nociones tales como '3' y '*' puede ser representado sin ninguna necesidad de operadores primitivos externamente definidos o de constantes. Es posible identificar los términos que en el cálculo lambda, cuando están interpretados convenientemente, se comportan como el número 3 y el operador de la multiplicación.

El cálculo lambda es computacionalmente equivalente en poder a muchos otros modelos plausibles para el cómputo; es decir, cualquier cálculo que se pueda lograr en cualesquiera de estos otros modelos se puede expresar en el cálculo lambda y viceversa.

Quizás parezca sorprendente que el cálculo lambda pueda representar cualquier cómputo concebible usando solamente las nociones simples de abstracción funcional y aplicación basado en la substitución textual simple de términos por variables. Pero aún más notable es que incluso la abstracción no es requerible: la lógica combinatoria es un modelo del cómputo equivalente al cálculo lambda, pero sin la abstracción.


Definición informal

En lambda cálculo, todas las expresiones representan funciones de un sólo argumento. Este argumento, a su vez, sólo puede ser una función de un sólo argumento. Todas las funciones son anónimas, y están definidas por expresiones lambda, que dicen que se hace con su argumento.

Por ejemplo, la función "sumar 2",
f(x) = x + 2 se expresa en lambda cálculo así:
λ x. x + 2 o, equivalentemente,
λ y. y + 2 (ya que el nombre de su argumento no es importante).

Y el número f(3) sería escrito como (λ x. x + 2) 3.
La aplicación de funciones de asociativa a izquierda: f x y = (f x) y.
Considerando la función que aplica una función al número 3: λ f. f 3. , podemos pasarle "sumar 2", quedando así:
(λ f. f 3) (λ x. x + 2).

Las tres expresiones:

(λ f. f 3)(λ x. x + 2) , (λ x. x + 2) 3 y 3 + 2 son equivalentes.

No todas las expresiones lambda pueden ser reducidas a un "valor" definido. Considérese la siguente:

(λ x. x x) (λ x. x x)
ó
(λ x. x x x) (λ x. x x x)

tratar de reducir estas expresiones sólo lleva a encontrase con la misma expresión o algo más complejo.

(λ x. x x) es conocido como ω combinador;
((λ x. x x) (λ x. x x)) se conoce como Ω,
((λ x. x x x) (λ x. x x x)) como Ω2, etc.

Definición formal

Gramática

Formalmente, se comienza con un conjunto infinito numerable de identificadores, por ejemplo {a, b, c,..., x, y, z, x1, x2,...}. El conjunto de todas las expresiones lambda puede ser descrito usando esta gramática libre de contexto:
  1. <expr> ::= <identificador>
  2. <expr> ::= (λ <identificador>. <expr>)
  3. <expr> ::= (<expr> <expr>)

Las primeras dos reglas, generan funciones, la última describe la aplicación de una función a su argumento. Usualmente, los paréntesis para las abstracciones lambda (regla 2) y la aplicación de funciones (regla 3) son omitidos si no hay ambigüedad, asumiendo que la aplicación de funciones es asociativa a izquierda y el lambda abarca toda la expresión que le sigue. Por ejemplo: ((λ x. (x x)) (λ y. y)) puede ser expresada como (λ x. x x) λ y. y.

Términos

Sea X un conjunto infinito numerable. El conjunto L de los términos del λ-cálculo son las frases del lenguaje reconocido por la siguiente gramática:
      L ::= x     x Є X         variables
        ||  ut    u,t Є L       aplicación
        ||  λx.t  x Є X, t Є L  abstracción
        ||  (t)   t Є L

La aplicación asocia hacia la izquierda: ut1 t2... tk representa (...((ut1)t2)...)tk y cuando k=0 representa a u

Subtérminos

Los subtérminos de un término t (notación Sub(t)) son:
         Sub(x) = x (x Є X)
        Sub(uv) = Sub(u) ∪ Sub(v) ∪ {(uv)}
      Sub(λx.u) = Sub(u) ∪ {λx.u}

Variables libres y ligadas

Las apariciones (ocurrencias) de variables en una expresión son de tres tipos:
  1. Ocurrencias de ligadura (binders)
  2. Ocurrencias ligadas (bound occurrences)
  3. Ocurrencias libres (free occurrences)

Las variables de ligadura son aquellas que están entre el λ y el punto. Por ejemplo, siendo E una expresión lambda:

     (λ x y z. E) Los binders son x,y y z.
El binding de ocurrencias de una variable está definido recursivamente sobre la estructura de las expresiones lambda, de esta manera:
  1. En expresiones de la forma V, donde V es una variable, V es una ocurrencia libre.
  2. En expresiones de la forma λ V. E, las ocurrencias son libres en E salvo aquellas de V. En este caso las V en E se dicen ligadas por el λ antes V.
  3. En expresiones de la forma (E E′), las ocurrencias libres son aquellas ocurrencias de E y E′.

Expresiones lambda tales como λ x. (x y) no definen funciones porque las ocurrencias de y están libres. Si la expresión no tiene variables libres, se dice que es cerrada.

Como se permite la repetición del identificador de variables, cada binding tiene una zona de alcance asociada (scope de ahora en adelante) Un ejemplo típico es: (λx.x(λx.x))x, donde el scope del binding más a la derecha afecta sólo a la x que tiene ahí, la situación del otro binding es análoga, pero no incluye el scope de la primera. Por último la x más a la derecha está libre. Por lo tanto, esa expresión puede reexpresarse así (λy.y(λz.z))x

Las variables libres de t (notación VL(t)) es el conjunto de variables con al menos una ocurrencia libre en t. Un término sin variables libres es un término cerrado.

         VL(x) = {x} (x Є X)
        VL(uv) = VL(u) ∪ VL(v)
      VL(λx.u) = VL(u) - {x}

Las variables ligadas de t (notación VG(t)) son las variables que aparecen en t siguiendo al simbolo λ. Las variables de t (notación Var(t)) son las variables libres y ligadas en t.

         VG(x) = ∅ (x Є X)
        VG(uv) = VG(u) ∪ VG(v)
      VG(λx.u) = VG(u) ∪ {x}
        Var(t) = VL(t) ∪ VG(t)

Sustitución simple

Sea u, t1,...,tk términos y x1,...,xk variables distintas. La aplicación en un término u de la substitución
   s = [xi ← ti| 1 ≤ i ≤ k]
escrito us se define por la recurrencia sobre la estructura de t.
     (xj)s = tj                                   1 ≤ i ≤ k
      (y)s = y                                    y { x1,...,xk}
     (uv)s = (us)(vs)
 (λ xj.u)s = λ xj.(u[xi ← ti| i=1,...,k,j ≠ i])   1 ≤ i ≤ k
  (λ y.u)s = λy.(us)                              y { x1,...,xk}

α-Equivalencia (≡)

Se puede cambiar el nombre de las varaibles ligadas y obtener expresiones equivalentes. Para ello se define la relación ≡ entre términos por recurrencia sobre su estructura.
                                   x ≡ x (x Є X)
   u ≡ u'  y    v ≡ v'     ⇒      uv ≡ u'v'
   v[x  y] ≡ v'[x'  y]     ⇒      λx.v ≡ λx'.v'
   
   y ∉ Var(v)  Var(v')

Si u ≡ u' entonces VL(u) = VL(u') y ambos términos tienen igual número de nodos


Clausuras Reflexiva y Transitiva

Sea R una relación binaria. La clausura reflexiva Rr de R es la mas pequeña relación binaria que contiene R tal que si uRrpara todo elemento u. La clausura transitiva (o reflexotransitiva) R* de R es la más pequeña relación binaria que contiene Rr tal que si uR*v y vR*w entonces uR*w.

Si uR*w, existe n ≥ 0 y los elementos v0 = u, v1, ...,vn = w tales que para todo i(1 ≤ i ≤ n), vi-1 Rvi


α-Conversión

La regla de alfa-conversión fue pensada para expresar la idea siguiente: los nombres de las variables ligadas no son importantes. Por ejemplo λx.x y λy.y son la misma función. Sin embargo, esta regla no es tan simple como parece a primera vista. Hay algunas restricciones que hay que cumplir antes de cambiar el nombre de una variable por otra. Por ejemplo, si reemplazamos x por y en λx.λy.x, obtenemos λy.λy.y, que claramente, no es la misma función. Este fenómeno se conoce como captura de variables.

La regla de alfa-conversión establece que si V y W son variables, E es una expresión lambda, y

   E[V := W] 
representa la expresión E con todas las ocurrencias libres de V en E reemplazadas con W, entonces
    λ V. E  ==  λ W. E[V := W] 
si W no está libre en E y W no está ligada a un λ donde se haya reemplazado a V. Esta regla nos dice, por ejemplo, que λ x. (λ x. x) x es equivalente a λ y. (λ x. x) y.

En un ejemplo de otro tipo, se ve que

for (int i = 0; i < max; i++) { proc(i); } 
es equivalente a
for (int j = 0; j < max; j++) { proc(j); } 

β-Reducción

La regla de beta reducción expresa la idea de la aplicación funcional. Enuncia que
    ((λ V. E) E′)  ==  E[V := E′]
si todas las ocurrencias de E′ están libres en E[V := E′].
Una expresión de la forma ((λ V. E) E′) es llamada un beta redex. Una lambda expresión que no admite ninguna beta reducción se dice que está en su forma normal. No toda expresión lambda tiene forma normal, pero si existe, es única. Más aún, existe un algoritmo para computar la formal normal: la reducción de orden normal. La ejecución de este algoritmo termina si y sólo si la expresión lambda tiene forma normal. El teorema de Church-Rosser nos dice que dos expresiones reducen a una misma si y sólo si son equivalentes (salvo por el nombre de sus variables ligadas)

η-Conversión

Es la tercera regla, esta conversión, que podría ser añadida a las dos anteriores para formar una nueva relación de equivalencia. La eta conversión expresa la idea de extensionalidad, que en este contexto implica que dos funciones son la misma si y solo si dan el mismo resultado para cualquier argumento. La eta conversión convierte entre λ x. f x y f siempre que x no aparezca sola en f. Esto puede ser entendido como equivalente a la extensionalidad así:
Si f y g son extensionalmente equivalentes, es decir, si f a==g a para cualquier expresión lambda a entonces, en particular tomando a como una variable x que no aparece sola en f ni en g, tenemos que f x == g x y por tanto λ x. f x == λ x. g x, y así por eta conversión f == g. Entonces, si aceptamos la eta conversión como válida, resulta que la extensionalidad es válida.

Inversamente, si aceptamos la extensionalidad como válida entonces, dado que por beta reducción de todo y tenemos que (λ x. f x) y == f y, resulta que λ x. f x == f; es decir, descubrimos que la eta conversión es válida.


Cálculos aritméticos con lambda

Hay varias formas posibles de definir los número naturales  en el cálculo lambda, pero el más común son los números de Church, que pueden definirse como sigue:

0 := λ f x. x
1 := λ f x. f x
2 := λ f x. f (f x)
3 := λ f x. f (f (f x))

y así sucesivamente. Instintivamente el número n en el cálculo lambda es una función que toma a otra función f como argumento y devuelve la n-ava composición de f. Así que, un número de Church es una función de alto nivel -- toma una única función f como parámetro y otra función de parámetro único.

(Véase que en el cálculo original lambda de Church era obligatorio que el parámetro formal de la expresión lambda apareciera al menos una vez en el cuerpo de la función, lo que hace imposible definir el 0.) Dada esta definición de los números de Church, se puede establecer una función de sucesión que dado un número n devuelve n + 1:

SUCC := λ n f x. f ((n f) x)

La suma se define así:

PLUS := λ m n f x. n f (m f x)

PLUS puede entenderse como una función que toma dos números naturales como parámetros devolviendo otro; puede verificarse que

PLUS 2 3    and    5

son expresiones lambda equivalentes. La Multiplicación se expresa como

MULT := λ m n. m (PLUS n) 0,

la idea es que multiplicar m y n es lo mismo que sumar m veces a n. De otra manera:

MULT := λ m n f. m (n f)

La función Predecesor  PRED n = n - 1  de un entero positivo n es más compleja:

PRED := λ n f x. ng h. h (g f)) (λ u. x) (λ u. u

o alternativamente

PRED := λ n. ng k. (g 1) (λ u. PLUS (g k) 1) k) (λ v. 0) 0

Véase que el truco consiste en que (g 1) (λ u. PLUS (g k) 1) k que devuelve k si el valor de g(1) es cero o g(k) + 1 en cualquier otro caso.


Lógica y predicados

Para poder llegar a una definición de booleanos en cálculo lambda, se comienza con su especificación: TRUE, FALSE e ifthenelse deben ser λ-expresiones en forma normal, tal que para todo par de λ-expresiones P y Q

(ifthenelse FALSE P Q) →β Q
(ifthenelse TRUE P Q) →β P

Cualquier par de expresiones que cumplan esto sirve. La solución más simple resulta de fijar ifthenelse como λb.λx.λy. b x y, dejando que todo el trabajo de aplicar los booleanos recaiga sobre TRUE y FALSE, entonces:

(ifthenelse TRUE) →β (λx.λy.x)
(ifthenelse FALSE) →β (λx.λy.y)

Quedando:

TRUE := λ x y. x
FALSE := λ x y. y

Los booleanos (como era de esperarse) también son funciones. Es fácil ver que es posible cambiar la λ-expresión ifthenelse para que aplique los parámetros en orden inverso, cambiando la forma de TRUE y FALSE. Por eso, se adapta, por convención, de esta manera. (conocida como booleanos de Church) Nótese que FALSE es equivalente al número de Church cero.

Luego, con estas dos definiciones podemos definir algunos operadores lógicos:

AND := λ p q. p q FALSE
OR := λ p q. p TRUE q
NOT := λ p. p FALSE TRUE

Ahora podemos reducir, por ejemplo:

AND TRUE FALSE
≡ (λ p q. p q FALSE) TRUE FALSE →β TRUE FALSE FALSE
≡ (λ x y. x) FALSE FALSE →β FALSE

y vemos que AND TRUE FALSE es equivalente a FALSE.

Un predicado es una función que devuelve un valor booleano. El predicado más simple es ISZERO el cual nos devuelve TRUE si el número de Church argumento es 0 o FALSE en otro caso.

ISZERO := λ n. nx. FALSE) TRUE

Por supuesto, esta definición nos sirve sólo para los números naturales definidos previamente.


Pares

Un par (2-tupla) puede ser definido en términos de TRUE y FALSE.

CONS := λfs. λb. b f s
CAR := λp. p TRUE
CDR := λp. p FALSE
NIL := λx.TRUE
NULL := λp. p (λx y.FALSE)

Una estructura de datos del tipo lista enlazada puede ser definida, tanto como NIL para la lista vacía, o como el CONS de un elemento y de la lista más pequeña.


Recursión

Recursión es la definición de una función usando la función que se está definiendo. El cálculo lambda no permite esto. Sin embargo, esta noción es un poco confusa. Considere por ejemplo la definición de la función factorial f(n) definida recursivamente por:
f(n) = 1, if n = 0; and n·f(n-1), if n>0.

En el cálculo lambda, no es posible definir funciones que se incluyan a si mismas. Para sortear esta dificultad, se comienza por definir una función, denominada aquí como g, que toma a una función f como argumento y devuelve otra función que toma n como argumento:

g := λ f n. (1, if n = 0; and n·f(n-1), if n>0).

La función que devuelve g es o bien la constante 1, o n veces la aplicación de la función f a n-1. Usando el predicado ISZERO, y las definiciones booleanas y algebraicas anteriores, la función g puede ser definida en el cálculo lambda.

Sin embargo, g todavía no es recursiva en si misma; para usar g para crear la función factorial recursiva, la función pasada a g como f debe tener unas propiedades específicas. A saber, la función pasada como f debe expandirse a la funcióng llamada con un argumento -- y que el argumento debe ser la función que ha sido pasado como f de nuevo.

En otras palabras, f debe expandir a g(f). Esta llamada a g expandirá a la siguiente a la función factorial y calculará otro nivel de recursión. En la expansión la función f aparecerá nuevamente, y nuevamente expandirá a g(f) y continuara la recursión. Este tipo de función, donde f = g(f), es llamada un fixed-point de g, y resulta que puede ser implementado en el cálculo lambda usando lo que es conocido como el paradoxical operator or fixed-point operator y es representado como Y -- el Y combinator: 

Y = λ g. (λ x. g (x x)) (λ x. g (x x))

En el cálculo lambda, Y g es un punto dijo de g, debido a que expande a g (Y g). Ahora, para completar nuestra llamada recursiva a la función factorial, simplemente llamaría  g (Y g) n,  donde n es el número del cual queremos calcular el factorial.

Dado, por ejemplo n = 5, esta se expandirá como:

n.(1, si n = 0; y n·((Y g)(n-1)), si n>0)) 5
1, si 5 = 0; y 5·(g(Y g)(5-1)), si 5>0
5·(g(Y g) 4)
5·(λ n. (1, si n = 0; y n·((Y g)(n-1)), si n>0) 4)
5·(1, si 4 = 0; y 4·(g(Y g)(4-1)), si 4>0)
5·(4·(g(Y g) 3))
5·(4·(λ n. (1, si n = 0; y n·((Y g)(n-1)), si n>0) 3))
5·(4·(1, if 3 = 0; y 3·(g(Y g)(3-1)), si 3>0))
5·(4·(3·(g(Y g) 2)))
...

Y así, se va evaluando la estructura del algoritmo de forma recursiva. Cada función recursiva definida puede ser vista como un punto fijo de otra función adecuada, y por lo tanto, utilizando Y, cada función recursiva definida puede expresarse como una expresión lambda. En particular, ahora podemos definir limpiamente la resta, la multiplicación y la comparación de predicado de los números naturales de forma recursiva.


Normalización

Se dice que un término esta en forma normal (FN) si no contiene radicales. Un término t es normalizable si existe t' en forma normal tal que (t β⇒ t').

Un término t es fuertemente normalizable si no existe secuencia infinita de β-conversiones a partir de t.


Tipos

Verificación de tipos

Para saber si un programa esta bien escrito se debe demostrar su corrección, esta no puede ser verificada automáticamente, es un problema indecidible. Puede realizarse análisis estáticos para la verificación del programa. Antes de correr los programas pueden identificarse errores de no correspondencia entre operaciones y sus argumentos.

Tipos y esquemas

Sea Xt el conjunto de variables de tipo con elementos típicos α, β, ...:Ct el conjunto de constructores de los términos y el cuantificador universal ∀. Los conectores binarios →, × Є Ct serán escritos de forma infija. Los tipos int, bool,... corresponden a las constantes y expresiones de tipo entero, booleano, etc. El conjunto T de tipos y el conjunto S de los esquemas de tipos se definen con la gramatica siguiente:
 T ::= α || τ → ρ || τ × ρ || c(τ1, ..., τn)
        
    α Є Xt, c Є Ct, τ, ρ, τ1,...τn Є T(n ≥ 0)
        
 S ::= ∀ α.δ || τ  α Є Xt, τ Є T, δ Є S 

La flecha asocia hacia la derecha, los paréntesis podrán ser utilizados según sea necesario. Los elementos de S, llamados esquemas de tipo, se construyen a partir de los tipos agregando cuantificadores de variables al exterior.

Sustitución y Unificación

La sustitución y la unificación de términos se aplica a los tipos (mas no a los esquemas). Por ejemplo

Para unificar los tipos α → β → γ y (δ → δ) → δ → δ, primero hay que reconocer, usando la regla de asociación de la flecha, la estructura de los constructores de tipo(para ello puede resultar útil introducir los paréntesis adicionales α → (β → γ) y (δ → δ) → (δ → δ)). Es importante notar que una parentisacion incorrecta conduce invariantemente a un resultado incorrecto en lal unificación. Al unificar a izquierda de la flecha principal se obtiene la sustitucion [ α (δ → δ) ], la cual se completa unificando a derecha con [ β ← δ, γ ← δ ].

Ambiente de tipos

Un ambiente de tipos Г es una parte finita de ((X ∪ Cc ) × S), donde X es el conjunto de las variables de las λ-expresiones y Cc es un conjunto de símbolos que representan los constructores de tipos (que serán utilizados posteriormente), tal que X ∩ Cc = Ø. Un ambiente representa un conjunto de hipótesis sobre los tipos de las variables de una expresión.

En un ambiente Г bien formado , los elementos de X ∪ Cc en cada par todos son distintos. Cada par (x,σ) de Г será notado como x:σ. Las variables libres de Г se definen como VL(Г)={VL(σ)|x:σ Є Г}.

La extension de un ambiente con una nueva asignación de tipo, excluye una eventual ocurrencia de una variable con el mismo nombre.

Г + {x:σ} = {y:σ'|y:σ' Є Г ∧ y x} ∪ {x:σ} 

Instanciación

La relación de instanciación entre un esquema σ ≡ ∀α1...αn.ρ y un tipo τ, escrita inst(σ,τ), se establece cuando existe una sustitución s cuyo dominio es el conjunto {α1...αn} tal que (ρ)s = τ.

Si un esquema no tiene cuantificadores, su instanciación es él mismo. La forma más genérica de instanciar un esquema es remplazando las variables cuantificadas por variables nuevas (es decir,variables que no se hayan utilizado anteriormente en el contexto de trabajo).

Sistema de tipos monomórfico

Las siguientes reglas definen la tipabilidad de un término t Є T. El juicio Г Ⱶ t : τ se lee "Dado Г, el tipo de t es τ".

Se escribirá Ⱶ t : τ como abreviación de ∅ Ⱶ t : τ. Ninguna de las reglas presentadas hasta ahora introduce esquemas con cuantificadores, de manera que, la instanciacion se comportará como una identidad.

El axioma Г Ⱶ c : τc (Ctt) tiene una instancia para cada constante. Por ejemplo, Ⱶ 1:int, Ⱶ false:bool, Ⱶ +:int → int → int, etc.

Derivaciones de Tipos

Para utilizar el sistema propuesto en el cálculo del tipo de una expresión, se utiliza la unificación como mecanismo de acoplamiento entre reglas.

Ejemplo: la siguiente derivación permite calcular el tipo de la funcion 2 = λf.λx.f(f x)

Para derivar el tipo de la expresión (λf.λx.f(fx))(λx.1) es necesario realizar entre otros, los pasos que permitieron conocer el tipo de λf.λx.f(f x). Sin embargo, la derivación no es idéntica puesto que el tipo para esta subexpresión debe ser más particular (int → int) → int → int en lugar de (α → α) → α → α

Aquí se encuentra un ejemplo completo de derivación Ejemplo de Derivación

Tipo del producto cartesiano

A los pares ordenados u,v les corresponde como tipo el producto cartesiano de los tipos de u y de v:
    Г Ⱶ u:τ    Г Ⱶ v:ρ
        Producto:
    Г Ⱶ u,v : τ × ρ
Tipos para la recursión y condicionales

Dos nuevas reglas permiten el análisis de las definiciones recursivas:

    Г Ⱶ b:bool   Г Ⱶ u:τ    Г Ⱶ v:τ
        Condicional:
    Г Ⱶ if b then u else v:τ
    Г + {f:τ} Ⱶ u:τ
        Recursión:
    Г Ⱶ rec f = u:τ

En los condicionales la condición debe ser booleana y para lograr hacer un análisis estático de de las expresiones (es decir, antes de calcular su valor), se requiere que ambos lados del condicional tengan el mismo tipo, que es el tipo resultante. En la recursión, el tipo de la variable recursiva y el de la expresión que la define deben ser idénticos.


Estructuras de Datos

Definición de estructuras de datos

Se han introducido anteriormente los conjuntos X como el conjunto de variables de los términos de T, Xt como el conjunto de las variables de tipo y Ct como el conjunto de los nombres de tipo. Sea Cc un conjunto de símbolos que representan los constructores de tipos, tal que XCc = ∅

En una definición de tipo bien formada los constructores C1,...,Cn son todos diferentes, las variables de cada tipo τi están contenidas en { α1,...,αm }

Las listas de valores de tipo uniforme se definen en la construcción:

u representa el resto de las expresiones donde las listas se utilizan.

Reglas de tipo para definiciones de datos

Una definición de estructura de datos extiende el ambiente con las operaciones de construcción de nuevos objetos del tipo. En las siguientes reglas, def representa una construcción a la forma:

Las reglas auxiliares a la regla Tipo tratan la definición de constructor de Tipos.

Al definir el tipo de las listas el ambiente resultante contiene al conjunto.

Estos son los primeros ejemplos de esquemas de tipos con cuantificador en los ambientes. Dado el ambiente Гl se puede derivar el tipo de la expresión [[1]] (lista de lista que contiene la constante 1), la cual escrita sin las abreviaciones representa el término ::(::(1,[]),[]). Para representar la prueba se utilizan las siguientes abreviaciones:

Primero se obtiene el tipo de ::(1,[])

El tipo de la expresión completa se obtiene con una derivación:

Definiciones por caso

Los patrones serán extendidos a continuación para incluir las construcciones introducidas en las definiciones por casos.

Las reglas de filtrage se extienden naturalmente:

La notación [ p ← v ] se simplifica hasta obtener una substitución igualmente en el caso de los tipos contruidos:

Reglas de tipo para definiciones por caso

Para extender la regla de la abstracción con las definiciones por casos se introduce una nueva regla y sus auxiliares:

Cada patron en cada caso genera una extensión del ambiente con la cual se deriva el tipo de la expresión asociada. Las reglas auxiliares permiten distribuir el tipo del patrón entre sus variables.

Polimorfismo

Los constructores de tipos admiten diferentes instancias de tipos. En el ejemplo anterior, el constructor ::, cuyo esquema de tipo asociado a ∀α.α × lista(α) → lista(α), toma en sus dos instancias los tipos int × lista(int) → lista(int) (remplazando α por int) y lista(int) × lista(lista(int)) → lista(lista(int)) (remplazando α por lista(int)).

Se introduce una nueva construcción que permitirá asociar esquema de tipos a las variables, permitiendo así su uso en diferentes contextos con diferentes instancias de tipo.

Desde el punto de vista de su evaluación, esta nueva construcción puede considerarse como una abreviación de la expresión (λp.v)u.

Reglas de tipo para definiciones locales

Sea Г un ambiente τ un tipo y σ un esquema. La relación gen(Г,τ,σ) de generalización se cumple cuando σ = ∀α.τ. Donde α = Var(τ) - VL(Г)

La regla de tipos para las definiciones locales introduce esquemas de tipos mediante la generalización.


Bibliografía

- A shor introduction to the a Lambda Calculus. Achim Jung..
- P. M, Kogge, The Architecture of Symbolic Computers, McGraw-Hill, New York, 1991, chapter 4.
- G. Michaelson, An Introduction to Functional Programming through Lambda Calculus, Addison-Wesley, Wokingham, 1988.
- G. Revesz, Lambda-Calculus Combinators and Functional Programming, Cambridge University Press, Cambridge, 1988, chapters 1,3
- El Cálculo Lambda Puro. Favio Ezequiel Miranda Perea
- Cálculo lambda en Wikipedia 
- Cálculo lambda en Enciclopedia.us.es
- La Máquina G. Elementos del lambda cálculo
- Modelos de computación