Càlcul lambda

Térmens enllaçats en funcions de recursión.

En llògica matemàtica, el càlcul lambda és un sistema formal dissenyat per a investigar la definició de funció, la noció d'aplicació de funcions i la recursión. Va ser introduït per Alonzo Church i Stephen Kleene en la década de 1930 com a part de les seues investigacions sobre els fonaments de les matemàtiques. Church va usar el càlcul lambda en 1936 per a resoldre l'Entscheidungsproblem. Pot ser usat per a definir de manera neta i precisa qué és una "funció computable".

L'interrogant de si dos expressions del càlcul lambda són equivalents no pot ser resolt per un algoritme general. Esta va ser la primera pregunta, inclús abans que el problema de la parada, que la seua indecidibilidad va ser provada. El càlcul lambda té una gran influència sobre els llenguages funcionals, com Lisp, ML i Haskell.

Es pot considerar al càlcul lambda com un dels llenguages universals de programació més minimalistes. Consistix en una regla de transformació simple (substitució de variables) i un esquema simple per a definir funcions.

El càlcul lambda és universal perque qualsevol funció computable pot ser expressada i evaluada a través d'ell. Per lo tant, és equivalent a les màquines de Turing. No obstant, el càlcul lambda no fa émfasis en l'us de regles de transformació i no considera les màquines reals que poden implementar-ho. Es tracta d'una proposta més propenca al software que al hardware.

Este artícul s'enfocarà sobre el càlcul lambda sense tipos, com va ser dissenyat originalment per Church. Des de llavors, alguns càlcul lambda tipados varen ser creats.

Història

Originalment, Church havia tractat de construir un sistema formal complet per a modelizar la matemàtica; pero en 1934 Kleene i Rosser varen publicar una implementació de la paradoxa de Richard. Des d'eixe punt, el càlcul lambda va ser usat per a estudiar la computabilidad, culminant en la resposta negativa al problema de la parada. En 1940, Church va introduir el Càlcul lambda simplement tipado que és computacionalment menys poderós, pero llògicament consistent.

Introducció informal

Considere's les següents dos funcions. Per un costat, la funció identitat I(x) = x, que pren un únic argument, x, i immediatament torna x. Per un atre costat, la funció suma S(x,i) = x + i, que pren dos arguments, x i i, i torna la suma d'abdós: x + i. Usant estes dos funcions com a eixemple, és possible fer algunes observacions útils sobre vàries idees fonamentals del càlcul lambda.

La primera observació és que les funcions no necessiten ser explícitament nomenades. Açò és, la funció S(x,i) = x + i pot ser reescrita com una funció anònima: x,i → x + i (que es llig: «el parell de x i i es mapea a x + i»). De la mateixa manera, I(x) = x pot ser reescrita de forma anònima com a x → x, que es llig: «l'argument x es mapea a sí mateixa».

La segona observació és que el nom que s'assigne als arguments de la funció és generalment irrellevant. Açò és, x → x i i → i expressen la mateixa funció: la funció identitat. De la mateixa manera, x,i → x + i i o,v → o + v expressen la mateixa funció: la funció suma.

Una tercera observació és que tota funció que requerix dos arguments, com per eixemple la funció suma, pot ser reescrita com una funció que accepta un únic argument, pero que torna una atra funció, la qual a la seua volta accepta un únic argument. Per eixemple, x,i → x + i pot ser reescrita com a x → (i → x + i). Esta transformació es coneix com currificación, i pot generalisar-se per a funcions que accepten qualsevol número d'arguments. Açò pot semblar difícil d'entendre, pero s'entén millor per mig d'un eixemple. Considere's la funció suma no currificada:

x,i → x + i

En prendre als números 2 i 3 com a arguments, s'obté:

2 + 3

La qual cosa és igual a 5. Considere's ara la versió currificada de la funció:

x → (i → x + i)

Si es pren al número 2 com a argument, s'obté la funció:

i → 2 + i

