Cálculo lambda - Historial de revisiones

Javiermartin jc: Texto reemplazado: «
» por «»

2019-06-21T00:36:14Z

Texto reemplazado: «<div align="justify">» por «»

Pinar1 jc en 17:50 29 sep 2011

2011-09-29T17:50:24Z

Pinar1 jc: /* β-reducción */

2011-09-28T15:55:35Z

‎β-reducción

Pinar1 jc: /* η-conversión */

2011-09-28T15:55:09Z

‎η-conversión

Pinar1 jc: /* Definición formal */

2011-09-28T15:52:50Z

‎Definición formal

Pinar1 jc: /* Definición Informal */

2011-09-28T15:52:05Z

‎Definición Informal

Pinar1 jc: /* β-reducción */

2011-09-28T15:48:27Z

‎β-reducción

Pinar1 jc: Página creada con '{{Definición |nombre= Cálculo Lambda |imagen= |tamaño= |concepto= Es el lenguaje de programación mas pequeño consiste en transformación simple(sustituir variables) y en d...'

2011-09-28T15:43:06Z

Página creada con '{{Definición |nombre= Cálculo Lambda |imagen= |tamaño= |concepto= Es el lenguaje de programación mas pequeño consiste en transformación simple(sustituir variables) y en d...'

Página nueva

{{Definición
|nombre= Cálculo Lambda
|imagen=
|tamaño=
|concepto= Es el lenguaje de programación mas pequeño consiste en transformación simple(sustituir variables) y en definir funciones
}}
'''Cálculo Lambda'''. Es el más pequeño lenguaje universal de programación, consiste en en una regla de transformación simple (sustituir variables) y un esquema simple para definir funciones.

El cálculo lambda se puede decir que es equivalente a las máquinas Turing porque es capaz de evaluar y expresar cualquier función computable. Church había querido hacer un sistema formal completo para modelizar la matemática pero después separó el cálculo lambda y lo ideó para que estudiara la computabilidad.

== Surgimiento ==

Originalmente, Church había tratado de construir un sistema formal completo para modelizar la [[Matemática]]; pero cuando éste se volvió susceptible a la paradoja de Russell, separó del sistema al cálculo lambda y lo usó para estudiar la computabilidad, culminando en la respuesta negativa al problema de la parada.

== Definición Informal ==

Considérese las siguientes dos [[Función matemática|Funciones]]. Por un lado, la [[Función Identidad]] ''I(x) = x'', que toma un único argumento, ''x'', e inmediatamente devuelve ''x''. Por otro lado, la función suma ''S(x,y) = x + y'', que toma dos argumentos, ''x'' e ''y'', y devuelve la suma de ambos: ''x + y''. Usando estas dos funciones como ejemplo, es posible hacer algunas observaciones útiles acerca de varias ideas fundamentales del cálculo lambda.

La primera observación es que las funciones no necesitan ser explícitamente nombradas. Esto es, la función ''S(x,y) = x + y'' puede ser reescrita como una función anónima: ''x,y → x + y'' (que se lee: «el par de ''x'' e ''y'' se mapea a ''x + y''»). Del mismo modo, ''I(x) = x'' puede ser reescrita de forma anónima como ''x → x'', que se lee: «el argumento ''x'' se mapea a sí mismo».

La segunda observación es que el nombre que se asigne a los argumentos de la función es generalmente irrelevante. Esto es, ''x → x'' e ''y → y'' expresan la misma función: la función identidad. Del mismo modo, ''x,y → x + y'' y ''u,v → u + v'' expresan la misma función: la función suma.

Una tercera observación es que toda función que requiere dos argumentos, como por ejemplo la función suma, puede ser reescrita como una función que acepta un único argumento, pero que devuelve ''otra'' función, la cual a su vez acepta un único argumento. Por ejemplo, ''x,y → x + y'' puede ser reescrita como ''x → (y → x + y)''. Esta transformación se conoce como currificación, y puede generalizarse para funciones que aceptan cualquier número de argumentos. Esta puede parecer oscuro, pero se entiende mejor mediante un ejemplo. Considérese la función suma no currificada:

:''x,y → x + y''

