cálculo de combinadores SKI

El cálculo combinatorio SKI es un sistema de lógica combinatoria y un sistema computacional . Puede considerarse un lenguaje de programación, aunque no resulta práctico para escribir software. En cambio, es importante en la teoría matemática de algoritmos porque es un lenguaje Turing completo extremadamente simple . Se puede comparar con una versión reducida del cálculo lambda sin tipos . Fue introducido por Moses Schönfinkel ^[¹^] y Haskell Curry ^[²^] .

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 ).

La I en sí misma es redundante y puede expresarse solo con S y K , por ejemplo como SKK , pero su uso a menudo hace que las definiciones sean más cortas y fáciles de entender.

Notación

Aunque la representación más formal de los objetos en este sistema requiere árboles binarios, para simplificar la composición tipográfica, a menudo se representan como expresiones entre paréntesis, como una forma abreviada del árbol que representan. Cualquier subárbol puede ir entre paréntesis, pero generalmente solo se incluyen los subárboles del lado derecho, asumiendo la asociatividad izquierda para cualquier aplicación sin paréntesis. Por ejemplo, ISK significa (( IS ) K ). Usando esta notación, un árbol cuyo subárbol izquierdo es el árbol KS y cuyo subárbol derecho es el árbol SK se puede escribir como KS ( SK ). Si se desea mayor claridad, también se pueden incluir los paréntesis implícitos: (( KS )( SK )).

Descripción informal

De forma informal, y utilizando la jerga de los lenguajes de programación, un árbol ( xy ) puede considerarse como la aplicación de la función x a un argumento y . Al evaluarse ( es decir , cuando la "función" se "aplica" al argumento), el árbol "devuelve un valor", es decir , se transforma en otro árbol. La "función", el "argumento" y el "valor" son combinadores o árboles binarios con nodos de aplicación. Si son árboles binarios, también pueden considerarse funciones, si fuera necesario.

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

( x , y , y z representan expresiones formadas a partir de los combinadores S , K , e I , y posiblemente variables que representan algunas expresiones SKI aún no especificadas ):

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 y , devuelve x :

K xy = x

S es un operador de sustitución. Recibe tres argumentos y devuelve el primer argumento aplicado al tercero, que a su vez se aplica al resultado del segundo argumento aplicado al tercero. Más claramente:

S xyz = xz ( yz )

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

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

A partir de estas definiciones, se puede demostrar que el cálculo SKI, si bien es un sistema minimalista, puede realizar completamente cualquier cálculo del cálculo lambda. Todas las apariciones de I en cualquier expresión pueden reemplazarse por ( SKK ), ( SKS ) o ( SK x ) para cualquier x , y la expresión resultante dará el mismo resultado. Por lo tanto, la " I " es simplemente azúcar sintáctico . Dado que I es opcional, el sistema también se conoce como cálculo SK o cálculo combinatorio SK .

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

ι x = x SK = S (λ x . x S )(λ x . K ) x = S ( S (λ x . x )(λ x . S ))( KK ) x = S ( SI ( KS ))( KK ) x

Es posible reconstruir S , K e I a partir del combinador iota. Aplicando ι a sí mismo se obtiene ιι = ι SK = SSKK = SK ( KK ) que es funcionalmente equivalente a I . K se puede construir aplicando ι dos veces a I (lo que es equivalente a aplicar ι a sí mismo): ι(ι(ιι)) = ι(ιι SK ) = ι( ISK ) = ι( SK ) = SKSK = K . Aplicando ι una vez más se obtiene ι(ι(ι(ιι))) = ι K = KSK = S .

El término más simple posible que forma una base es X = λ f . f (λ xyz . x z ( y z )) (λ xyz . x ), que satisface XX = K , y X (XX) = S .

Definición formal

Los términos y derivaciones de este sistema también pueden definirse de manera más formal:

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

S , K e I son términos.
Si τ ₁ y τ ₂ son términos, entonces ( τ ₁τ ₂ ) es un término.
Nada es un término si no lo exigen las dos primeras reglas.

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

