Lògica combinatòria

De Viquipèdia
Dreceres ràpides: navegació, cerca
Per a altres significats vegeu «Lògica (desambiguació)».

La lògica combinatòria és la lògica última i com a tal pot ser un model simplificat del còmput, usat en la teoria de computabilitat (l'estudi de què pot ser computat) i la teoria de la prova (l'estudi de què es pot provar matemàticament .)

Introducció[modifica | modifica el codi]

La teoria, a causa del seu simplicitat, captura les característiques essencials de la naturalesa del còmput. La lògica combinatòria ( LC ) és el fonament del càlcul lambda, en eliminar el darrer tipus de variable d'aquest: la variable lambda. En LC les expressions lambda (usades per a permetre l'abstracció funcional) són substituïdes per un sistema limitat de combinacions, les funcions primitives que no contenen cap variable lliure ( ni lligada ). És fàcil transformar expressions lambda en expressions combinatòries, i ja que la reducció d'un combinat és més simple que la reducció lambda, LC s'ha utilitzat com la base per a la posada en pràctica d'alguns llenguatges de programació funcionals no estrictes en programari i maquinari.

Sumari del càlcul lambda[modifica | modifica el codi]

El càlcul lambda es refereix a objectes anomenats lambda-termes, que són cadenes de símbols d'una de les formes següents:

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

on v és un nom de variable pres d'un conjunt infinit predefinit de noms de variables, i E1 i E2 són lambda-termes. Els termes de la forma λv.E1 són anomenades abstraccions. La variable ν es diu el paràmetre formal de l'abstracció, i E1 és el cos de l'abstracció.

El terme λv.E1 representa la funció que, si és aplicada a un argument, lliga el paràmetre formal v a l'argument i llavors computa el valor resultant de E1 --- és a dir, retorna E1 , amb cada ocurrència de ν substituït per l'argument.

Els termes de la forma (E1 E2) són anomenats aplicacions. Les aplicacions modelen la invocació o execució d'una funció: La funció representada per E1 és invocada, amb E2 com el seu argument, i es computa el resultat. Si E1 (de vegades anomenat el aplicant) és una abstracció, el terme pot ser reduït: E2 , l'argument, es pot substituir en el cos de E1 en lloc del paràmetre formal de E1 , i el resultat és un nou terme lambda que és equivalent a l'antic. Si un terme lambda no conté cap subterme de la forma (λv.E1 E2) llavors no pot ser reduït, i es diu que està en forma normal .

L'expressió E [a/v] representa el resultat de prendre el terme E i substituint totes les ocurrències lliures de v pel a . Escrivim així

 (λv.E a) ⇒ E [a/v] 

