Marco Ordoñez

Términos del cálculo lambda (type free)

En este post veremos con más detalle la definición y reglas de los términos en el cálculo lambda.

El conjunto de expresiones lambda está definido de la siguiente forma:

  • Todas las variables son términos lambda (x, y, z...). También son llamadas átomos o término atómico.
  • Si M y N son términos-λ, entonces (MN) también lo es (aplicación).
  • Si M es un término-λ y x es una variable, entonces (λx.M) es un término-λ también (abstracción).

A continuación algunos ejemplos:

  1. (x (λx.(λx.x)))
  2. (λx.(yz))
  3. (λx.(xy))

En el caso (1), hay dos ocurrencias de la variable x, si bien está permitido no es una buena práctica.
En el caso (2), la expresión es del tipo (λx.M) tal que x no está presente en M. Este tipo de términos es llamada abstracciones vacías.

La expresión 'λ' no es un término, al igual que 'λx' tampoco lo es.

La asociación de los términos siempre es de izquierda a derecha. Por ejemplo, el término 'M N Q P' sería '(((M N) Q) P)'.

La longitud de un término M (|M|) es el número de ocurrencias de variables en el término M. Se define que:

|x| = 1

|MN| = |M| + |N|

|λx.M| = 1 + |M|

Por ejemplo el término |(λx.yz)(λh.op)| = 6

Los subtérminos de un término M son definidos por inducción de la siguiente forma:

  • Un átomo es un subtérmino de si mismo.
  • Si M ≡ λx.P, sus subtérminos son M y todos los subtérminos de P.
  • Si M ≡ OP, sus subtérminos son M, todos los subtérminos de O y todos los subtérminos de P.

Por ejemplo, si M(λx.yx)(λz.x(yx)), sus subtérminos serían: x, y, yx, λx.yx, x(yx), λz.x(yx) y M.

Una variable x es ligada solo sí se encuentran en el ámbito de una ocurrencia de λx en un término M, de lo contrario será una variable libre. Se debe considerar el caso en el que una variable x puede ser libre y ligada al mismo tiempo, por ejemplo: M ≡ x(λx.x).

En el siguiente post profundizaremos en las sustituciones.

También te puede interesar http://www.mordonez.me/un-primer-vistazo-al-calculo-lambda/

Marco Ordonez