Si Δ es una derivación que termina en una expresión de la forma α ( I β) ι , entonces Δ seguido del término αβι es una derivación.
Si Δ es una derivación que termina en una expresión de la forma α (( K β) γ ) ι , entonces Δ seguido del término αβι es una derivación.
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 sea una derivación válida desde el principio, se puede extender utilizando estas reglas. Todas las derivaciones de longitud 1 son derivaciones válidas.

Conversión de términos lambda a combinadores SKI

Una expresión en el cálculo lambda se puede convertir en una expresión del cálculo de combinadores SKI de acuerdo con las siguientes reglas:

λ x . x = I
λ x . c = K c (siempre que c no dependa de x )
λ x . c x = c (siempre que c no dependa de x )
λ x . y z = S (λ x . y )(λ x . z )

expresiones de SKI

Autoaplicación y recursión

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

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

Esto también se conoce como combinador U , U x = xx . Una propiedad interesante del mismo es que su autoaplicación es irreducible:

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

O bien, utilizando la ecuación U x = xx como su definición directamente, obtenemos inmediatamente U U = U U .

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

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

o puede verse como la definición directa de otro combinador, H xy = x ( yy ).

Esta función se puede utilizar para lograr la recursión . Si β es la función que aplica α a la autoaplicación de otra cosa,

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

entonces la autoaplicación de este β es el punto fijo de ese α :

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

\ldots

O, directamente nuevamente de la definición derivada, H α ( H α ) = α ( H α ( H α )).

Si α expresa un "paso computacional" calculado por αρν para algún ρ y ν , lo que supone que ρν′ expresa "el resto del cálculo" (para algún ν′ que α "calculará" a partir de ν ), entonces su punto fijo ββ expresa todo el cálculo recursivo, puesto que usar la misma función ββ para la llamada al "resto del cálculo" (con ββν = α ( ββ ) ν ) es la definición misma de recursión: ρν′ = ββν′ = α(ββ)ν′ = ... . El término α tendrá que emplear algún tipo de condicional para detenerse en algún "caso base" y no hacer la llamada recursiva entonces, para evitar la divergencia.

Esto se puede formalizar, con

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

como

Y α = SII β = SII ( H α ) = S ( K ( SII )) H α = S ( K ( SII ))( S ( S ( KS ) K )( K ( SII ))) α

lo que nos da una posible codificación del combinador Y. Una variación más corta reemplaza sus dos subtérminos principales con solo SSI , ya que H α( H α) = SHH α = SSIH α.

Esto se vuelve mucho más corto con el uso adicional de los combinadores B, C, W , como el equivalente

Y α = S ( KU )( SB ( KU ))α = U ( B α U ) = BU ( CBU )α = SSI ( CBU )α

Y con una sintaxis pseudo- Haskell se convierte en la excepcionalmente corta Y = U . (. U ).

Siguiendo este enfoque, son posibles otras definiciones de combinadores de punto fijo. Por lo tanto,

Esta Y , por Haskell Curry :

H gx = g ( xx ) ; Y g = H g ( H g ) ; Y = S(KU)(SB(KU)) = SS(S(S(KS)K))(K(SII))

La Θ de Turing :

H hg = g ( hhg ) ; Θ g = HH g ; Θ = U(B(SI)U) = SII(S(K(SI))(SII))

Y′ (con codificación SK por John Tromp ^{[ 3 ]} ):

H gh = g ( hgh ) ; Y′ g = H g H ; Y′ = WC(SB(C(WC))) = SSK(S(K(SS(S(SSK))))K)

Θ ₄ por R. Statman: ^{[ 4 ]}

H gyz = g ( yyz ) ; Θ ₄ g = H g ( H g )( H g ) ; Θ ₄ = B(WW)(BW(BBB))

o en general,

H algo = g ( halgo ) ; Y _{_H} g = H _____ H __ g

(donde cualquier cosa vale en lugar de "_") o cualquier otra definición de combinador H intermedio, con su correspondiente definición Y _{_H} para ponerlo en marcha correctamente. En particular, una construcción, debida a Jan Klop, ^{[ 5 ]} es

L abcdefghijklmnopqstuvwxyzr = r ( thisisafixedpointcombinator ) ; Y _{_K} = LLLLLLLLLLLLLLLLLLLLLLLLLL

