De Wikipedia, la enciclopedia libre
Ir a navegaciónSaltar a buscar

El cálculo del combinador de SKI es una lógica combinatoria , un sistema computacional que puede percibirse como una versión reducida del cálculo lambda no tipificado . Se puede considerar como un lenguaje de programación de computadoras, aunque no es conveniente para escribir software. En cambio, es importante en la teoría matemática de los algoritmos porque es un lenguaje completo de Turing extremadamente simple . Fue introducido por Moses Schönfinkel [1] y Haskell Curry . [2]

Todas las operaciones en el cálculo lambda se pueden codificar mediante eliminación de abstracción en el cálculo SKI como árboles binarios cuyas hojas son uno de los tres símbolos S , K e I (llamados combinadores ).

Aunque la representación más formal de los objetos en este sistema requiere árboles binarios, por lo general se representan, para la tipificación, como expresiones entre paréntesis, ya sea con todos los subárboles entre paréntesis o solo los subárboles secundarios del lado derecho entre paréntesis. Entonces, el árbol cuyo subárbol izquierdo es el árbol KS y cuyo subárbol derecho es el árbol SK generalmente se escribe como (( KS ) ( SK )), o más simplemente como KS ( SK ), en lugar de dibujarse completamente como un árbol ( según lo requiera la formalidad y la legibilidad). Poner entre paréntesis solo el subárbol derecho hace que esta notación sea asociativa a la izquierda: ISK significa (( IS ) K ).

I es redundante, ya que se comporta igual que SKK , pero se incluye por conveniencia.

Descripción informal

De manera informal, y usando la jerga del lenguaje de programación, un árbol ( xy ) se puede considerar como una "función" x aplicada a un "argumento" y . Cuando se "evalúa" ( es decir , cuando la función se "aplica" al argumento), el árbol "devuelve un valor", es decir , se transforma en otro árbol. Por supuesto, los tres de la "función", el "argumento" y el "valor" son combinadores o árboles binarios, y si son árboles binarios, también pueden considerarse funciones siempre que surja la necesidad.

La operación de evaluación se define de la siguiente manera:

( x , y y z representan expresiones hechas a partir de las funciones S , K e I , y establecen valores):

Me devuelve su argumento:

Yo x = x

K , cuando se aplica a cualquier argumento x , produce una función constante de un argumento K x , que, cuando se aplica a cualquier argumento, devuelve x :

K xy = x

S es un operador de sustitución. Toma tres argumentos y luego devuelve el primer argumento aplicado al tercero, que luego se aplica al resultado del segundo argumento aplicado al tercero. Mas claro:

S xyz = xz ( yz )

Ejemplo de cálculo: SKSK se evalúa como KK ( SK ) por la regla S. Entonces, si evaluamos KK ( SK ), obtenemos K por la regla K. Como no se puede aplicar ninguna regla adicional, el cálculo se detiene aquí.

Para todos los árboles xy todos los árboles y , SK xy siempre evaluará ay en dos pasos, K y ( xy ) = y , por lo que el resultado final de evaluar SK xy siempre será igual al resultado de evaluar y . Decimos que SK x e I son "funcionalmente equivalentes" porque siempre dan el mismo resultado cuando se aplican a cualquier y .

A partir de estas definiciones se puede demostrar que el cálculo SKI no es el sistema mínimo que puede realizar por completo los cálculos del cálculo lambda, ya que todas las apariciones de I en cualquier expresión pueden ser reemplazadas por ( SKK ) o ( SKS ) o ( SK lo que sea) y la expresión resultante producirá el mismo resultado. Entonces el " yo " es simplemente azúcar sintáctico . Como I es opcional, el sistema también se conoce como cálculo SK o cálculo combinador SK.

Es posible definir un sistema completo utilizando un solo combinador (inadecuado). Un ejemplo es el combinador de iotas de Chris Barker , que se puede expresar en términos de S y K de la siguiente manera:

ι x = x SK

Es posible reconstruir S , K e I a partir del combinador de iota. Aplicando ι a sí mismo da ιι = ι SK = SSKK = SK ( KK ), que es funcionalmente equivalente a I . K se puede construir mediante la aplicación de ι dos veces para I (que es equivalente a la aplicación de ι a sí mismo): ι (ι (ιι)) = ι (ιι SK ) = ι ( ISK ) = ι ( SK ) = SKSK = K . Aplicando ι una vez más da ι (ι (ι (ιι))) = ι K = KSK = S .

