Comment définir y-combinator sans "let rec"?

Question

Dans presque tous les exemples, y combinator en ML-type de langues est écrit comme ceci:

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

Cela fonctionne comme prévu, mais il se sent comme de la tricherie, de définir le y combinator l'aide d' let rec ....

Je veux définir ce combinateur sans utiliser la récursivité, à l'aide de la définition de la norme:

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

Une traduction directe est comme suit:

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

Cependant, F# se plaint qu'il ne peut pas comprendre les types:

  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'

Comment puis-je écrire le y combinator en F# sans l'aide d' let rec ...?

Answer 1

Comme le compilateur points, il n'y a pas de type qui peut être attribué x de sorte que l'expression (x x) est bien typés (ce n'est pas strictement vrai; vous pouvez taper explicitement x comme obj->_ - voir mon dernier paragraphe). Vous pouvez contourner ce problème en déclarant récursive de type, de sorte qu'une expression très semblable:

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

Maintenant, le Y combinator peut être écrite comme:

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

Malheureusement, vous trouverez que ce n'est pas très utile car F# est un langage "strict", de sorte que toute fonction que vous essayez de définir l'utilisation de ce combinateur va provoquer un débordement de pile. Au lieu de cela, vous devez utiliser l'applicatif version du 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')

Une autre option serait d'utiliser explicitement la paresse de définir la normale afin 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

Ceci a l'inconvénient que la fonction récursive définitions maintenant besoin d'un explicite de la force de la paresse de la valeur (à l'aide de l' Value de la propriété):

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

Cependant, il a l'avantage que vous pouvez définir des non-fonction récursive des valeurs, comme vous le feriez dans un paresseux langue:

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

Comme dernière alternative, vous pouvez essayer de mieux rapprocher les non typée lambda calcul en utilisant la boxe et de passer. Ce serait vous donner (encore une fois à l'aide de l'applicatif version du Y combinator):

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

Cela a le désavantage évident qu'il entraîne boxing et unboxing, mais au moins c'est purement interne à la mise en œuvre et ne sera jamais réellement conduire à l'échec lors de l'exécution.

Answer 2

Je dirais que c'est impossible, et lui a demandé pourquoi, je voudrais handwave et invoquer le fait que le lambda calcul simplement typé a la normalisation de la propriété. En bref, tous les termes du lambda calcul simplement typé fin (donc Y ne peut pas être défini dans le lambda calcul simplement typé).

F#'s type de système n'est pas exactement le type de système de lambda calcul simplement typé, mais il est assez proche. F# sans let rec vient vraiment à proximité du lambda calcul simplement typé -- et, pour rappel, dans cette langue, vous ne pouvez pas définir un terme qui n'a pas de fin, et qui exclut de la définition de Y trop.

En d'autres termes, en F#, "let rec" doit être une langue primitive, à tout le moins, parce que même si vous étiez capable de le définir à partir de l'autre primitives, vous ne seriez pas en mesure de le type de cette définition. Ayant comme primitive permet, entre autres choses, de donner un type spécial de cette primitive.

EDIT: kvb indique dans sa réponse que les définitions de type (l'une des caractéristiques qui sont absentes de la tout simplement tapé lambda-calcul mais laissez-rec-moins F#) permettent d'obtenir une sorte de récursivité. Très intelligent.

Answer 3

Cas et laisser états ML dérivés sont ce qu'il fait de Turing Complet, je crois qu'elles sont fondées sur le Système F et pas simplement typé, mais le point est le même.

Le système F ne peut pas trouver un type pour les tout point fixe combinator, si elle le pouvait, elle n'était pas fortement normalisant.

De quoi fortement normalisant signifie que toute expression a exactement une forme normale, où une forme normale est une expression qui ne peut être réduite, ce qui diffère de l'typée où chaque expression a au max une forme normale, il peut aussi n'ont pas de forme normale.

Si vous avez tapé lambda calculs pouvaient construire un point fixe de l'opérateur en ce que jamais, il était tout à fait possible pour une expression ne pas avoir de forme normale.

Un autre célèbre théorème, le Problème de l'Arrêt, implique que fortement normalisant les langues ne sont pas Turing, il dit que c'est impossible de décider (différent de prouver) de turing langue, ce que sous-ensemble de ses programmes s'arrête sur ce qui d'entrée. Si une langue est fortement normalisant, c'est decidable si elle s'arrête, soit il toujours s'arrête. Notre algorithme pour décider ce qui est du programme: true;.

Pour résoudre ce problème, ML-dérivés d'étendre le Système F de l'affaire et de laisser (rec) pour surmonter ce. Les fonctions peuvent ainsi se référer à eux-mêmes dans leurs définitions de nouveau, en effet pas de lambda-calculs de plus, il n'est plus possible de s'appuyer sur les fonctions anonymes seul pour toutes les fonctions calculables. Ils peuvent donc à nouveau entrer dans une boucle infinie et de retrouver leur turing-complétude.

Answer 4

Réponse courte: Vous ne pouvez pas.

Réponse longue: Le lambda calcul simplement typé est fortement normalisant. Cela signifie qu'il n'est pas Turing équivalent. La raison pour cela, fondamentalement, se résume au fait qu'un de Y combinator doit être primitive ou définies de manière récursive (comme vous l'avez trouvé). Il ne peut tout simplement pas être exprimé dans le Système F (ou plus simplement tapé des calculs). Il n'y a pas moyen de contourner cela (c'est prouvé, après tout). Le Y combinator, vous pouvez mettre en œuvre fonctionne exactement de la manière que vous voulez, bien que.

Je vous suggère d'essayer le régime si vous voulez un véritable Église de style Y combinator. Utiliser l'applicatif version donnée ci-dessus, comme les autres versions ne fonctionne pas, sauf si vous explicitement ajouter la paresse, ou l'utilisation d'un paresseux interpréteur Scheme. (Le schéma n'est techniquement pas complètement non typée, mais c'est dynamiquement typé, ce qui est assez bon pour cela.)

Voir ce pour la preuve de la forte normalisation: http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.127.1794

Après avoir réfléchi un peu plus, je suis assez sûr que l'ajout d'une primitive de Y combinator qui se comporte exactement de la manière la letrec défini un fait F Turing. Tout ce que vous devez faire pour simuler une machine de Turing est alors de mettre en œuvre la bande comme un entier (interpréter en binaire) et un passage (à la position de la tête).