Lambda Calcul étapes de Réduction

Lambda calcul

Lambda calcul a une sorte de spirale dans un grand nombre de mesures, de décisions résolution de problèmes fastidieux, et il peut être vraiment dur, mais il n'est en fait pas si mal que ça. Dans le lambda calcul, de leur ne sont que des lambdas, et tout ce que vous pouvez faire avec eux, c'est la substitution. Les Lambdas sont comme une fonction ou une méthode si vous êtes familier avec la programmation, ils sont des fonctions qui prennent une fonction en entrée, et de retourner une nouvelle fonction de sortie.

Il y a fondamentalement deux et demi processus en lambda calcul:

1) Alpha de Conversion - si vous présentez deux expressions lambda avec le même nom de variable à l'intérieur, vous modifiez l'un d'entre eux pour un nouveau nom de variable. Par exemple (λx.xx)(λx.x) devient quelque chose comme (λx.xx)(λy.y) ou (λx.xx)(λx'.x') après réduction. Le résultat est équivalent à ce que vous commencer avec, juste avec différents noms de variables.

2) de Réduction de la Bêta - Fondamentalement, il suffit de substitution. C'est le processus de l'appel de l'expression lambda avec entrée, et de sortie. Une expression lambda est comme une fonction, vous devez appeler la fonction en remplaçant l'entrée tout au long de l'expression. Prendre (λx.xy)z, la seconde moitié de l' (λx.xy), tout ce qui est après la période, est de sortie, vous gardez la sortie, mais en remplaçant la variable (nommé avant la période) avec la condition d'entrée. z est l'entrée, x est le nom du paramètre, xy est la sortie. Trouver toutes les occurrences du paramètre dans la sortie, et de les remplacer par l'entrée et c'est ce qu'il se réduit, de sorte (λx.xy)z => xy avec z substitué x, qui est zy.

2.5) Eta Conversion/Eta Réduction - C'est cas spécial de réduction, je n'appelle que la moitié d'un processus, parce que c'est un peu Bêta de Réduction, un peu, comme dans technichally ce n'est pas. Vous pouvez le voir écrit sur wikipédia ou dans un livre comme "l'Eta-conversion convertit entre λx.(f x) et de f lorsque x n'apparaît pas libre dans f", qui sonne vraiment déroutant. Tout ce qui signifie vraiment, c'est λx.(f x) = f si f ne pas utiliser de x. si Il fait réellement sens complet, mais est mieux illustré par un exemple. Considérer (λx.(λy.aa)x), c'est l'équivalent par l'eta réduction (λy.aa), car f = (λy.aa), qui n'a pas un x, vous pourriez montrer ce en la réduisant, comme il permettrait de résoudre à l' (λx.xx), ce qui est observable la même chose. Vous avez dit de se concentrer sur la bêta de réduction, et donc je ne vais pas discuter de l'eta de conversion dans le détail qu'elle mérite, mais beaucoup de gens ont donné leurs aller à elle sur la cs de la théorie de la pile d'échange

Sur la Notation pour la Bêta de Réduction:

Je vais utiliser la notation suivante pour remplacer la condition d'entrée dans la sortie:

(λ param . output)input => output [param := input] => result

Cela signifie que nous remplacer les occurrences de param en sortie, et c'est ce qu'elle se réduit à

Exemple:

(λx.xy)z

= (xy)[x:=z]

= (zy)

= zy

Assez de théorie, nous allons résoudre ce problème. Lambda Calcul est bon plaisir.

Le problème que vous est venu avec peut être résolu avec seulement Alpha de Conversion, et la Bêta de Réduction, Ne soyez pas effrayé par combien de temps le processus ci-dessous. C'est assez long, sans doute, mais pas d'étape de la résolution, il est vraiment dur.

(λxyz.xyz)(λx.xx)(λx.x)x