I prenent després al número 3 com a argument, s'obté:

2 + 3

La qual cosa és igual a 5. De modo que la versió currificada torna el mateix resultat que la versió no currificada. En el càlcul lambda, totes les expressions representen funcions anònimes d'un sol argument.

Una quarta observació és que una funció pot acceptar com a argument a una atra funció, sempre i quan esta atra funció tinga ella mateixa un sol argument. Per eixemple, la funció identitat pot acceptar com a argument a la funció suma (currificada). És dir, es pren a la funció x → (i → x + i) i li la posa com a argument en z → z. El resultat serà òbviament x → (z → x + z), (igual a la x → (i → x + i)) puix la funció identitat sempre torna lo mateix que se li dona.

En el càlcul lambda, les funcions estan definides per expressions lambda, que diuen qué es fa en el seu argument. Per eixemple, la funció "sumar 2",  f(x) = x + 2  s'expressa en càlcul lambda aixina:  λ x. x + 2  (o, equivalentemente,  λ i. i + 2 ya que el nom del seu argument no és important). I el número f(3) seria escrit com  (λ x. x + 2) 3. L'aplicació de funcions és associativa a esquerra:  f x i = (f x) i.  Considerant la funció que aplica una funció al número 3: λ f. f 3. , podem passar-li "sumar 2", quedant aixina:  (λ f. f 3) (λ x. x + 2). 

Les tres expressions:

(λ f. f 3)(λ x. x + 2)   ,    (λ x. x + 2) 3    i    3 + 2   

són equivalents.

No totes les expressions lambda poden ser reduïdes a un "valor" definit. Considere's la següent:

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

o

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

tractar de reduir estes expressions solament du a trobar-se en la mateixa expressió o alguna cosa més complex.  (λ x. x x)  és conegut com ω combinador; ((λ x. x x) (λ x. x x))  es coneix com Ω,  ((λ x. x x x) (λ x. x x x))  com Ω₂, etc.

Referències

• Abelson, Harold & Gerald Jay Sussman. Structure and Interpretation of Computer Programs. [[The MIT Press]]. ISBN 0-262-51087-1.

• Barendregt, Henk, The lambda calculus, its syntax and semantics, North-Holland (1984), is the comprehensive reference on the (untyped) lambda calculus; see also the paper Introduction to Lambda Calculus.
• Barendregt, Henk, The Type Free Lambda Calculus pp1091-1132 of Handbook of Mathematical Logic, North-Holland (1977) ISBN 0-7204-2285-X
• Church, Alonzo, An unsolvable problem of elementary number theory, American Journal of Mathematics, 58 (1936), pp. 345-363. This paper contains the proof that the equivalence of lambda expressions is in general not decidable.
• Clinger, William, Foundations of Actor Semantics. MIT Mathematics Doctoral Dissertation, June 1981.
• Punit, Gupta, Amit & Ashutosh Agte, Untyped lambda-calculus, alpha-, beta- and eta- reductions and recursion
• Henz, Martin, The Lambda Calculus. Formally correct development of the Lambda calculus.
• Hewitt, Carl, What is Commitment? Physical, Organizational, and Social
• Archivat el 11 de febrer de 2021 archivat en Wayback Machine. COINAAMAS. April 27, 2006.
• Kleene, Stephen, A theory of positive integers in formal logic, American Journal of Mathematics, 57 (1935), pp. 153-173 and 219-244. Contains the lambda calculus definitions of several familiar functions.
• Landin, Peter, A Correspondence Between ALGOL 60 and Church's Lambda-Notation, Communications of the ACM, vol. 8, no. 2 (1965), pages 89-101. Available from the ACM site. A classic paper highlighting the importance of lambda-calculus as a basis for programming languages.
• Larson, Jim, An Introduction to Lambda Calculus and Scheme. A gentle introduction for programmers.

Some parts of this article llaure based on material from FOLDOC, used with permission.

• Miguel Ángel Jiménez Santana, Lambda Calculus Graphical Interpreter