per convenció, prenem (bc d. .. z) com abreviatura per (... (((ab) c) d) ... z). ( Reglament d'associació per esquerra).

La motivació per a aquesta definició de la reducció és que captura el comportament essencial de totes les funcions matemàtiques. Per exemple, considereu la funció que computa el quadrat d'un nombre. Es pot escriure el quadrat de x és x * x (usant "*" per indicar la multiplicació.) x aquí és el paràmetre formal de la funció. Per avaluar el quadrat per a un argument particular, diguem 3, el inserim en la definició en lloc del paràmetre formal:

El quadrat de 3 és 3 * 3

per avaluar l'expressió que resulta 3 * 3, hauríem de recórrer al nostre coneixement de la multiplicació i del nombre 3. Com que qualsevol còmput és simplement una composició de l'avaluació de funcions adequades amb arguments primitius adequats, aquest principi simple substitució és suficient per capturar el mecanisme essencial del còmput. D'altra banda, en el càlcul lambda, nocions com ara '3 'i' * 'pot ser representat sense cap necessitat d'operadors primitius externament definides o de constants. És possible identificar els termes que en el càlcul lambda, quan estan interpretats convenientment, es comporten com el número 3 i l'operador de la multiplicació.

El càlcul lambda és computacionalment equivalent en poder a molts altres models plausibles per al còmput (màquines de Turing incloses), és a dir, qualsevol càlcul que es pugui aconseguir en qualsevol d'aquests altres models es pot expressar en el càlcul lambda, i viceversa. Segons la tesi de Church-Turing, tots dos models poden expressar qualsevol còmput possible. Potser sembli sorprenent que el càlcul lambda pugui representar qualsevol còmput concebible usant només les nocions simples d'abstracció funcional i aplicació basat en la substitució textual simple de termes per variables . Però encara més notable és que fins i tot l'abstracció no és requerit . La Lògica Combinatòria és un model del còmput equivalent al càlcul lambda , però sense l'abstracció .

Càlculs combinatoris[modifica | modifica el codi]

Com que l'abstracció és l'única manera de fabricar funcions en el càlcul lambda, alguna cosa ha de substituir en el càlcul combinatori. En comptes de l'abstracció, el càlcul combinatori proporciona un conjunt limitat de funcions primitives i de les quals les altres funcions poden ser construïdes.

Termes combinatoris[modifica | modifica el codi]

Un terme combinatori té una de les formes següents:

  • V
  • P
  • (E1 E2)

on V és una variable, P és una de les funcions primitives, E1 i E2 són termes combinatoris. Les funcions primitives mateixes són combinats, o funcions que no contenen cap variable lliure.

Exemples de combinadors[modifica | modifica el codi]

L'exemple més simple d'un combinat és I , el Combinator identitat , definit per

( I   x ) =  x 

per a tots els termes x . altre Combinator simple és K , que produeix funcions constants: ( K x ) és la funció que, per a qualsevol argument, torna x , així que diem

(( K   x )  i ) =  x 

per a tots els termes x i i . O, seguint la mateixa convenció per a l'ús múltiple que en el càlcul lambda,

( K   x   i ) =  x 

Un tercer combinador és S , que és una versió generalitzada de l'aplicació:

( S   x   i   z ) = ( x   z  ( i   z ))

S s'aplica x a i després de substituir primer az en cada un d'ells.

Donats S i K , tot el mateix I és innecessari, ja que pot ser construït pels altres dos:

(( S   K   K )  x )
= ( S   K   K   x )
= ( K   x  ( K   x ))
=  x 

per altra paraula x . Noteu que encara que (( S K K ) x ) = ( I x ) per a qualsevol x , ( S K K ) en si mateix no és igual a I . Diem que els termes són extensionalmente iguals.

La igualtat extensional[modifica | modifica el codi]

La igualtat extensional captura la noció matemàtica de la igualtat de funcions: que dues funcions són 'iguals' si produeixen sempre els mateixos resultats per les mateixos arguments. En contrast, els termes mateixos capturen la noció d'igualtat intensionals de funcions: que dues funcions són 'iguals' només si tenen implementacions idèntiques. Hi ha moltes maneres d'implementar una funció identitat; ( S K K ) i I estan entre aquestes maneres. ( S K S ) és un altre. Utilitzarem la paraula equivalent per indicar la igualtat extensional, reservant igual pels termes combinatoris idèntics.

Un combinat més interessant és el combinador de punt fix o Combinator I , que es pot utilitzar per implementar la recursió.

Completesa de la base S-K[modifica | modifica el codi]

És, potser, un fet sorprenent que S i K es puguin compondre per produir els combinats que són extensionalmente iguals a qualsevol terme lambda, i per tant, per la tesi de Church, a qualsevol funció computable. La prova és presentar una transformació, T [], que converteix un terme arbitrari lambda en un combinador equivalent. T [] pot ser definit com segueix: T [ V ] ⇒ V T [( E1 E2 )] ⇒ ( T [ E1 ] T [ E2 ]) Tx . E ] ⇒ ( K E ) (si x no està lliure en E) Tx . x ] ⇒ I Tx . Λ i . E ] ⇒ Tx . T λ '' i ''. '' E '' (si x està lliure a E) Tx . ( E1 E2 )] ⇒ ( S Tx . E1 ] Tx . E2 ])

Conversió d'un terme lambda a un terme combinatori equivalent[modifica | modifica el codi]

Per exemple, convertirem el terme lambda λ x . Λ i . ( i x ) a un combinador:

 T  [ λx .  λy . ( i   x )]