Al tomar a los números 2 y 3 como argumentos, se obtiene:

:''2 + 3''

Lo cual es igual a 5. Considérese ahora la versión currificada de la función:

:''x → (y → x + y)''

Si se toma al número 2 como argumento, se obtiene la función:

:''y → 2 + y''

Y tomando luego al número 3 como argumento, se obtiene:

:''2 + 3''

Lo cual es igual a 5. De modo que la versión currificada devuelve el mismo resultado que la versión no currificada. En el cálculo lambda, todas las expresiones representan funciones anónimas de un sólo argumento.

Una cuarta observación es que una función puede aceptar como argumento a ''otra'' función, siempre y cuando esta otra función tenga ella misma un sólo argumento. Por ejemplo, la función identidad puede aceptar como argumento a la función suma (currificada). Es decir, se toma a la función ''x → (y → x + y)'' y se la pone como argumento en ''z → z''. El resultado será obviamente ''x → (z → x + z)'', (igual a la ''x → (y → x + y)'') pues la función identidad siempre devuelve lo mismo que se le da.

En el cálculo lambda, las funciones están definidas por expresiones lambda, que dicen qué se hace con su argumento. Por ejemplo, la función "sumar 2", <tt> ''f''(''x'') = ''x'' + 2 </tt> se expresa en cálculo lambda así: <tt> λ ''x''. ''x'' + 2 </tt> (o, equivalentemente, <tt> λ ''y''. ''y'' + 2</tt>
ya que el nombre de su argumento no es importante). Y el número <tt>''f''(3)</tt> sería escrito como <tt> (λ ''x''. ''x'' + 2) 3</tt>. La aplicación de funciones es [[asociatividad|asociativa]] a izquierda: <tt> ''f'' ''x'' ''y'' = (''f'' ''x'') ''y''</tt>. 
Considerando la función que aplica una función al número <tt>3</tt>:<tt> λ ''f''. ''f'' 3</tt>. , podemos pasarle "sumar 2", quedando así: <tt> (λ ''f''. ''f'' 3) (λ ''x''. ''x'' + 2)</tt>. 

Las tres expresiones:
: <tt>(λ ''f''. ''f'' 3)(λ ''x''. ''x'' + 2)   </tt>, <tt>   (λ ''x''. ''x'' + 2) 3   </tt> y <tt>   3 + 2   </tt>
son equivalentes.


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

: <tt>(λ ''x''. ''x'' ''x'') (λ ''x''. ''x'' ''x'')</tt>
ó
: <tt>(λ ''x''. ''x'' ''x'' ''x'') (λ ''x''. ''x'' ''x'' ''x'')</tt>
tratar de reducir estas expresiones sólo lleva a encontrase con la misma expresión o algo más complejo. <tt> (λ ''x''. ''x'' ''x'') </tt> es conocido como ω combinador;
<tt> ((λ ''x''. ''x'' ''x'') (λ ''x''. ''x'' ''x'')) </tt>
se conoce como Ω,
<tt> ((λ ''x''. ''x'' ''x'' ''x'') (λ ''x''. ''x'' ''x'' ''x'')) </tt>
como Ω2, etc.

== Definición formal ==

=== Sintaxis ===

En el cálculo lambda, una ''expresión'' o ''término'' se define [[Recursión|recursivamente]] a través de las siguientes reglas de formación:

# Toda variable es un término: <tt>x, y, z, u, v, w, x1, x2, y9,...</tt>
# Si <tt>t</tt> es un término y <tt>x</tt> es una variable, entonces <tt>(λx.t)</tt> es un término (llamado una ''abstracción lambda'').
# Si <tt>t</tt> y <tt>s</tt> son términos, entonces <tt>(ts)</tt> es un término (llamado una ''aplicación lambda'').
# Nada más es un término.

Según estas reglas de formación, las siguientes [[Cadena de caracteres|cadenas de caracteres]] son términos:

:<tt>x</tt>
:<tt>(xy)</tt>
:<tt>(((xz)y)x)</tt>
:<tt>(λx.x)</tt>
:<tt>((λx.x)y)</tt>
:<tt>(λz.(λx.y))</tt>
:<tt>((x(λz.z))z)</tt>

