¿Cómo puedo definir y-combinator sin "let rec"?

Question

En casi todos los ejemplos, un Y-Combinator en lenguajes de tipo ML se escribe así:

let rec y f x = f (y f) x 
let factorial = y (fun f -> function 0 -> 1 | n -> n * f(n - 1)) 

Esto funciona como se esperaba, pero se siente como hacer trampa para definir la ordenada en el combinador usando let rec ....

quiero definir este combinador sin utilizar la recursividad, usando la definición estándar:

Y = λf·(λx·f (x x)) (λx·f (x x)) 

una traducción directa es la siguiente:

let y = fun f -> (fun x -> f (x x)) (fun x -> f (x x));; 

Sin embargo, F # se queja de que no puede entender los tipos:

let y = fun f -> (fun x -> f (x x)) (fun x -> f (x x));; 
    --------------------------------^ 

C:\Users\Juliet\AppData\Local\Temp\stdin(6,33): error FS0001: Type mismatch. Expecting a 
    'a  
but given a 
    'a -> 'b  
The resulting type would be infinite when unifying ''a' and ''a -> 'b' 

¿Cómo wRIT e el combinador y en F # sin usar let rec ...?

Answer 1

Como el compilador señala, no hay un tipo que se puede asignar a x modo que la expresión (x x) está bien escrito-(esto no es estrictamente cierto, se puede escribir de forma explícita como xobj->_ - ver mi último párrafo) . Puede solucionar este problema al declarar un tipo recursivo para que una expresión muy similar funcionará:

type 'a Rec = Rec of ('a Rec -> 'a) 

Ahora la Y-Combinator se puede escribir como:

let y f = 
    let f' (Rec x as rx) = f (x rx) 
    f' (Rec f') 

Desafortunadamente, encontrará que esto no es muy útil porque F # es un lenguaje estricto, por lo que cualquier función que intente definir utilizando este combinador causará un desbordamiento de la pila. En su lugar, es necesario utilizar la versión aplicativo orden de la Y-Combinator (\f.(\x.f(\y.(x x)y))(\x.f(\y.(x x)y))):

let y f = 
    let f' (Rec x as rx) = f (fun y -> x rx y) 
    f' (Rec f') 

Otra opción sería utilizar la pereza explícita para definir el orden normal de Y-Combinator:

type 'a Rec = Rec of ('a Rec -> 'a Lazy) 
let y f = 
    let f' (Rec x as rx) = lazy f (x rx) 
    (f' (Rec f')).Value 

Esto tiene la desventaja de que las definiciones de funciones recursivas ahora necesitan una fuerza explícita del valor perezoso (utilizando la propiedad Value):

let factorial = y (fun f -> function | 0 -> 1 | n -> n * (f.Value (n - 1))) 

Sin embargo, tiene la ventaja de que se pueden definir los valores recursivos no de función, como ya se podía en un lenguaje vago:

let ones = y (fun ones -> LazyList.consf 1 (fun() -> ones.Value)) 

Como última alternativa, se puede tratar de una mejor aproximación al cálculo lambda no tipificado por usando boxeo y downcasting. Esto le daría (de nuevo utilizando la versión de orden aplicativo de la Y-Combinator):

let y f = 
    let f' (x:obj -> _) = f (fun y -> x x y) 
    f' (fun x -> f' (x :?> _)) 

Esto tiene el inconveniente obvio que hará que el boxeo no sean necesarios y unboxing, pero al menos esto es totalmente interna a la aplicación y nunca conducirá al fracaso en el tiempo de ejecución.

Answer 2

Yo diría que es imposible, y le pregunté por qué, me gustaría expresar e invocar el hecho de que simplemente mecanografiado lambda tiene el normalization property. En resumen, todos los términos del cálculo lambda simplemente tipeado terminan (en consecuencia, Y no se puede definir en el cálculo lambda simplemente tipado).

El sistema de tipo F # no es exactamente el tipo de sistema de cálculo lambda simplemente tipeado, pero está lo suficientemente cerca. F # sin let rec se parece mucho al cálculo lambda simplemente tipado, y, para reiterarlo, en ese idioma no se puede definir un término que no termine, y eso excluye la definición de Y también.

En otras palabras, en F #, "let rec" debe ser, como mínimo, una primitiva del lenguaje porque incluso si pudieras definirla a partir de las otras primitivas, no podrías escribir esta definición. Tenerlo como primitivo te permite, entre otras cosas, darle un tipo especial a ese primitivo.

EDITAR: kvb muestra en su respuesta que las definiciones de tipo (una de las características ausentes del cálculo lambda simplemente tipeado pero presente en let-rec-less F #) permiten obtener algún tipo de recursión. Muy inteligente.

Answer 3

Las declaraciones de mayúsculas y minúsculas en los derivados ML son lo que hace que sea Turing Complete, creo que están basadas en el Sistema F y no simplemente mecanografiadas, pero el punto es el mismo.

El sistema F no puede encontrar un tipo para cualquier combinador de punto fijo, si pudiera, no estaba fuertemente normalizado.

medios Lo fuertemente la normalización es que cualquier expresión tiene exactamente uno forma normal, en una forma normal es una expresión que no se puede reducir más lejos, esto difiere de sin tipo en el que cada expresión tiene en el máximo una forma normal, tampoco puede tener forma normal en absoluto.

Si los cálculos lambda tipados podrían construir un operador de punto fijo de alguna manera, era muy posible que una expresión no tuviera forma normal.

otro teorema famoso, el problema de la parada, implica que las lenguas fuertemente la normalización no se Turing completo, se dice que es imposible deciden (diferente de prueba) de un lenguaje Turing completo lo subconjunto de sus programas se detiene ante lo que de entrada . Si un lenguaje se está normalizando fuertemente, es decidible si se detiene, es decir, siempre se detiene. Nuestro algoritmo para decidir esto es el programa: true;.

Para resolver esto, los derivados ML extienden el Sistema-F con mayúsculas y dejan (rec) para superar esto. De este modo, las funciones pueden volver a referirse a sí mismas en sus definiciones, haciendo que ya no tengan ningún cálculo lambda, ya no es posible confiar únicamente en funciones anónimas para todas las funciones computables. De este modo, pueden entrar de nuevo en bucles infinitos y recuperar su turing-completitud.

Answer 4

Respuesta corta: No se puede.

Respuesta larga: El cálculo lambda simplemente tipeado es fuertemente normalizador. Esto significa que no es equivalente a Turing. La razón de esto básicamente se reduce al hecho de que un combinador Y debe ser primitivo o definido recursivamente (como lo ha encontrado).Simplemente no se puede expresar en el Sistema F (o cálculos tipeados más simples). No hay forma de evitar esto (se ha demostrado, después de todo). El combinador Y que puede implementar funciona exactamente de la manera que desee, sin embargo.

Le sugiero que pruebe el esquema si quiere un verdadero combinador Y de estilo Church. Use la versión de aplicación que se proporciona arriba, ya que otras versiones no funcionarán, a menos que agregue pereza explícitamente o use un intérprete de Scheme lento. (Esquema técnicamente no es completamente sin tipo, pero ha de tipos dinámicos, que es lo suficientemente bueno para esto.)

ver esto por la prueba de la fuerte normalización: http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.127.1794

Después de pensar un poco más, estoy bastante Asegúrese de que al agregar un combinador Y primitivo que se comporta exactamente como lo hace el definido por el letrec, el Sistema F Turing se completa. Todo lo que necesita hacer para simular una máquina de Turing es implementar la cinta como un número entero (interpretado en binario) y un desplazamiento (para colocar la cabeza).