Definición formal

Los términos y derivaciones en este sistema también se pueden definir más formalmente:

Términos : El conjunto T de términos se define de forma recursiva mediante las siguientes reglas.

  1. S , K e I son términos.
  2. Si τ 1 y τ 2 son términos, entonces (τ 1 τ 2 ) es un término.
  3. Nada es un término si no lo requieren las dos primeras reglas.

Derivaciones : una derivación es una secuencia finita de términos definidos recursivamente por las siguientes reglas (donde α y ι son palabras sobre el alfabeto { S , K , I , (,)} mientras que β, γ y δ son términos):

  1. Si Δ es una derivación que termina en una expresión de la forma α ( I β) ι, entonces Δ seguido del término αβι es una derivación.
  2. Si Δ es una derivación que termina en una expresión de la forma α (( K β) γ) ι, entonces Δ seguido del término αβι es una derivación.
  3. Si Δ es una derivación que termina en una expresión de la forma α ((( S β) γ) δ) ι, entonces Δ seguido del término α ((βδ) (γδ)) ι es una derivación.

Suponiendo que una secuencia es una derivación válida para empezar, se puede extender usando estas reglas. [1]

Pasar y citar parámetros recursivos

K = λq.λi.q
cita q e ignora i
S = λx.λy.λz. ((Xz) (yz))
forma un árbol binario cuyos parámetros pueden fluir desde la raíz a las ramas y ser leídos por identityFunc = ((SK) K) o leer un lambda q citado usando Kq.

Expresiones de SKI

Autoaplicación y recursividad

SII es una expresión que toma un argumento y lo aplica a sí mismo:

SII α = I α ( I α) = αα

Una propiedad interesante de esto es que hace que la expresión SII ( SII ) sea irreducible:

SII ( SII ) = I ( SII ) ( I ( SII )) = I ( SII ) ( SII ) = SII ( SII )

Otra cosa que resulta de esto es que te permite escribir una función que aplica algo a la autoaplicación de otra cosa:

( S ( K α) ( SII )) β = K αβ ( SII β) = α ( SII β) = α (ββ)

Esta función se puede utilizar para lograr la recursividad . Si β es la función que aplica α a la autoaplicación de otra cosa, entonces la autoaplicación β realiza α recursivamente sobre ββ. Más claramente, si:

β = S ( K α) ( SII )

luego:

SII β = ββ = α (ββ) = α (α (ββ)) =

La expresión inversa

S ( K ( SI )) K invierte los dos términos siguientes:

S ( K ( SI )) K αβ →
K ( SI ) α ( K α) β →
SI ( K α) β →
Yo β ( K αβ) →
Yo βα →
βα

Lógica booleana

El cálculo del combinador de SKI también puede implementar la lógica booleana en forma de una estructura if-then-else . Una estructura if-then-else consiste en una expresión booleana que es verdadera ( T ) o falsa ( F ) y dos argumentos, tales que:

T xy = x

y

F xy = y

La clave está en definir las dos expresiones booleanas. El primero funciona como uno de nuestros combinadores básicos:

T = K
K xy = x

El segundo también es bastante simple:

F = SK
SK xy = K y (xy) = y

Una vez que se definen verdadero y falso, toda la lógica booleana se puede implementar en términos de estructuras if-then-else .

Boolean NOT (que devuelve el opuesto de un booleano dado) funciona igual que la estructura if-then-else , con F y T como el segundo y tercer valor, por lo que se puede implementar como una operación de sufijo:

NO = ( F ) ( T ) = ( SK ) ( K )

Si esto se pone en una estructura if-then-else , se puede demostrar que tiene el resultado esperado

( T ) NO = T ( F ) ( T ) = F
( F ) NO = F ( F ) ( T ) = T

Boolean OR (que devuelve T si alguno de los dos valores booleanos que lo rodean es T ) funciona igual que una estructura if-then-else con T como segundo valor, por lo que se puede implementar como una operación infija:

O = T = K

Si esto se pone en una estructura if-then-else , se puede demostrar que tiene el resultado esperado:

( T ) O ( T ) = T ( T ) ( T ) = T
( T ) O ( F ) = T ( T ) ( F ) = T
( F ) O ( T ) = F ( T ) ( T ) = T
( F ) O ( F ) = F ( T ) ( F ) = F

