Vés al contingut

Lògica combinatòria

De la Viquipèdia, l'enciclopèdia lliure

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). La teoria, a causa de la seva 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 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 a 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]

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 l'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, cal suposar que es diu 3, s'insereix en la definició en lloc del paràmetre formal:

El quadrat de 3 és 3 * 3,

per avaluar l'expressió que resulta 3 * 3, s'hauria de recórrer al 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 de 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' * 'poden ser representades sense cap necessitat d'operadors primitius externament definits o de constants. És possible identificar els termes que en el càlcul lambda, quan estan interpretats convenientment, es comporten com el nombre 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. Pot ser que 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 a 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]

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]

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]

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 es diu: 

(( 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 . Es diu que els termes són extensionalment iguals.

La igualtat extensional

[modifica]

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 pels 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. S'utilitzarà 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]

És, potser, un fet sorprenent que S i K es puguin compondre per produir els combinats que són extensionalment 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 ]) T [λ x . E ] ⇒ ( K E ) (si x no està lliure en E) T [λ x . x ] ⇒ I T [λ x . Λ i . E ] ⇒ T [λ x . T λ '' i ''. '' E '' (si x està lliure a E) T [λ x . ( E1 E2 )] ⇒ ( S T [λ x . E1 ] T [λ x . E2 ])

Conversió d'un terme lambda a un terme combinatori equivalent

[modifica]

Per exemple, es converteix 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 s'aplica 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[Cal aclariment] un terme combinatori de la longitud Θ (3 n ).

Explicació de la transformació T []

[modifica]

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 l'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, cal primer convertir el seu cos a un Combinator, i després eliminar l'abstracció. La regla 6 elimina realment l'abstracció.

λ x . (E1E2) és una funció que pren un argument, es diu 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]

Η-reducció

[modifica]

Els combinadors generats per la transformació T [] poden ser fets més petits si es considera 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 extensionalment igual a la funció E mateixa. És per tant prou convertir E a la forma combinatòria. 

Prenent aquesta simplificació en compte, l'exemple de 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]

Els combinadors S , K es troben ja en Schönfinkel (tot i que el símbol C s'usava per a 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 de temps 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, es poden 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 l'aplicant com en l'argument abans d'efectuar l'aplicació, C realitza la substitució només en l'aplicant, i B només en l'argument.

Conversió inversa

[modifica]

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]

É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, cal suposar 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 cal considerar 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 s'ha 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 hi ha 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]

Referències

[modifica]
Obtingut de «https://ca.wikipedia.org/w/index.php?title=Lògica_combinatòria&oldid=33111988»