lambda calcul pour la programmation fonctionnelle

Question

en lambda calcul (λ x. Λ y λ s λ z. Xs (ysz)) est utilisé pour l'addition de deux chiffres de l'Église comment pouvons-nous expliquer cela, y at-il une bonne ressource le 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 l'addition car elle substitue en effet (f2 s z), le nombre représenté par f2, au "zéro" à l'intérieur (f1 s z). Exemple: Prenons deux pour f2, s s z sous forme développée. f1 est un: s z. Remplacer ce dernier z par f2 et vous obtenez s s s z, le formulaire développé pour trois.

Ce serait plus facile avec un tableau et agiter la main, désolé.

Answer 2

Dans le calcul lambda, vous codez un type de données en fonction des opérations qu'il 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 but principal de calcul est fournir une liaison à l'itération. Ainsi, on code un nombre naturel comme un opérateur qui prend en entrée une fonction f, une valeur x, et itère 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ération n fois, c'est (NFX), puis itérer pour m fois de plus, à partir du résultat précédent, qui est

       m f (n f x) 

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

        m (n f) x 

L'encodage précédent des types de données est plus formellement expliqué dans les termes des constructeurs et des éliminateurs correspondants (ce que l'on appelle le codage Bohm-Berarducci ).