Eglise Numerals: comment encoder zéro dans le calcul lambda?

Question

J'apprends le calcul lambda, mais je ne peux pas comprendre semble l'encodage pour le nombre 0.

comment est « fonction qui prend une fonction et une seconde valeur et applique zéro fois la fonction sur l'argument » zéro? Est-il un autre moyen d'encoder zéro? Quelqu'un pourrait-il me aider ici encode 0?

Answer 1

« fonction qui prend une fonction et une seconde valeur et applique la fonction zéro fois sur l'argument » A est, bien sûr, pas zéro. Il est un encodage de zéro. Lorsque vous traitez avec le calcul lambda ordinaire, vous devez encoder des chiffres (ainsi que d'autres types primitifs) d'une certaine façon, et il y a quelques exigences dictées pour chacun de ces types. Par exemple, une exigence de nombres naturels est d'être en mesure d'ajouter 1 à un nombre donné, et une autre est de pouvoir distinguer zéro des plus grands nombres (si vous voulez en savoir plus, recherchez « Peano Arithmétique »). L'encodage populaire que Dario cité vous donne ces deux choses, et il est également représentant un entier N par une fonction qui fait quelque chose (codé comme argument de f) N fois -. Ce qui est une sorte d'une façon naturelle d'utiliser Naturals

Il y a d'autres encodages qui sont possibles - par exemple, une fois que vous pouvez représenter les listes, vous pouvez représenter N comme une liste d'éléments N. Ces codages ont leurs avantages et leurs inconvénients, mais celle ci-dessus est de loin le plus populaire.

Answer 2

Voir wikipedia :

0 ≡ λf.λx. x
1 ≡ λf.λx. f x
2 ≡ λf.λx. f (f x)
3 ≡ λf.λx. f (f (f x))
...
n ≡ λf.λx. fn x

Answer 3

Si vous apprenez Lambda Calcul, vous savez probablement déjà que λxy.y arg1 * arg2 * sera réduit à arg2 , puisque x est remplacé par rien, et reste (λy.y) est la fonction identité.

Vous pouvez écrire zéro dans bien d'autres façons (par exemple trouver une autre convention), mais il y a de bonnes raisons d'utiliser λxy.y. Par exemple, vous voulez zéro être le premier nombre naturel, de sorte que si vous appliquez la fonction successeur, vous obtenez 1, 2, 3, etc. Avec la fonction λabc.b (abc), vous obtenez λxy.x (y ), λxy.x (x (y)), λxy.x (x (x (y))), etc., autrement dit, vous obtenez un système entier.

De plus, vous voulez zéro être l'élément neutre par rapport à l'addition. Avec notre fonction successeur S: = λabc.b (abc), nous pouvons définir n + * m * comme n m , à savoir, n fois l'application de la fonction successeur m . Nos zéro λxy.y satisfait ce, à la fois 0 S m et m S 0 réduire à m .