Por convención se suelen omitir los paréntesis externos, ya que no cumplen ninguna función de desambiguación. Por ejemplo se escribe <tt>(λz.z)z</tt> en vez de <tt>((λz.z)z)</tt>, y se escribe <tt>x(y(zx))</tt> en vez de <tt>(x(y(zx)))</tt>. Además se suele adoptar la convención de que la aplicación de funciones es asociativa hacia la izquierda. Esto quiere decir, por ejemplo, que <tt>xyzz</tt> debe entenderse como <tt>(((xy)z)z)</tt>, y que <tt>(λz.z)yzx</tt> debe entenderse como <tt>((((λz.z)y)z)x)</tt>.

Las primeras dos reglas generan funciones, mientras que la última describe la aplicación de una función a un argumento. Una abstracción lambda <tt>λx.t</tt> representa una función anónima que toma un único argumento, y se dice que el signo <tt>λ</tt> ''liga'' la variable <tt>x</tt> en el término <tt>t</tt>. En cambio, una aplicación lambda <tt>ts</tt> representa la aplicación de un argumento <tt>s</tt> a una función <tt>t</tt>. Por ejemplo, <tt>λx.x</tt> representa la [[Función Identidad]] <tt>x → x</tt>, y <tt>(λx.x)y</tt> representa la función identidad aplicada a <tt>y<tt>. Luego, <tt>λx.y</tt> representa la función constante <tt>x → y</tt>, que develve <tt>y</tt> sin importar qué argumento se le dé.

Las expresiones lambda no son muy interesantes por sí mismas. Lo que las hace interesantes son las muchas nociones de equivalencia y reducción que pueden ser definidas sobre ellas.

== Variables libres y ligadas ==

Las apariciones (ocurrencias) de variables en una
expresión son de tres tipos:

# Ocurrencias de ligadura (binders)
# Ocurrencias ligadas (bound occurrences)
# Ocurrencias libres (free occurrences)

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

<tt> (λ ''x y z''. E)</tt>
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:

# En expresiones de la forma <tt> ''V''</tt>,  donde <tt>''V''</tt> es una variable, <tt>''V''</tt> es una ocurrencia libre.
# En expresiones de la forma <tt> λ ''V''. ''E''</tt>,  las ocurrencias son libres en <tt>''E''</tt> salvo aquellas de <tt>''V''</tt>. En este caso las <tt>''V''</tt> en <tt>''E''</tt> se dicen ligadas por el <tt>λ</tt> antes <tt>''V''</tt>.
# En expresiones de la forma <tt> (''E'' ''E′'')</tt>,  las ocurrencias libres son aquellas ocurrencias de <tt>''E''</tt> y <tt>''E′''</tt>.

Expresiones lambda tales como <tt> λ ''x''. (''x'' ''y'') </tt> no definen funciones porque las ocurrencias de <tt>''y''</tt> 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: <tt> (λx.x(λx.x))x</tt>, 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í <tt> (λy.y(λz.z))x</tt>

== α-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 <tt> λ''x''.''x'' </tt> y <tt> λ''y''.''y'' </tt> 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ómemo se conoce como '''captura de variables'''.

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

<tt>''E''[''V'' := ''W'']</tt>

representa la expresión <tt>''E''</tt> con todas las ocurrencias libres de <tt>''V''</tt> en <tt>''E''</tt> reemplazadas con <tt>''W''</tt>, entonces

: <tt>λ ''V''. ''E''  ==  λ ''W''. ''E''[''V'' := ''W'']</tt>

si <tt>''W''</tt> no está libre en <tt>''E''</tt> y <tt>''W''</tt> no está ligada a un <tt>λ</tt> donde se haya reemplazado a V. Esta regla nos dice, por ejemplo, que <tt> λ ''x''. (λ ''x''. ''x'') ''x'' </tt> es equivalente a <tt> λ ''y''. (λ ''x''. ''x'') ''y''</tt>.

En un ejemplo de otro tipo, se ve que

<tt>for (int i = 0; i < max; i++) { proc (i); }</tt>

es equivalente a

<tt>for (int j = 0; j < max; j++) { proc (j); }</tt>

== β-reducción ==