En un lenguaje de programación estricto, el combinador Y se expandirá hasta el desbordamiento de la pila , o nunca se detendrá en caso de optimización de llamadas de cola . ^{[ 6 ]} El combinador Z funcionará en lenguajes estrictos (también llamados lenguajes ansiosos), donde el orden de evaluación aplicativa está en efecto.

Su diferencia con el combinador Y es que está utilizando $Qx=B(Ux)I=S(K(Ux))I=S(BS(BKU))(KI)x$ como el $\eta$ -forma expandida del plano de Y $Ux$ Mientras que Y = BU ( CBU ), tenemos Z = BU ( CBQ ) = S ( KU )( SB ( KQ )):

{\begin{aligned}\\Z&=\lambda f.(\lambda x.f(\lambda v.xxv))(\lambda x.f(\lambda v.xxv))\\&=\lambda f.U(\lambda x.f(\lambda v.Uxv))\\&=S(\lambda f.U)(\lambda f.\lambda x.f(\lambda v.Uxv))\\&=S(KU)(\lambda f.S(\lambda x.f)(\lambda x.\lambda v.Uxv))\\&=S(KU)(\lambda f.S(Kf)(\lambda x.\lambda v.Uxv))\\&=S(KU)(S(\lambda f.S(Kf))(\lambda f.\lambda x.\lambda v.Uxv))\\&=S(KU)(S(S(\lambda f.S)(\lambda f.Kf))(K(\lambda x.\lambda v.Uxv)))\\&=S(KU)(S(S(KS)K)(K(\lambda x.\lambda v.Uxv)))\\&=S(KU)(S(S(KS)K)(K(\lambda x.S({\color {Red}\lambda v.Ux})(\lambda v.v))))\\&=S(KU)(S(S(KS)K)(K(\lambda x.S(K(Ux))I)))\\&=S(KU)(S(S(KS)K)(K(S(\lambda x.S(K(Ux)))(\lambda x.I))))\\&=S(KU)(S(S(KS)K)(K(S(\lambda x.S(K(Ux)))(KI))))\\&=S(KU)(S(S(KS)K)(K(S(S(\lambda x.S)(\lambda x.K(Ux)))(KI))))\\&=S(KU)(S(S(KS)K)(K(S(S(KS)(S(\lambda x.K)(\lambda x.Ux)))(KI))))\\&=S(KU)(S(S(KS)K)(K(S(S(KS)(S(KK)U))(KI))))\\\end{aligned}}

La expresión de inversión

S ( K ( SI )) K invierte los dos términos que le siguen:

S ( K ( SI )) K αβ →

K ( SI )α( K α)β →

SI ( K α)β →

Yo β( K αβ) →

Yo βα →

βα

Es, por lo tanto, equivalente a CI . Y en general, S ( K ( S f )) K es equivalente a C f , para cualquier f .

lógica booleana

El cálculo combinatorio SKI también puede implementar lógica booleana en forma de una estructura if-then-else . Una estructura if-then-else consta de una expresión booleana que es verdadera ( V ) o falsa ( F ) y dos argumentos, de tal manera que:

T xy = x

y

F xy = y

La clave está en definir las dos expresiones booleanas. La primera funciona igual que uno de nuestros combinadores básicos:

T = K

K xy = x

La segunda también es bastante sencilla:

F = SK

SK xy = K y ( xy ) = y

Una vez definidos los conceptos de verdadero y falso, toda la lógica booleana puede implementarse en términos de booleanos que actúan como estructuras if-then-else .

La negación booleana (que devuelve el opuesto de un valor booleano dado) funciona igual que la estructura if-then-else , con F y T como segundo y tercer valor:

NO b = b FT = S ( SI ( KF ))( KT ) b

Si esto se coloca en una estructura if-then-else , tiene el resultado esperado:

NO ( T ) = ( T ) FT = F

NO ( F ) = ( F ) FT = T

La operación OR booleana (que devuelve T si cualquiera de sus dos argumentos booleanos es T ) funciona igual que una estructura if-then-else con T como segundo valor:

O ab = a T b = SI ( KT ) ab

Si esto se coloca en una estructura if-then-else , tiene el resultado esperado:

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

O ( V )( F ) = ( V ) V ( F ) = V

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

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

