Mon conseil, de ma propre expérience limitée mais récente:
- Est-ce une chose à la fois: effectuer une conversion alpha, une réduction de bêta ou une conversion eta. Notez dans la marge de la page que vous travaillez sur ce que vous avez fait pour atteindre la ligne suivante. Si ces mots ne vous sont pas familiers, ce qu'ils font sera - jetez un coup d'oeil sur Wikipedia.
Un résumé rapide de ces étapes de réduction:
Alpha signifie simplement changer les noms des variables dans un contexte toujours:
λfx. f (f x) => λgx. g (g x)
Beta signifie simplement appliquer le lambda à un argument
(λf x. f x) b => λx. b x
Eta est simplement «déballer» une fonction inutilement enveloppée qui ne change pas sa signification.
λx.f x => f
Puis
Utilisez beaucoup de conversion alpha pour modifier les noms des variables pour rendre les choses plus claires. Tous ces f s, ça va toujours être déroutant.Vous avez fait quelque chose de similaire avec le " sur votre deuxième ligne
Imaginez que vous êtes un calcul! Ne pas sauter en avant ou sauter une étape lorsque vous évaluez une expression. Fais juste la prochaine chose (et une seule chose). Ne vous déplacez plus vite qu'une fois que vous êtes sûr de vous déplacer lentement. Envisagez de nommer certaines expressions et de ne leur substituer que des expressions lambda lorsque vous devez les évaluer. Je note habituellement la substitution dans la marge de la page comme by def car ce n'est pas vraiment une étape de réduction. Quelque chose comme:
add two three
(λm n f x. m f (n f x)) two three | by def
Ainsi, en suivant les règles ci-dessus, voici mon exemple travaillé:
two = λfx. f (f x)
three = λfx. f (f (f x))
add = λmnfx. m f (n f x)
0 | add two three
1 | (λm n f x. m f (n f x)) two three | by def
2 | (λn f x. two f (n f x)) three | beta
3 | (λf x. two f (three f x)) | beta
4 | (λf x. two f ((λfx. f (f (f x))) f x)) | by def
5 | (λf x. two f ((λgy. g (g (g y))) f x)) | alpha
6 | (λf x. two f ((λy. f (f (f y))) x)) | beta
7 | (λf x. two f (f (f (f x)))) | beta
8 | (λf x. (λfx. f (f x)) f (f (f (f x)))) | by def
9 | (λf x. (λgy. g (g y)) f (f (f (f x)))) | alpha
10 | (λf x. (λy. f (f y)) (f (f (f x)))) | beta
11 | (λf x. (λy. f (f (f (f (f x)))))) | beta
+1 Ce fait ma journée, merci! –
merci beaucoup. Franchement, je n'ai pas compris comment aller avec les œufs d'Alligator! –
J'ai par le passé trébuché sur ces alligators, mais cela m'a semblé comme des freakings de quelque fou. Bien que je connaisse très bien Lambda Calculus, je ne pouvais pas comprendre ce que ces alligators avaient à faire avec cela et comment cela pourrait-il aider à l'interpréter: -P Donc, mon opinion personnelle est que ça aide beaucoup à comprendre le LC, mais introduit confusion supplémentaire. – SasQ