La regla de beta reducción expresa la idea de la aplicación funcional. Enuncia que

: <tt>((λ ''V''. ''E'') ''E′'')  ==  ''E''[''V'' := ''E′'']</tt>
si todas las ocurrencias de <tt>''E′''</tt> están libres en <tt>''E''[''V'' := ''E′'']</tt>.

Una expresión de la forma <tt>((λ ''V''. ''E'') ''E′'')</tt> 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 tercer regla, eta 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 <tt> λ ''x''. ''f'' ''x'' </tt> y <tt> ''f'' </tt> siempre que <tt>''x''</tt> no aparezca sola en <tt>''f''</tt>. Esto puede ser entendido como equivalente a la extensionalidad así:

Si <tt>''f''</tt> y <tt>''g''</tt> son extensionalmente equivalentes, es decir, si <tt> ''f'' ''a''== ''g'' ''a'' </tt> para cualquier expresión lambda <tt>''a''</tt> entonces, en particular tomando <tt>''a''</tt> como una variable <tt>''x''</tt> que no aparece sola en <tt>''f''</tt> ni en <tt>''g''</tt>, tenemos que <tt> ''f'' ''x''  == ''g'' ''x'' </tt> y por tanto <tt> λ ''x''. ''f'' ''x'' ==  λ ''x''. ''g'' ''x''</tt>,  y así por eta conversión <tt> ''f''  == ''g''</tt>.  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 <tt>''y''</tt> tenemos que <tt> (λ ''x''. ''f'' ''x'') ''y'' ==  ''f'' ''y''</tt>,  resulta que <tt> λ ''x''. ''f'' ''x''   ==  ''f''</tt>;  es decir, descubrimos que la eta conversión es válida.

== Conclusiones ==

El cálculo lambda es computacionalmente equivalente en poder a muchos otros modelos plausibles para el cómputo (máquinas de Turing incluídas); 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. Según la tesis de Church-Turing, ambos modelos pueden expresar cualquier cómputo posible.

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.

== Véase También ==

*[[Python]]
*[[Lenguaje de programación Haskell]]
*[[Programación lógica]]
*[[Programación Correcta]]

== Fuentes ==

*[http://ceciliaurbina.blogspot.com/2010/11/calculo-lambda.html Cálculo Lambda]
*[http://enciclopedia.us.es/index.php/C%C3%A1lculo_lambda Cálculo Lambda]

[[Category:Informática]]

@@ Línea 146: / Línea 146: @@
 si todas las ocurrencias de <tt>''E′''</tt> están libres en <tt>''E''[''V'' := ''E′'']</tt>.
-Una expresión de la forma <tt>((λ ''V''. ''E'') ''E′'')</tt> 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)
+Una expresión de la forma <tt>((λ ''V''. ''E'') ''E′'')</tt> 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 ==

@@ Línea 46: / Línea 46: @@
 En el cálculo lambda, las funciones están definidas por expresiones lambda, que dicen qué se hace con su argumento. Por ejemplo, la función "sumar 2", <tt>&nbsp;''f''(''x'') = ''x'' + 2&nbsp;</tt> se expresa en cálculo lambda así: <tt>&nbsp;λ ''x''. ''x'' + 2&nbsp;</tt> (o, equivalentemente, <tt>&nbsp;λ ''y''. ''y'' + 2</tt>
-ya que el nombre de su argumento no es importante). Y el número <tt>''f''(3)</tt> sería escrito como <tt>&nbsp;(λ ''x''. ''x'' + 2) 3</tt>. La aplicación de funciones es [[asociatividad|asociativa]] a izquierda: <tt>&nbsp;''f'' ''x'' ''y'' = (''f'' ''x'') ''y''</tt>.&nbsp;
+ya que el nombre de su argumento no es importante). Y el número <tt>''f''(3)</tt> sería escrito como <tt>&nbsp;(λ ''x''. ''x'' + 2) 3</tt>. La aplicación de funciones es asociativa a izquierda: <tt>&nbsp;''f'' ''x'' ''y'' = (''f'' ''x'') ''y''</tt>.&nbsp;
 Considerando la función que aplica una función al número <tt>3</tt>:<tt>&nbsp;λ ''f''. ''f'' 3</tt>.&nbsp;, podemos pasarle "sumar 2", quedando así: <tt>&nbsp;(λ ''f''. ''f'' 3) (λ ''x''. ''x'' + 2)</tt>.&nbsp;