La operación AND booleana (que devuelve T si ambos valores de sus argumentos booleanos son T ) funciona igual que una estructura if-then-else con F como tercer valor:

Y ab = ab F = S a ( KF ) b = SS ( K ( KF )) ab

Si esto se coloca en una estructura if-then-else , tiene el resultado esperado:

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

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

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

Y ( F )( F ) = ( F )( F ) F = F

Esto demuestra que el sistema SKI puede expresar plenamente la lógica booleana.

El cálculo SKI es completo , por lo que cualquier otro combinador lógico también puede expresarse en él, como por ejemplo:

XOR ab = O ( Y a ( NO b )) ( Y ( NO a ) b )

de modo que

XOR abxy = ( a ( b FT ) F ) T (( a FT ) b F ) xy = a ( byx )( bxy )

así como

NO bxy = b FT xy = b ( F xy )( T xy ) = byx

O bien abxy = a T bxy = a ( T xy )( bxy ) = ax(bxy)

Y abxy = ab F xy = a ( bxy )( F xy ) = a(bxy)y

Conexión con la lógica intuicionista

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

AK : A \to (B \to A)

,

AS : (A \to (B \to C)) \to ((A \to B) \to (A \to C))

.

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

MP

: de

A

y

A \to 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:

el fragmento implicacional de la lógica clásica requeriría el análogo combinatorio de la ley del tercero excluido , es decir , la ley de Peirce ;
La lógica clásica completa requeriría el análogo combinatorio del axiomaproposicional $F \to A.$

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

Ejemplos de reducción

Por lo general, existen varias formas de realizar una reducción. Si el término tiene una forma normal, es único, por lo que se llegará al mismo resultado en tal caso, independientemente del orden de las operaciones .

${\mathsf {SKI(KIS)}}$ ${\mathsf {SKI(KIS)}}$
- ${\mathsf {SKI(KIS)}}\Rightarrow {\mathsf {K(KIS)(I(KIS))}}\Rightarrow {\mathsf {KI(I(KIS))}}\Rightarrow {\mathsf {I}}$
- ${\mathsf {SKI(KIS)}}\Rightarrow {\mathsf {K(KIS)(I(KIS))}}\Rightarrow {\mathsf {KIS}}\Rightarrow {\mathsf {I}}$
- ${\mathsf {SKI(KIS)}}\Rightarrow {\mathsf {SKII}}\Rightarrow {\mathsf {KI(II)}}\Rightarrow {\mathsf {I}}$
${\mathsf {KS(I(SKSI))}}$ ${\mathsf {KS(I(SKSI))}}$
- ${\mathsf {KS(I(SKSI))}}\Rightarrow {\mathsf {KS(I(KI(SI)))}}\Rightarrow {\mathsf {KS(I(I))}}\Rightarrow {\mathsf {KS(II)}}\Rightarrow {\mathsf {KSI}}\Rightarrow {\mathsf {S}}$
- ${\mathsf {KS(I(SKSI))}}\Rightarrow {\mathsf {S}}$
${\mathsf {SKIK}}$ ${\mathsf {SKIK}}$
- ${\mathsf {SKIK}}\Rightarrow {\mathsf {KK(IK)}}\Rightarrow {\mathsf {KKK}}\Rightarrow {\mathsf {K}}$
- ${\mathsf {SKIK}}\Rightarrow {\mathsf {KK(IK)}}\Rightarrow {\mathsf {K}}$

Véase también

Lógica combinatoria
Sistema B, C, K, W
Combinador de punto fijo
Cálculo lambda
Programación funcional
Lenguaje de programación Unlambda
Los lenguajes de programación Iota y Jot , diseñados para ser incluso más sencillos que SKI.
Para imitar a un ruiseñor

Referencias

