f# - ¿Cómo defino y-combinator sin "let rec"?

Question

En casi todos los ejemplos, un combinador y 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 el combinador y usando let rec ...

Quiero definir este combinador sin usar recursión, 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 averiguar 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 escribo el combinador y en F # sin usar let rec ... ?

Answer 1

Como señala el compilador, no hay ningún tipo que pueda asignarse a x por lo que la expresión (xx) está bien escrita (esto no es estrictamente cierto; puede escribir explícitamente x como obj->_ - vea mi último párrafo ). Puede solucionar este problema declarando un tipo recursivo para que funcione una expresión muy similar:

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

Ahora el 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 usando este combinador causará un desbordamiento de pila. En su lugar, debe usar la versión de orden aplicativo del combinador Y ( /f.(/xf(/y.(xx)y))(/xf(/y.(xx)y)) ):

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

Otra opción sería usar la pereza explícita para definir el combinador Y de orden normal:

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 (usando la propiedad Value ):

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

Sin embargo, tiene la ventaja de que puede definir valores recursivos no funcionales, como podría hacerlo en un lenguaje perezoso:

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

Como alternativa final, puede tratar de aproximar mejor el cálculo lambda no tipificado mediante el uso del boxeo y la reducción de emisiones. Esto le daría (nuevamente usando la versión de orden aplicativo del combinador en Y):

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

Esto tiene la desventaja obvia de que causará boxeo y desempaquetado innecesarios, pero al menos esto es totalmente interno a la implementación y nunca llevará a fallas en el tiempo de ejecución.

Answer 2

El caso y las declaraciones en los derivados de LD son lo que lo hace Turing Complete, creo que están basadas en el Sistema F y no simplemente escritas, pero el punto es el mismo.

El sistema F no puede encontrar un tipo para el combinador de puntos fijos, si pudiera, no estaba muy normalizado.

Lo que significa normalizar fuertemente es que cualquier expresión tiene exactamente una forma normal, donde una forma normal es una expresión que no puede reducirse más, esto difiere de la sin tipo, donde cada expresión tiene al máximo una forma normal, tampoco puede tener una forma normal en todos.

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

Otro famoso teorema, el problema de la detención, implica que los idiomas que se normalizan fuertemente no están completos de Turing, dice que es imposible decidir (a diferencia de la prueba) de un lenguaje completo de qué subconjunto de sus programas se detendrá en qué entrada. Si un idioma se normaliza 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 de ML extienden el Sistema-F con mayúsculas y dejan que (rec) supere esto. Por lo tanto, las funciones pueden referirse a sí mismas en sus definiciones nuevamente, lo que hace que, en efecto, ya no sean cálculos lambda, ya no es posible confiar solo en funciones anónimas para todas las funciones computables. De este modo, pueden volver a entrar en bucles infinitos y recuperar su completa integridad.

Answer 3

Respuesta corta: No puedes.

Respuesta larga: el cálculo lambda simplemente tipificado está fuertemente normalizado. Esto significa que no es el equivalente de Turing. La razón de esto básicamente se reduce al hecho de que un combinador de Y debe ser primitivo o definido recursivamente (como lo ha encontrado). Simplemente no puede expresarse en el Sistema F (o cálculos de tipo más simple). No hay forma de evitar esto (ha sido probado, después de todo). Sin embargo, el combinador de Y que puede implementar funciona exactamente de la manera que desee.

Te sugiero que pruebes el esquema si quieres un verdadero combinador Y de estilo de la Iglesia. Use la versión aplicativa dada anteriormente, ya que otras versiones no funcionarán, a menos que agregue explícitamente la pereza, o use un intérprete de esquema perezoso. (Técnicamente, el esquema no está completamente desvinculado, pero se escribe dinámicamente, lo cual es lo suficientemente bueno para esto).

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

Después de pensar un poco más, estoy bastante seguro de que agregar un combinador de Y primitivo que se comporta exactamente de la manera que letrec define hace al Sistema F Turing completo. Todo lo que necesita hacer para simular una máquina de Turing es implementar la cinta como un entero (interpretado en binario) y un cambio (para posicionar la cabeza).

Answer 4

Yo diría que es imposible, y preguntando por qué, me gustaría hacer una mano e invocar el hecho de que simplemente teclear lambda calculus tiene la propiedad de normalización . En resumen, todos los términos del cálculo lambda simplemente escrito terminan (por lo tanto, Y no puede definirse en el cálculo lambda simplemente escrito).

El sistema de tipos de F # no es exactamente el sistema de tipos del simple cálculo lambda, pero está lo suficientemente cerca. F # sin let rec acerque mucho al cálculo lambda, simplemente escrito - y, para reiterar, en ese lenguaje no puede definir un término que no termine, y que excluya la definición de Y también.

En otras palabras, en F #, "dejar que rec" debe ser un lenguaje primitivo como mínimo porque, incluso si pudiera definirlo a partir de otros primitivos, no podría escribir esta definición. Tenerlo como primitivo le permite, entre otras cosas, darle un tipo especial a ese primitivo.

EDIT: kvb muestra en su respuesta que las definiciones de tipo (una de las características ausentes del cálculo lambda simplemente escrito pero que está presente en F # sin dejar de grabar) permiten obtener algún tipo de recursión. Muy inteligente.