@@ Línea 52: / Línea 52: @@
 : <tt>(λ ''f''. ''f'' 3)(λ ''x''. ''x'' + 2)&nbsp;&nbsp;&nbsp;</tt>, <tt>&nbsp;&nbsp;&nbsp;(λ ''x''. ''x'' + 2) 3&nbsp;&nbsp;&nbsp;</tt> y <tt>&nbsp;&nbsp;&nbsp;3 + 2&nbsp;&nbsp;&nbsp;</tt>
 son equivalentes.
-<!-- Una función de dos variables puede ser expresada en cálculo lambda como una función de un solo argumento (véase [[Currificación]]). Por ejemplo, la función <tt>&nbsp;''f''(''x'', ''y'') = ''x'' - ''y''&nbsp;</tt> puede ser escrita como <tt>&nbsp;λ ''x''. λ ''y''. ''x'' - ''y''</tt>. Una forma de abreviación común de funciones currificadas es esta <tt>&nbsp;λ ''x'' ''y''. ''x'' - ''y''</tt>. -->
+<!-- Una función de dos variables puede ser expresada en cálculo lambda como una función de un solo argumento. Por ejemplo, la función <tt>&nbsp;''f''(''x'', ''y'') = ''x'' - ''y''&nbsp;</tt> puede ser escrita como <tt>&nbsp;λ ''x''. λ ''y''. ''x'' - ''y''</tt>. Una forma de abreviación común de funciones currificadas es esta <tt>&nbsp;λ ''x'' ''y''. ''x'' - ''y''</tt>. -->
 No todas las expresiones lambda pueden ser reducidas a un "valor" definido. Considérese la siguiente:
@@ Línea 69: / Línea 69: @@
 === Sintaxis ===
-En el cálculo lambda, una ''expresión'' o ''término'' se define [[Recursión|recursivamente]] a través de las siguientes reglas de formación:
+En el cálculo lambda, una ''expresión'' o ''término'' se define recursivamente a través de las siguientes reglas de formación:
 # Toda variable es un término: <tt>x, y, z, u, v, w, x<sub>1</sub>, x<sub>2</sub>, y<sub>9</sub>,...</tt>
@@ Línea 76: / Línea 76: @@
 # Nada más es un término.
-Según estas reglas de formación, las siguientes [[Cadena de caracteres|cadenas de caracteres]] son términos:
+Según estas reglas de formación, las siguientes cadenas de caracteres son términos:
 :<tt>x</tt>
@@ Línea 146: / Línea 146: @@
 si todas las ocurrencias de <tt>''E′''</tt> están libres en <tt>''E''[''V'' := ''E′'']</tt>.
-Una expresión de la forma <tt>((λ ''V''. ''E'') ''E′'')</tt> 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)
+Una expresión de la forma <tt>((λ ''V''. ''E'') ''E′'')</tt> 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 ==

@@ Línea 1: / Línea 1: @@
-<div align="justify">
 {{Definición
 |nombre=  Cálculo Lambda

← Revisión anterior		Revisión del 17:50 29 sep 2011
Línea 1:		Línea 1:
		+	<div align="justify">
	{{Definición		{{Definición
	\|nombre= Cálculo Lambda		\|nombre= Cálculo Lambda

Cálculo lambda - Historial de revisiones

Javiermartin jc: Texto reemplazado: «» por «»

Pinar1 jc en 17:50 29 sep 2011

Pinar1 jc: /* β-reducción */

Pinar1 jc: /* η-conversión */

Pinar1 jc: /* Definición formal */

Pinar1 jc: /* Definición Informal */

Pinar1 jc: /* β-reducción */

Pinar1 jc: Página creada con '{{Definición |nombre= Cálculo Lambda |imagen= |tamaño= |concepto= Es el lenguaje de programación mas pequeño consiste en transformación simple(sustituir variables) y en d...'

Javiermartin jc: Texto reemplazado: «
» por «»