^ Schönfinkel, M. (1924). "Über die Bausteine der mathematischen Logik". Annalen Matemáticas . 92 ( 3– 4): 305– 316. doi : 10.1007/BF01448013 . S2CID 118507515 . Traducido por Stefan Bauer-Mengelberg como van Heijenoort, Jean , ed. (2002) [1967]. «Sobre los bloques de construcción de la lógica matemática» . A Source Book in Mathematical Logic 1879–1931 . Harvard University Press. pp. 355–366 . ISBN 9780674324497.
↑ Curry, Haskell Brooks (1930). "Grundlagen der Kombinatorischen Logik" [ Fundamentos de la lógica combinatoria ] . American Journal of Mathematics (en alemán). 52 (3). Johns Hopkins University Press: 509– 536. doi : 10.2307/2370619 . JSTOR 2370619 .
↑ https://tromp.github.io/
↑ Larry Wos, William McCune (septiembre de 1988). "Búsqueda de combinadores de punto fijo mediante la demostración automatizada de teoremas: un informe preliminar" (PDF) . Laboratorio Nacional Argonne . Consultado el 12 de diciembre de 2024 .pág. 9
↑ "Una construcción debida a Klop 2007" https://ncatlab.org/nlab/show/fixed-point+combinator
↑ Bene, Adam (17 de agosto de 2017). "Combinadores de punto fijo en JavaScript" . Bene Studio . Medium . Consultado el 2 de agosto de 2020 .

Smullyan, Raymond (1985). Para imitar a un ruiseñor . Knopf. ISBN 0-394-53491-3.Una introducción amena a la lógica combinatoria, presentada como una serie de acertijos recreativos que utilizan metáforas de la observación de aves.
— (1994). «Cap. 17–20». Diagonalización y autorreferencia . Oxford University Press. ISBN 9780198534501OCLC 473553893 Son una introducción más formal a la lógica combinatoria, con especial énfasis en los resultados de punto fijo.

Enlaces externos

O'Donnell, Mike " El cálculo combinatorio SKI como sistema universal. "
Keenan, David C. (2001) " Para diseccionar un sinsonte. "
Rathman, Chris, " Aves Combinadoras " .
" "Combinadores de arrastrar y soltar (Applet de Java). "
En las páginas 25 a 28, el libro "A Calculus of Mobile Processes, Part I (PostScript)" (de Milner, Parrow y Walker) muestra un esquema para la reducción de grafos combinatorios para el cálculo SKI.
El lenguaje de programación Nock puede considerarse un lenguaje ensamblador basado en el cálculo de combinadores SK, del mismo modo que el lenguaje ensamblador tradicional se basa en las máquinas de Turing. La instrucción 2 de Nock (el "operador Nock") es el combinador S y la instrucción 1 es el combinador K. Las demás instrucciones primitivas de Nock (instrucciones 0, 3, 4, 5 y la pseudoinstrucción "implicit cons") no son necesarias para la computación universal, pero facilitan la programación al proporcionar herramientas para trabajar con estructuras de datos de árboles binarios 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.

[1] Schönfinkel, M. (1924). "Über die Bausteine der mathematischen Logik". Annalen Matemáticas . 92 ( 3– 4): 305– 316. doi : 10.1007/BF01448013 . S2CID 118507515 . Traducido por Stefan Bauer-Mengelberg como van Heijenoort, Jean , ed. (2002) [1967]. «Sobre los bloques de construcción de la lógica matemática» . A Source Book in Mathematical Logic 1879–1931 . Harvard University Press. pp. 355–366 . ISBN 9780674324497.

[2] Curry, Haskell Brooks (1930). "Grundlagen der Kombinatorischen Logik" [ Fundamentos de la lógica combinatoria ] . American Journal of Mathematics (en alemán). 52 (3). Johns Hopkins University Press: 509– 536. doi : 10.2307/2370619 . JSTOR 2370619 .

[3] ttps://tromp.github.io/

[4] Larry Wos, William McCune (septiembre de 1988). "Búsqueda de combinadores de punto fijo mediante la demostración automatizada de teoremas: un informe preliminar" (PDF) . Laboratorio Nacional Argonne . Consultado el 12 de diciembre de 2024 .pág. 9

[5] "Una construcción debida a Klop 2007" https://ncatlab.org/nlab/show/fixed-point+combinator

[6] Bene, Adam (17 de agosto de 2017). "Combinadores de punto fijo en JavaScript" . Bene Studio . Medium . Consultado el 2 de agosto de 2020 .

[

[

[ 3 ]

[ 4 ]

[ 5 ]

[ 6 ]