Combinador de punto fijo

En el cálculo lambda clásico sin tipos , cada función tiene un punto fijo. Una implementación particular de${\displaystyle \mathrm {fix} }$es el combinador paradójico Y de Haskell Curry , dado por ^{[ 2 ] : 131 [ nota 1 ] [ nota 2 ]}

${\displaystyle \mathrm {Y} =\lambda f.\ (\lambda xf\ (x\ x))\ (\lambda xf\ (x\ x))}$

(Aquí se utilizan las notaciones y convenciones estándar del cálculo lambda: Y es una función que toma un argumento f y devuelve la expresión completa que sigue al primer período; la expresión${\displaystyle \lambda xf\ (x\ x)}$denota una función que toma un argumento x , considerado como una función, y devuelve la expresión${\displaystyle f\ (x\ x)}$, dónde${\displaystyle (x\ x)}$denota x aplicada a sí misma. La yuxtaposición de expresiones denota la aplicación de una función , es asociativa por la izquierda y tiene mayor precedencia que el punto.

El siguiente cálculo verifica que${\displaystyle \mathrm {Y} g}$es de hecho un punto fijo de la función${\displaystyle g}$:

El término lambda${\displaystyle g\ (\mathrm {Y} \ g)}$En general, puede que no se reduzca β al término${\displaystyle \mathrm {Y} \g}$Sin embargo, ambos términos se reducen β al mismo término, como se muestra.

A continuación se presenta un ejemplo de implementación de Y en el lenguaje R :

Y <- \ ( f ) { g <- \ ( x ) f ( x ( x )) g ( g ) }

Esto se puede utilizar para implementar el factorial de la siguiente manera:

hecho <- \ ( f ) \ ( n ) si ( n == 0 ) 1 sino n * f ( n - 1 ) Y ( hecho )( 5 ) # produce 5! = 120

La letra Y solo es necesaria cuando no se especifican los nombres de las funciones. Sustituyendo todas las definiciones en una sola línea, de modo que no se requieran los nombres de las funciones, se obtiene:

( \ ( f ) ( \ ( x ) f ( x ( x )))( \ ( x ) f ( x ( x )))) ( \ ( f ) \ ( n ) si ( n == 0 ) 1 si no n * f ( n - 1 )) ( 5 )

Esto funciona porque R utiliza evaluación perezosa .

Los lenguajes que utilizan evaluación estricta , como Python , C++ y otros lenguajes de programación estrictos , a menudo pueden expresar Y; sin embargo, cualquier implementación es inútil en la práctica ya que entra en un bucle indefinidamente hasta que termina por un desbordamiento de pila .

Muchas funciones no tienen puntos fijos, por ejemplo${\displaystyle f:\mathbb {N} \to \mathbb {N} }$con${\displaystyle f(n)=n+1}$Mediante la codificación de Church , los números naturales pueden representarse en el cálculo lambda, y esta función f puede definirse en dicho cálculo. Sin embargo, su dominio ahora contendrá todas las expresiones lambda, no solo las que representan números naturales. El combinador Y, aplicado a f , dará como resultado un punto fijo para f , pero este punto fijo no representará un número natural . Si se intenta calcular Y f en un lenguaje de programación real, se producirá un bucle infinito.

El combinador de punto fijo puede definirse en matemáticas y luego implementarse en otros lenguajes. Las matemáticas generales definen una función en función de sus propiedades extensionales . ^{[ 3 ]} Es decir, dos funciones son iguales si realizan la misma función. El cálculo lambda y los lenguajes de programación consideran la identidad de una función como una propiedad intensional . La identidad de una función se basa en su implementación.

Una función (o término) del cálculo lambda es una implementación de una función matemática. En el cálculo lambda existen varios combinadores (implementaciones) que satisfacen la definición matemática de un combinador de punto fijo.

La lógica combinatoria es una teoría de funciones de orden superior . Un combinador es una expresión lambda cerrada , lo que significa que no tiene variables libres . Los combinadores se pueden combinar para dirigir valores a sus posiciones correctas en la expresión sin necesidad de nombrarlos como variables.

La función factorial proporciona un buen ejemplo de cómo se puede utilizar un combinador de punto fijo para definir funciones recursivas. La definición recursiva estándar de la función factorial en matemáticas se puede escribir como

${\displaystyle \operatorname {fact} \ n={\begin{cases}1&{\text{si}}~n=0\\n\times \operatorname {fact} (n-1)&{\text{en otro caso.}}\end{cases}}}$

donde n es un entero no negativo .

Esto plantea un problema, sin embargo, ya que${\displaystyle \operatorname {fact} }$dentro de la definición de${\displaystyle \operatorname {fact} }$No puede significar la inclusión de la definición en su totalidad dentro de sí misma. En cambio, y como suele pasar casi desapercibido, se trata de la referencia a la definición por su nombre . Esto presupone la existencia de un registro global de nombres, el llamado «entorno». Y el cálculo lambda carece por completo de esto.

Sin embargo, en el cálculo lambda existen referencias a nombres: nombres locales, nombres de parámetros de una función dada. Y por lo tanto, lo anterior se puede reescribir como

${\displaystyle {\begin{aligned}&\operatorname {fact} (n)=\operatorname {f} (\operatorname {f} ,n)\\&\quad {\text{donde}}\\&\quad \operatorname {f} (s,n)={\begin{cases}1&{\text{si}}~n=0\\n\times s(s,n-1)&{\text{en otro caso}}\end{cases}}\end{aligned}}}$

Separar una copia independiente de${\displaystyle \operatorname {f} }$y al pasarlo como argumento a sí mismo, lo pone a su disposición para ser llamado, según sea necesario, dentro de sí mismo. En tal llamada, debe pasarse nuevamente como argumento para que esté disponible para la siguiente invocación, y así sucesivamente, a medida que avanza la cadena de invocaciones. La definición de${\displaystyle \operatorname {f} }$es recursivo abierto y llamando${\displaystyle \operatorname {f} }$Consistiendo en sí mismo como argumento en la parte superior, se cierra el círculo.

Implementar esto en el cálculo lambda ahora es trivial y conduce directamente a la definición del combinador Y, una instancia de un combinador de punto fijo, tal que${\displaystyle \operatorname {fix} f=f\,(\operatorname {fix} f)}$. O directamente, defina una función F de dos argumentos f y n :

${\displaystyle F\ f\ n=(\operatorname {IsZero} \ n)\ 1\ (\operatorname {multiply} \ n\ (f\ (\operatorname {pred} \ n)))}$

(Aquí${\displaystyle (\operatorname {IsZero} \ n)}$es una función que toma dos argumentos y devuelve su primer argumento si n = 0, y su segundo argumento en caso contrario;${\displaystyle \operatorname {pred} \ n}$se evalúa a n –1.)

Ahora define${\displaystyle \operatorname {fact} ={\textsf {fix}}\ F=F\ ({\textsf {fix}}\ F)}$. Entonces${\displaystyle \operatorname {fact} }$es un punto fijo de F , que da

${\displaystyle {\begin{aligned}\operatorname {fact} n&=F\ \operatorname {fact} \ n\\&=(\operatorname {IsZero} \ n)\ 1\ (\operatorname {multiply} \ n\ (\operatorname {fact} \ (\operatorname {pred} \ n)))\ \end{aligned}}}$

como se desee.

En el cálculo lambda sin tipos, los combinadores de punto fijo no son especialmente raros. De hecho, hay infinitos. ^{[ 5 ]} En 2005, Mayer Goldberg demostró que el conjunto de combinadores de punto fijo del cálculo lambda sin tipos es recursivamente enumerable . ^{[ 6 ]}

El combinador Y se puede expresar en el cálculo SKI como

${\displaystyle {\mathsf {Y=S(K(SII))(S(S(KS)K)(K(SII)))=SS(S(S(KS)K))(K(SII))}}}$

Los combinadores adicionales ( sistema B, C, K, W ) permiten codificaciones mucho más cortas. Con${\displaystyle {\mathsf {U=SII}}}$el combinador de autoaplicación, ya que${\displaystyle {\mathsf {S}}({\mathsf {K}}x)yz=x(yz)={\mathsf {B}}xyz}$y${\displaystyle {\mathsf {S}}x({\mathsf {K}}y)z=xzy={\mathsf {C}}xyz}$, lo anterior se convierte en

${\displaystyle {\mathsf {Y=S(KU)(SB(KU))=BU(CBU)}}\ \ \$ ;\ \ {\mathsf {Y=SSI(BWB)}}}

El combinador de punto fijo más corto en el cálculo SK que utiliza solo combinadores S y K, hallado por John Tromp , es

${\displaystyle {\mathsf {Y'=SSK(S(K(SS(S(SSK))))K)=WC(SB(C(WC)))}}}$

aunque tenga en cuenta que no está en forma normal, que es más larga. Este combinador corresponde a la expresión lambda.

${\displaystyle {\mathsf {Y}}'=(\lambda xy.xyx)(\lambda yx.y(xyx))}$

El siguiente combinador de punto fijo es más simple que el combinador Y, y se reduce mediante β al combinador Y; a veces se le cita como el propio combinador Y:

${\displaystyle {\mathsf {X}}=\lambda f.(\lambda x.xx)(\lambda xf(xx))\ \ \$ ;\ \ {\mathsf {Xf=U(BfU)}}}

Otro combinador de punto fijo común es el combinador de punto fijo de Turing (llamado así por su descubridor, Alan Turing ): ^{[ 7 ] [ 2 ] : 132}

${\displaystyle \Theta =(\lambda xy.y(xxy))\ (\lambda xy.y(xxy))={\mathsf {SII(S(K(SI))(SII))=U(B(SI)U)}}}$

Su ventaja sobre${\displaystyle {\mathsf {Y}}}$es que${\displaystyle \Theta \ f}$beta-reduce a${\displaystyle f\ (\Theta f)}$, ^{[ nota 3 ]} mientras que${\displaystyle {\mathsf {Y}}\ f}$y${\displaystyle f\ ({\mathsf {Y}}f)}$solo beta-reducción a un término común.

${\displaystyle \Theta }$También tiene una forma sencilla de llamada por valor :

${\displaystyle \Theta _{v}=(\lambda xy.y(\lambda z.xxyz))\ (\lambda xy.y(\lambda z.xxyz))}$

El análogo de la recursión mutua es un combinador de punto fijo polivariádico , ^{[ 8 ] [ 9 ] [ 10 ]} que puede denotarse como Y*.

En un lenguaje de programación estricto, el combinador Y se expandirá hasta desbordamiento de pila , o nunca se detendrá en caso de optimización de llamada de cola . ^{[ 11 ]} El combinador Z funcionará en lenguajes estrictos (también llamados lenguajes ansiosos, donde se aplica el orden de evaluación aplicativo). El combinador Z tiene el siguiente argumento definido explícitamente, lo que impide la expansión de${\displaystyle Zg}$en el lado derecho de la definición: ^{[ 12 ]}

${\displaystyle Zgv=g(Zg)v\ .}$

y en el cálculo lambda es una expansión eta del combinador Y:

${\displaystyle Z=\lambda f.(\lambda x.f(\lambda v.xxv))\ (\lambda x.f(\lambda v.xxv))\ .}$

Si F es un combinador de punto fijo en el cálculo lambda sin tipos, entonces se cumple que:

${\displaystyle {\mathsf {F}}=\lambda x.Fx=\lambda x.x(Fx)=\lambda x.x(x(Fx))=\cdots }$

Términos que tienen el mismo árbol de Böhm que un combinador de punto fijo, es decir, tienen la misma extensión infinita.${\displaystyle \lambda x.x(x(x\cdots ))}$Se denominan combinadores de punto fijo no estándar . Cualquier combinador de punto fijo es también uno no estándar, pero no todos los combinadores de punto fijo no estándar son combinadores de punto fijo, ya que algunos no satisfacen la ecuación de punto fijo que define a los "estándar". Estos combinadores se denominan combinadores de punto fijo estrictamente no estándar ; un ejemplo es el siguiente combinador:

${\displaystyle {\mathsf {N=BU(B(BU)B)}}}$

dónde

${\displaystyle {\mathsf {B}}=\lambda xyz.x(yz)}$

${\displaystyle {\mathsf {U}}=\lambda x.xx\ }$

desde

${\displaystyle {\mathsf {N}}=\lambda x.Nx=\lambda x.x(N_{2}x)=\lambda x.x(x(x(N_{3}x)))=\lambda x.x(x(x(x(x(x(N_{4}x))))))=\cdots }$

dónde${\displaystyle {\mathsf {N}}_{i}}$son modificaciones de${\displaystyle {\mathsf {N}}}$creados sobre la marcha que añaden${\displaystyle i}$casos de${\displaystyle x}$inmediatamente en la cadena mientras se reemplaza con${\displaystyle {\mathsf {N}}_{i+1}}$.

El conjunto de combinadores de punto fijo no estándar no es recursivamente enumerable . ^{[ 6 ]}

En un lenguaje que admite evaluación perezosa , como Haskell , es posible definir un combinador de punto fijo utilizando la ecuación definitoria del combinador de punto fijo que convencionalmente se denomina fix. Dado que Haskell tiene tipos de datos perezosos , este combinador también se puede usar para definir puntos fijos de constructores de datos (y no solo para implementar funciones recursivas). La definición se da aquí, seguida de algunos ejemplos de uso. En Hackage, el ejemplo original es: ^{[ 13 ]}

fix , fix' :: ( a -> a ) -> a fix f = let x = f x in x -- Lambda eliminada. Compartición. -- Definición original en Data.Function. -- alternativa: fix' f = f ( fix' f ) -- Lambda levantada. No compartición.corregir ( \ x -> 9 ) -- esto se evalúa como 9fix ( \ x -> 3 : x ) -- se evalúa a la lista infinita perezosa [3,3,3,...]hecho = fijo fac -- se evalúa a la función factorial donde fac f 0 = 1 fac f x = x * f ( x - 1 )Dato 5 : se evalúa a 120.

En un lenguaje funcional estricto, como se ilustra a continuación con OCaml , el argumento de f se expande de antemano, lo que produce una secuencia de llamadas infinita,

${\displaystyle f\ (f...(f\ ({\mathsf {fix}}\ f))...)\ x}$.

Esto puede resolverse definiendo la corrección con un parámetro adicional.

sea ​​rec fix f x = f ( fix f ) x (* observe la x adicional; por lo tanto fix f = \x-> f (fix f) x *)let factabs fact = function (* factabs tiene un nivel adicional de abstracción lambda *) 0 -> 1 | x -> x * fact ( x - 1 )let _ = ( fix factabs ) 5 (* se evalúa a "120" *)

En un lenguaje funcional multiparadigma (uno decorado con características imperativas), como Lisp , Peter Landin sugirió el uso de una asignación de variables para crear un combinador de punto fijo, ^{[ 14 ]} como en el siguiente ejemplo usando Scheme :

( define Y! ( lambda ( f ) (( lambda ( g ) ( set! g ( f ( lambda ( x ) ( g x )))) ;; (set! g expr) asigna a g el valor de expr, g ) ;; reemplazando el valor inicial de g de #f, creando #f ))) ;; por lo tanto, el valor verdaderamente autorreferencial en g

Utilizando un cálculo lambda con axiomas para sentencias de asignación, se puede demostrar que Y!satisface la misma ley de punto fijo que el combinador Y de llamada por valor: ^{[ 15 ] [ 16 ]}

${\displaystyle (Y_{!}\ \lambda x.e)e'=(\lambda x.e)\ (Y_{!}\ \lambda x.e)e'}$

En el uso más idiomático de Scheme moderno, esto normalmente se manejaría a través de una letrecexpresión, ya que el alcance léxico se introdujo en Lisp en la década de 1970:

( define Y* ( lambda ( f ) ( letrec ;; (letrec ((g expr)) ...) define localmente g (( g ;; como expr recursivamente: g en expr se refiere a ( f ( lambda ( x ) ( g x ))))) ;; esa misma g definida, g = f (λx. gx) g ))) ;; ((Y* f) ...) = (g ...) = ((f (λx. gx)) ...)

O sin la etiqueta interna:

( define Y* ( lambda ( f ) (( lambda ( i ) ( i i )) ( lambda ( i ) ( f ( lambda x ( apply ( i i ) x )))))))

Este ejemplo es una implementación ligeramente interpretativa de un combinador de punto fijo. Se utiliza una clase para contener la fix()función, llamada FixedPointCombinator. La función que se va a corregir está contenida en una clase que hereda de fixer. La fix()función accede a la función que se va a corregir usando un concepto para llamar a apply(). En cuanto a la definición funcional estricta, fix()se le da explícitamente un parámetro adicional x, lo que significa que no se necesita evaluación perezosa.

usando std :: same_as ;plantilla < typename Ret , typename Arg , typename T > concepto FixedPointApplicable = requiere ( Arg x ) { { T :: apply ( x ) } -> same_as < Ret > ; };plantilla < typename Ret , typename Arg , FixedPointApplicable < Ret , Arg > Derived > clase FixedPointCombinator { public : static Ret fix ( Arg x ) noexcept { return Derived :: apply ( x ); } };clase Factorial : public FixedPointCombinator < long , long , Factorial > { static long apply ( long x ) noexcept { if ( x == 0 ) { return 1 ; } return x * fix ( x - 1 ); } };resultado largo = Factorial :: fijar ( 5 );

Utilizando únicamente funciones lambda, se puede crear un combinador de punto fijo como este:

auto fix = []( auto f ) { return [ f ]( auto && ... args ) -> decltype ( auto ) { return f ( f , std :: forward < decltype ( args ) > ( args )...); }; };auto factorial = fix ([]( auto self , long n ) -> long { return n == 0 ? 1 : n * self ( self , n - 1 ); });std :: println ( "5! = {}" , factorial ( 5 )); // imprime 120

Se puede mostrar otro ejemplo para demostrar el cálculo del combinador SKI (con el nombre del pájaro dado de la lógica combinatoria ) que se utiliza para construir el combinador Z para lograr un comportamiento similar a una llamada de cola a través del trampolín:

// Combinadores const K = < A , B > ( a : A ) => ( _b : B ) => a ; // Cernícalo const S = < A , B , C > ( a : ( x : C ) => ( y : B ) => A ) => ( b : ( x : C ) => B ) => ( c : C ) => a ( c )( b ( c )); // Estornino// Combinadores derivados const I = S ( K )( K ); // Identidad const B = S ( K ( S ))( K ); // Azulejo const C = S ( B ( B )( S ))( K ( K )); // Cardenal const W = C ( S )( I ); // Reinita const T = C ( I ); // Zorzal const V = B ( C )( T ); // Vireo const I1 = C ( C ( I )); // Ave Identidad una vez eliminada; igual que C(B(B)(I))(I) const C1 = B ( C ); // Cardenal una vez eliminada const R1 = C1 ( C1 ); // Petirrojo una vez eliminada const V1 = B ( R1 )( C1 ); // Vireo una vez eliminada const I2 = R1 ( V ); // Ave Identidad dos veces eliminada// Combinadores Z const Z = B ( W ( I1 ))( V1 ( B )( W ( I2 )));const Z2 = S ( K ( S ( S ( K ( S ( S ( K )( K ))( S ( K )( K ))))( S ( K ( S ( K ( S ))( K )))( S ( K ( S ( S ( K )( K ))))( K ))))( K ( S ( S ( S ( K ))))))( S ( S ( K ( S ( S ( S ( K ( S ( K ( S ))( K )))( S ))( K ( K ))))( S ( K ( S ( S ( K ( S ( K ( S ) )( K )) )( S ))( K ( K ))))( S ( K ( S ))( K ))))( K ( S ( S ( K ( S ( S ( K )( K ))( S ( K )( K ))))( S ( K ( S ( K ( S ))( K )))( S ( K ( S ( S ( K )( K ))))( K ))))( K ( S ( K ( S ( S ( K ( S ( S ( K ( S ( K ( S ) )( K )) ) ( S ))( K ( K ))))( S ( K ( S ( S (K ( S ( K ( S ))( K ) ))( S ))( K ( K ))))( S ( K ( S ( S ( K )( K ))))( K ))))))( K )))))); // Forma alternativa totalmente expandida.const Z3 = S ( S ( K ( S ( S )( K ( S ( S ( K )( K ))( S ( K )( K ))))))( K ))( S ( S ( K ( S )) ( K ))( K ( S ( S ( K ( S ))( S ( K ( S ( K ( S ( K ( S ( S ) ( K ( K ) )))( K )))( S )))( S ( S ( K )( K ))))) ) ( K ) ))( K ( K ( S ( S ( K ) ( K ))( S ( K )( K )))))))); // Otra versión más corta.const trampolín = < T > ( fn : T | (() => T )) : T => { let ctx = fn ; while ( typeof ctx === "function" ) { ctx = ( ctx as () => T )(); } return ctx ; };const countFn = ( self : ( n : number ) => any ) => ( n : number ) : any => n === 0 ? ( console . log ( n ), n ) : () => self ( n - 1 ); // Devuelve thunk "() => self(n - 1)" en su lugar.// Ejemplos trampolín ( Z ( countFn )( 10 )); trampolín ( Z2 ( countFn )( 10 )); trampolín ( Z3 ( countFn )( 10 ));

En los lenguajes de programación que admiten tipos de datos recursivos con nombre , la recursión ilimitada en${\displaystyle t:=t\to a}$, lo que crea el tipo que sería infinito${\displaystyle t}$, se rompe al nombrar el tipo${\displaystyle t}$explícitamente, como por ejemplo tipo${\displaystyle R\ a}$que se define de manera que sea isomorfo a (o simplemente sinónimo de) el tipo${\displaystyle R\ a\to a}$. De este modo${\displaystyle R\ a:=R\ a\to a}$se reconoce como un tipo recursivo. Un dato (valor) del tipo${\displaystyle R\ a}$se crea simplemente etiquetando un valor que es una función que tiene el tipo${\displaystyle R\ a\to a}$, por la etiqueta del constructor de datos para el tipo${\displaystyle R\ a}$.

Por ejemplo, en el siguiente código Haskell, sea Recese nombre de etiqueta, y por lo tanto Recy appsean los nombres de las dos direcciones del isomorfismo, con tipos: ^{[ 19 ] [ 20 ]}

Rec :: ( R a -> a ) -> R a app :: R a -> ( R a -> a )

(dónde${\displaystyle$ ::} significa "tiene tipo"). Esto nos permite escribir:

nuevo tipo R a = Rec { app :: R a -> a } -- app (Rec g) = g -- g :: R a -> a -- Rec g :: R a -- app :: R a -> (R a -> a)y :: ( a -> a ) -> a y f = ( \ x -> f ( app x x )) ( Rec ( \ x -> f ( app x x ))) -- x :: R a -- app x :: R a -> a -- app xx :: a

La definición habitual del cálculo lambda${\displaystyle \operatorname {Y} f=\operatorname {U} (\lambda x.f\ (\operatorname {U} x))}$(dónde${\displaystyle \operatorname {U} x=x\ x}$y por lo tanto el término${\displaystyle \operatorname {U} (\lambda x.f\ (\operatorname {U} x))}$testigos de la equivalencia${\displaystyle x\ x=f\ (x\ x)}$) contiene en su núcleo la autoaplicación${\displaystyle x\ x}$, que no es tipificable en los lenguajes de programación de tipado estático. Pero la expresión app x xanterior sí es tipificable. De forma equivalente, podemos redefinir el combinador de autoaplicación.${\displaystyle \operatorname {U} }$y usarlo como

U' g = g ( Rec g ) y f = U' ( \ Rec g -> f ( U' g )) -- g (Rec g) = f (g (Rec g))U'' x = app x x y f = U'' ( Rec ( \ x -> f ( U'' x ))) -- app xx = f (app xx)

O en OCaml:

tipo ' a recc = En de ( ' a recc -> ' a ) dejar fuera ( En x ) = xsea ​​y f = ( fun x a -> f ( out x x ) a ) ( In ( fun x a -> f ( out x x ) a ))

Alternativamente:

sea ​​y f = ( fun x -> f ( fun z -> out x x z )) ( In ( fun x -> f ( fun z -> out x x z )))

Algunos lenguajes permiten marcar explícitamente tipos generales como recursivos incluso sin nombrarlos. Hacer eso también permite definir el${\displaystyle \operatorname {Y} }$combinador en dichos lenguajes.