lambda-calcul pour la programmation fonctionnelle

Question

dans le calcul lambda (λ x. Λ y. Λ s. Λ z. X s (y s z)) est utilisé pour plus de deux chiffres de l'Église comment pouvons-nous expliquer cela, est-il une bonne ressource du lambda-calcul pour la programmation fonctionnelle? votre aide est très appréciée

Answer 1

En fait λ f1. λ f2. λ s. λ z. (F1 s (f2 s z)) calcule outre parce qu'il est en remplacement de l'effet (f2 s z), le nombre représenté par f2, le "zéro" à l'intérieur (z s f1).

Exemple: Prenons deux pour f2, s s z sous forme expansée. f1 est une: s z. Remplacer cette dernière z par f2 et vous obtenez s s s z, la forme développée pour trois.

Ce serait plus facile avec un tableau noir et la main en agitant, désolé.

Answer 2

Dans le calcul lambda, vous codez un type de données en fonction des opérations qu'elle induit. Par exemple, un booléen est juste une fonction de choix qui prend en entrée deux valeurs a et b et renvoie soit a ou b:

                      true = \a,b.a   false = \a,b.b

Quelle est l'utilisation d'un nombre naturel? Son principal objectif est de calcul fournir une borne d'itération. Donc, on code un nombre naturel comme un opérateur qui prend en entrée une fonction f, une valeur x, et itérer l'application de f au-dessus de x à n fois:

                        n = \f,x.f(f(....(f x)...))

avec n occurrences de f.

Maintenant, si vous voulez itérer n + m fois la fonction f à partir de x vous devez commencer à itérer n fois, c'est (n f x), puis itérer pour m fois de plus, à partir du résultat précédent, à savoir

                                m f (n f x)

De même, si vous voulez itérer n * m fois que vous devez itérer m fois le fonctionnement de l'itération n fois f (comme dans les deux boucles imbriquées), qui est

                                 m (n f) x  

Le codage précédent de façon plus formelle est datatypes expliqué en termes des constructeurs et des éliminateurs correspondantes (que l'on appelle Bohm-Berarducci codage).