=  T  [ λx .  T  [ λy . ( i   x )] (per 5)
=  T  [ λx . ( S   T  [ λy .  i ]  T  [ λy .  x ])] (per 6)
=  T  [ λx . ( S   R   T  [ λy .  x ])] (per 4)
=  T  [ λx . ( S   I  ( K   x ))] (per 3)
= ( S   T  [ λx . ( S   I )]  T  [ λx . ( K   x )]) (per 6)
= ( S  ( K  ( S   I ))  T  [ λx . ( K   x )]) (per 3)
= ( S  ( K  ( S   I )) ( S   T  [ λx .  K ]  T  [ λx .  x ])) (per 6)
= ( S  ( K  ( S   I )) ( S  ( K   K )  T  [ λx .  x ])) (per 3)
= ( S  ( K  ( S   I )) ( S  ( K   K )  I )) (per 4)

si apliquem aquest Combinator a qualsevol dos termes x i i , redueix la manera següent:

( S  ( K  ( S   I )) ( S  ( K   K )  I ) x i)
= ( K  ( S   I ) x ( S  ( K   K )  I  x) i)
= ( S   I  ( S  ( K   K )  I  x) i)
= ( I  i ( S  ( K   K )  I  x i))
= (I ( S  ( K   K )  I  x i))
= (I ( K   K  x ( I  x) i))
= (I ( K  ( I  x) i))
= (I ( I  x))
= (I x)

La representació combinatòria, ( S ( K ( S I )) ( S ( K K ) I )) és molt més llarga que la representació com a terme lambdaλ x . λ i . ( i x ). Això és típic. En general, la construcció de T [] pot ampliar un terme lambda de la longitud na[Aclariment necessari] un terme combinatori de la longitud Θ (3 n ).

Explicació de la transformació T [][modifica | modifica el codi]

La transformació T [] és motivada per un desig d'eliminar l'abstracció. Dos casos especials, regles 3 i 4, són trivials: λ x . x és clarament equivalent a R, i λ x . E és clarament equivalent a (KE) si x no apareix lliure en E.

Les dues primeres regles són també simples: Les variables es converteixen en si mateixes, i les aplicacions permeses en termes combinatoris, són convertides els combinadors simplement convertint el aplicant i l'argument a combinadors.

Són les regles 5 i 6 les que tenen interès. La regla 5 diu simplement això: per convertir una abstracció complexa a un combinat, hem de primer convertir el seu cos a un Combinator, i després eliminem l'abstracció. La regla 6 elimina realment l'abstracció.

λ x . (E1E2) és una funció que pren un argument, diguem a , i el substitueix al terme lambda (E1 E2) en lloc de x , donant (E1 E2) [ a / x ]. Però substituir a (E1 E2) en lloc de x és precisament igual que substituir-lo en E1 i E2, així que

( E1   E2 ) [ a / x ] = ( E1  [ a / x ]  E2  [ a / x ])


( λx . ( E1   E2 )  a ) = (( λx .  E1   a ) ( λx .  E2   a ))
= ( S   λx .  E1   λx .  E2   a )
= (( S   λx .  E1   λx .  E2 )  a )

Per igualtat extensional,

 λx . ( E1   E2 ) = ( S   λx .  E1   λx .  E2 )

Per tant, per trobar un combinador equivalent a λx . ( E1 E2 ), n'hi ha prou trobar un combinador equivalent a ( S λx . E1 λx . E2 ), i

( S   T  [ λx .  E1 ]  T  [ λx .  E2 ])

evidentment compleix l'objectiu. E1 i E2 contenen cadascun estrictament menys aplicacions que (E1 E2) , així que la repetició ha d'acabar en un termini lambda sense aplicació cap-ni una variable, ni un terme de la forma λ x . E .

Simplificacions de la transformació[modifica | modifica el codi]

Η-reducció[modifica | modifica el codi]

Els combinadors generats per la transformació T [] poden ser fets més petits si considerem la regla de η-reducció:

 T  [ λx . ( E   x )] =  T  [ E ] (si  x  no està lliure en  E )

'' λx ''. ('' E '' x) és la funció que pren un argument, x, i aplica la funció E a ell, és a dir extensionalmente igual a la funció E mateixa. És per tant prou convertir E a la forma combinatòria.

Prenent aquesta simplificació en compte, l'exemple dalt es converteix en:
 T  [ λx .  λy . ( i   x )]
= ...
= ( S  ( K  ( S   I ))  T  [ λx . ( K   x )])
= ( S  ( K  ( S   I ))  K ) (per η-reducció)

Aquest combinador és equivalent a l'anterior, més llarg:

( S  ( K  ( S   I ))  K   x   i )
= ( K  ( S   I )  x  ( K   x )  i )
= ( S   I  ( K   x )  i )
= ( I   i  ( K   x   i ))
= ( i  ( K   x   i ))
= ( i   x )

semblantment, la versió original de la transformació T [] transformar la funció identitat λf . λx . ( f x ) a ( S ( S ( K S ) ( S ( K K ) I )) ( K I )). Amb la regla de η-reducció, λf . λx . ( f x ) es va transformar en I .


Els combinadors B, C de Curry[modifica | modifica el codi]

Els combinadors S , K es troben ja en Schönfinkel (tot i que el símbol C s'usava per l'actual K ) Curry va introduir l'ús de B , C , W (i K ), ja abans de la seva tesi doctoral de 1930 . En Lògica combinatòria T. I , S'ha tornat a S , K però es mostra, (via algorismes de Markov) que l'ús de B i C poden simplificar moltes reduccions. Això sembla haver-se utilitzat molt després per David Turner, el nom ha quedat lligat al seu ús computacional. S'introdueixen dos nous combinadors:

( C   a   b   c ) = ( a   c   b )
( B   a   b   c ) = ( a  ( b   c ))

Usant aquests combinats, podem estendre les regles per a la transformació de la manera següent:

  1. T [ V ] ⇒ V
  2. T [( E1 E2 )] ⇒ ( T [ E1 ] T [ E2 ])
  3. T [ λx . E ] ⇒ ( K E ) (if x no està lliure en E )
  4. T [ λx . x ] ⇒ I
  5. T [ λx . λy . E ] ⇒ T [ λx . T '' λy ''. '' E '' (en cas de x està lliure en E )
  6. T [ λx . ( E1 E2 )] ⇒ ( S T [ λx . E1 ] T [ λx . E2 ]) (si x està lliure tant en E1 com en E2 )
  7. T [ λx . ( E1 E2 )] ⇒ ( C T [ λx . E1 ] E2 ) (si x està lliure en E1 però no en E2 )
  8. T [ λx . ( E1 E2 )] ⇒ ( B E1 T [ λx . E2 ]) (si x està lliure en E2 però no en E1 )

Usant els combinadors B i C , la transformació de λx . λy . ( i x ) es veu així:

 T  ( λx .  λy . ( i   x ))
=  T  ( λx .  T  ( λy . ( i   x )))
=  T  ( λx . ( C   T  [ λy .  i )  x )) (per la regla 7)
=  T  ( λx . ( C   R   x ))
= ( C   I ) (η-reducció)
= C  *  (notació canònica tradicional: X  *  = XI)
= I '(notació canònica tradicional: X' = CX)

I, certament, ( C R x i ) es redueix a ( i x ):

( C   R   x   i )
= ( I   i   x )
= ( i   x )


La motivació aquí és que B i C són versions limitades de S . Mentre S pren un valor i el substitueix tant en el aplicant com en l'argument abans d'efectuar l'aplicació, C realitza la substitució només en el aplicant, i B només en l'argument.

Conversió inversa[modifica | modifica el codi]

La conversió L [] de termes combinatoris a termes lambda és trivial:

 L  [ I ] =  λx .  x 
 L  [ K ] =  λx .  λy .  x 
 L  [ C ] =  λx .  λy .  λz . ( x   z   i )
 L  [ B ] =  λx .  λy .  λz . ( x  ( i   z ))
 L  [ S ] =  λx .  λy .  λz . ( x   z  ( i   z ))
 L  [( E1   E2 )] = ( L  [ E1 ]  L  [ E2 ])

Noteu, però, que aquesta transformació no és la transformació inversa de cap de les versions de T [] que s'han vist.

Indecidibilitat del Càlcul combinatori[modifica | modifica el codi]

És indecidible quan un terme combinatori general té forma normal, quan dos termes combinatoris són equivalents, etc. Això és equivalent a la indecidibilitat dels corresponents problemes per termes lambda. No obstant això, una prova directa és la manera següent:

Primer, observeu que el terme

 A  = ( S   I   I  ( S   I   I ))

no té forma normal, perquè es redueix a si mateix en tres passos, la manera següent:

( S   I   I  ( S   I   I ))
= ( I  ( S   I   I ) ( I  ( S   I   I )))
= ( S   I   I  ( I  ( S   I   I )))
= ( S   I   I  ( S   I   I ))

i clarament cap altre ordre de reducció pot fer l'expressió més curta.

Ara, suposem que N fos un combinador per detectar formes normals, tal que

( N   x ) ⇒  T , si  x  té forma normal
 F , en cas contrari.

(On T i F són les transformacions de les definicions convencionals en càlcul lambda de veritable i fals, λx . λy . x i λx . λy . i . Les versions combinatòries tenen T = K i F = (KI) = 0 = K '.)

Ara sigui

 Z  = ( C  ( C  ( B   N  ( S   I   I ))  A )  I )

i considerem el terme ( S I I Z ). Té ( S I I Z ) una manera normal? La té si i només si:

( S   I   I   Z )
= ( I   Z  ( I   Z ))
= ( Z  ( I   Z ))
= ( Z   Z )
= ( C  ( C  ( B   N  ( S   I   I ))  A )  I   Z ) (definició de   Z  )
= ( C  ( B   N  ( S   I   I ))  A   Z   I )
= ( B   N  ( S   I   I )  Z   A   I )
= ( N  ( S   I   I   Z )  A   I )

Ara hem d'aplicar N a ( S I I Z ). O bé ( S I I Z ) té una forma normal, o no la té. Si tingués forma normal, llavors es redueix la manera següent:

( N  ( S   I   I   Z )  A   I )
= ( K   A   I ) (definició de  N )
=  A 

però A no té una forma normal, per tant tenim una contradicció. Però si ( S I I Z ) no té una forma normal, es redueix la manera següent:

( N  ( S   I   I   Z )  A   I )
= ( K   R   A   I ) (definició de  N )
= ( I   I )
 I 

el que significa que la forma normal de ( S I I Z ) és simplement I , una altra contradicció. Per tant, l'hipotètic combinador de manera normal N no pot existir.

Vegeu també[modifica | modifica el codi]

Referències[modifica | modifica el codi]