= (((λxyz.xyz)(λx.xx))(λx.x))x - allons ajouter des parenthèses dans "l'Ordre naturel", associativité gauche, abc réduit comme ((ab)c), où b est appliqué à un, et c est appliqué à la suite de cette

= (((λxyz.xyz)(λx.xx))(λx.x))x - Sélectionnez le plus profond imbriquée application et de réduire la première.

Le gras section réduit:

(λxyz.xyz)(λx.xx)

= (λx.λyz.xyz)(λx.xx) - signifie la même chose, mais nous tirez le premier paramètre puisque nous allons réduire l'écart et donc je veux qu'il soit clair

= (λx.λyz.xyz)(λx'.x, x') - Alpha de conversion, certaines personnes en tenir à de nouvelles lettres, mais j'aime ajoutant des numéros à la fin ou `s, de toute façon est bien. Parce que les deux expressions d'utiliser le paramètre x que nous avons à les renommer sur un côté, parce que les deux x sont des variables locales, et donc ne pas représenter la même chose.

= (λyz.xyz)[x := λx'.x 'x'] - Notation pour un bêta de réduction, nous allons supprimer le premier paramètre, et de le remplacer c'est occurrences dans la sortie avec ce qui est appliquée [a := b] indique qu'un être remplacé par b.

= (λyz.(λx'.x 'x') (y, z)) - La réduction réelle, nous remplaçons l'occurrence de x avec la lambda expression.

= (λyz. ((λx'.x 'x')y) z) - ordre Normal pour une parenthèse de nouveau, et le regard d'une autre application afin de réduire ce temps y est appliqué à (λx.xx`), donc permet de réduire que maintenant

= (λyz. ((x, x')[x := y]) z) - Mettre dans la notation pour la bêta de réduction.

= (λyz. (aa) z) - nous remplacer les deux occurrences de x 'x' pour Ys, et c'est maintenant entièrement réduit.

Ajouter ceci à l'origine de l'expression:

(((λxyz.xyz)(λx.xx))(λx.x))x

= ((λyz.(yy)z)(λx.x))x - Ceci n'est pas nouveau, juste de mettre ce que nous avons trouvé plus tôt dans.

= ((λyz.(yy)z)(λx.x))x - Attrapez le plus profond imbriquée à l'application, il est de (λx.x) appliqué à (λyz.(yy)z)

Nous allons résoudre cela à nouveau séparément:

(λyz.(yy)z)(λx.x)

= (λy.λz.(yy)z)(λx.x) - Simplement en apportant le premier paramètre pour la clarté de nouveau.

= (λz.(yy)z)[y := (λx.x)] - Mettre en bêta réduction de la notation, nous sortir le premier paramètre, et note que Ys est allumé (λx.x)

= (λz.((λx.x)(λx.x))z) - de La réduction ou de substitution, le gras section peut être réduite

= (λz.((x)[x := λx.x])z) - j'espère que vous avez compris l'idée maintenant, nous sommes au début de la bêta de réduire (λx.x)(λx.x) en le plaçant dans la forme (x)[x := λx.x]

= (λz.((λx.x))z) - Et là est la substitution

= (λz.(λx.x)z) - Nettoyer l'excès de la parenthèse, et que trouvons-nous, mais d'une autre application pour traiter

= (λz.(x)[x:=z]) - Pop le paramètre x, mis en notation

= (λz.(z)) - Effectuer la substitution

= (λz.z) - Nettoyez l'excès de la parenthèse

Remettre dans l'expression principale:

((λyz.(yy)z)(λx.x))x

= ((λz.z))x - Remplissage de ce que nous avons prouvé ci-dessus

= (λz.z)x - nettoyage excessif de la parenthèse, c'est maintenant réduite à une demande finale, x appliquée à(λz.z)

= (z)[z:=x] bêta - réduction, mis en notation

= (x) - faire de la substitution

= x - nettoyez l'excès de la parenthèse

Oui. La réponse est x, il réduit simplement groovy.

OriginalL'auteur rp.beltran