Boolean AND (que devuelve T si los dos valores booleanos que lo rodean son T ) funciona igual que una estructura if-then-else con F como tercer valor, por lo que se puede implementar como una operación de sufijo:

Y = F = SK

Si esto se pone en una estructura if-then-else , se puede demostrar que tiene el resultado esperado:

( T ) ( T ) Y = T ( T ) ( F ) = T
( V ) ( F ) Y = T ( F ) ( F ) = F
( F ) ( T ) Y = F ( T ) ( F ) = F
( F ) ( F ) Y = F ( F ) ( F ) = F

Debido a que esto define T , F , NOT (como un operador de sufijo), OR (como un operador de infijo) y AND (como un operador de sufijo) en términos de notación SKI, esto demuestra que el sistema SKI puede expresar completamente la lógica booleana.

A medida que el cálculo de SKI está completo , también es posible expresar NOT , OR y AND como operadores de prefijo:

NO = S ( SI ( KF )) ( KT ) (como S ( SI ( KF )) ( KT ) x = SI ( KF ) x ( KT x ) = I x ( KF x ) T = x FT )
O = SI ( KT ) (como SI ( KT ) xy = I x ( KT x ) y = x T y )
Y = SS ( K ( KF )) (como SS ( K ( KF )) xy = S x ( K ( KF ) x ) y = xy ( KF y ) = xy F )

Conexión con la lógica intuicionista

Los combinadores K y S corresponden a dos axiomas bien conocidos de lógica proposicional :

AK : A → ( B → A ) ,
AS : ( A → ( B → C )) → (( A → B ) → ( A → C )) .

La aplicación de la función corresponde a la regla modus ponens :

MP : de A y A → B , inferir B .

Los axiomas AK y AS y la regla MP son completos para el fragmento implicacional de la lógica intuicionista . Para que la lógica combinatoria tenga como modelo:

Esta conexión entre los tipos de combinadores y los axiomas lógicos correspondientes es un ejemplo del isomorfismo de Curry-Howard .

Ver también

Referencias

  1. ^ 1924. "Über die Bausteine ​​der Mathischen Logik", Mathematische Annalen 92 , págs. 305-316. Traducido por Stefan Bauer-Mengelberg como "Sobre los componentes básicos de la lógica matemática" en Jean van Heijenoort , 1967. A Source Book in Mathematical Logic, 1879-1931 . Universidad de Harvard. Presione: 355–66.
  2. ^ Curry, Haskell Brooks (1930). "Grundlagen der Kombinatorischen Logik" [Fundamentos de la lógica combinatoria]. American Journal of Mathematics (en alemán). Prensa de la Universidad Johns Hopkins. 52 (3): 509–536. doi : 10.2307 / 2370619 . JSTOR  2370619 .
  • Smullyan, Raymond , 1985. Para burlarse de un ruiseñor . Knopf. ISBN 0-394-53491-3 . Una suave introducción a la lógica combinatoria, presentada como una serie de acertijos recreativos utilizando metáforas de observación de aves. 
  • --------, 1994. Diagonalización y autorreferencia . Universidad de Oxford. Prensa. Chpts. 17-20 son una introducción más formal a la lógica combinatoria, con un énfasis especial en los resultados de punto fijo.

Enlaces externos

  • O'Donnell, Mike " El cálculo combinador de SKI como sistema universal " .
  • Keenan, David C. (2001) " Diseccionar un ruiseñor " .
  • Rathman, Chris, " Combinator Birds " .
  • " " Combinadores de arrastrar y soltar (subprograma Java). "
  • A Calculus of Mobile Processes, Part I (PostScript) (por Milner, Parrow y Walker) muestra un esquema para la reducción del gráfico de combinador para el cálculo de SKI en las páginas 25–28.
  • el lenguaje de programación Nock puede verse como un lenguaje ensamblador basado en el cálculo del combinador SK de la misma manera que el lenguaje ensamblador tradicional se basa en las máquinas de Turing. La instrucción Nock 2 (el "operador Nock") es el combinador S y la instrucción Nock 1 es el combinador K. Las otras instrucciones primitivas en Nock (instrucciones 0,3,4,5 y la pseudoinstrucción "cons implícitas") no son necesarias para el cálculo universal, pero hacen que la programación sea más conveniente al proporcionar facilidades para tratar con estructuras de datos de árbol binario y aritmética. ; Nock también proporciona 5 instrucciones más (6,7,8,9,10) que podrían haberse construido a partir de estas primitivas.