Comment puis-je définir y combinateur sans « laisser rec »?

Question

Dans presque tous les exemples, un y-Combinator dans les langues de type ML 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 pour définir l'y combinateur en utilisant let rec ....

Je veux définir ce combinateur sans utiliser récursion, en utilisant la définition standard:

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

Une traduction directe est la suivante:

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 l'y combinateur en F # sans utiliser let rec ...?

Answer 1

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

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

Maintenant, le Y-Combinator peut être écrit:

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

Malheureusement, vous constaterez 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'aide de cette Combinator provoquera un débordement de pile. , Vous avez besoin au lieu d'utiliser la version ordre du applicative 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 la paresse explicite pour définir l'ordre normale 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 pour inconvénient que les définitions de fonction récursive doivent maintenant une force explicite de la valeur paresseuse (en utilisant la propriété Value):

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 valeurs récursives non-fonction, tout comme vous pourriez dans une langue paresseuse:

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

En dernière alternative, vous pouvez essayer de mieux rapprocher le calcul typées lambda en utilisant la boxe et downcasting. Cela vous donne (en utilisant à nouveau la version ordre du applicative Y-Combinator):

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

Ceci présente l'inconvénient évident qu'il provoque la boxe et non nécessaire unboxing, mais au moins cela est tout à fait interne à la mise en œuvre et ne conduira jamais réellement à l'échec lors de l'exécution.

Answer 2

Je dirais qu'il est impossible, et a demandé pourquoi, je handwave et invoquer le fait que simplement typé lambda-calcul a la propriété normalisation . En bref, tous les termes du lambda-calcul simplement typé se terminent (par conséquent, Y ne peut pas être défini dans le lambda-calcul simplement typé).

système de type de F # est pas exactement le système de type de lambda-calcul simplement typé, mais il est assez proche. F # sans let rec est vraiment proche du lambda-calcul simplement typé - et, je le répète, dans cette langue que vous ne pouvez pas définir un terme qui ne se termine pas, et qui exclut la définition Y aussi.

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

EDIT: KVB montre dans sa réponse que les définitions de type (l'une des caractéristiques absentes du simplement typé lambda-calcul, mais présents dans let-rec-less F #) permettent d'obtenir une sorte de récursion. Très intelligent.

Answer 3

cas et laisser des déclarations sur les dérivés ML sont ce qui le rend complet Turing, je crois qu'ils sont basés sur le système F et non simplement typé mais le point est le même.

système F ne peut pas trouver un type pour le tout point fixe Combinator, si elle le pouvait, il n'a pas été fortement normalisant.

Quels sont les moyens fortement normalisante est que toute expression a exactement un forme normale, où une forme normale est une expression qui ne peut être réduite plus loin, cela diffère de typées où chaque expression a à max une forme normale, il peut aussi avoir aucune forme normale du tout.

Si lithiase lambda tapé pourrait construire un opérateur de point fixe de quelle que soit la manière, il était tout à fait possible pour une expression ne pas avoir de forme normale.

Un autre fameux théorème, le problème d'arrêt, implique que les langues fortement normalisant ne sont pas Turing complet, il dit que c'est impossible de décident (différent de prouver) d'un turation langage complet ce sous-ensemble de ses programmes seront mettre un terme à ce que l'entrée. Si une langue est fortement normalisant, il est décidable si elle arrête, à savoir qu'il toujours arrête. Notre algorithme pour décider c'est le programme. true;

Pour résoudre ce problème, ML dérivés étendent Système-F avec le cas et laisser (rec) pour surmonter cela. Les fonctions peuvent ainsi se référer à eux-mêmes dans leurs définitions à nouveau, ce qui les rend en effet pas lithiase lambda plus du tout, il est plus possible de compter uniquement sur les fonctions anonymes pour toutes les fonctions calculables. Ils peuvent ainsi entrer à nouveau des boucles infinies et retrouver leur turation-complet.

Answer 4

Réponse courte:. Vous ne pouvez pas

Réponse longue: Le calcul lambda simplement typé est fortement normalisant. Cela signifie qu'il n'est pas équivalent Turing. La raison pour cela se résume essentiellement au fait qu'un combinateur Y doit être soit primitive ou défini récursive (comme vous l'avez trouvé). Il ne peut simplement pas être exprimé dans le système F (ou lithiase dactylographiée plus simple). Il n'y a pas moyen de contourner cela (il a été prouvé, après tout). Le Y Combinator vous peut mettre en œuvre fonctionne exactement comme vous le souhaitez, cependant.

Je vous suggère d'essayer si vous voulez système un vrai style Eglise Y Combinator. Utilisez la version donnée ci-dessus applicative, que d'autres versions ne fonctionneront pas, sauf si vous ajoutez explicitement la paresse, ou d'utiliser un interpréteur Scheme paresseux. (Schéma est techniquement pas complètement typées, mais il est typé dynamiquement, ce qui est assez bon pour cela.)

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

Après avoir réfléchi un peu plus, je suis sûr que l'ajout d'un combinateur primitif Y qui se comporte exactement comme celle définie letrec ne fait complète système F Turing. Tout ce que vous devez faire pour simuler une machine de Turing est alors mettre en œuvre la bande comme un entier (interprété en binaire) et un décalage (pour positionner la tête).