2015-10-14 3 views
-1

J'essaie de comprendre le combinateur à virgule fixe. Je pense qu'il est utilisé par certaines langues pour implémenter la récursivité. Le principal problème est que je ne pouvais pas obtenir la définition suivante:Y-Combinator definiton

click here to see image

Alors s'il vous plaît expliquer l'image.

+0

Avez-vous fait vous-même la recherche, par exemple lisez l'article [Wikipedia] (https://en.wikipedia.org/wiki/Fixed-point_combinator#Fixed_point_combinators_in_lambda_calculus)? –

+0

@HansLub oui je l'ai lu de wikipedia et je ne l'ai toujours pas compris, c'est pourquoi posté ici. – Charlie

+0

@HansLub comment liriez-vous cette définition de l'image que j'ai liée? – Charlie

Répondre

0

C'est une implémentation du combinateur à virgule fixe dans le lambda-calcul (appelé un combinateur Y). Il vérifie l'équation

enter image description here

Il n'y a pas trop à « obtenir » au sujet de la mise en œuvre autre qu'elle satisfait au-dessus.

L'entrée de wikipedia here montre comment le Y-Combinator satisfait l'équation ci-dessus

+0

J'ai lu l'entrée wikipedia, mais n'est pas encore clair la sémantique de cette définition. spécialement la partie où il dit: (lamba x.f (x x)) .. pourquoi le paramètre x est-il répété 2 fois dans la fonction f. pourriez-vous écrire ici comment lire cette définition? – Charlie

+1

'(x x)' n'est pas 'x' répété deux fois, mais x est appliqué à lui-même. Si vous écrivez les deux étapes de réduction de β données dans l'article [wikipedia] (https://en.wikipedia.org/wiki/Fixed-point_combinator#Fixed_point_combinators_in_lambda_calculus), vous voyez que c'est essentiel pour réduire 'Y g' à' g (Y g) 'Note: c'est la direction de la réduction, * not *' g (Y g) 'à' Y g' comme on pourrait s'y attendre pour un point fixe ("branchez le point de repère' Y g' dans 'g ', démarrez le réducteur et récupérez' Y g': c'est * pas * comment ça marche ...) –