Somme des éléments de la liste et longueur de la liste dans le calcul lambda

Question

J'essaie de faire fonctionner pour calculer la somme des éléments de la liste et la longueur de la liste dans le calcul lambda.
Exemple d'une liste: a := [1, 2, 3] = λcn.c 1 (c 2 (c 3 n))
sum a doit retourner 6 et len a devrait revenir 3.

j'ai écrit versions récursives:

len = λl.if (empty l) 0 (plus 1 (len (tail l))) 
sum = λl.if (empty l) 0 (plus (head l) (sum (tail l))) 

où, si, vide, plus, la queue sont d'autres fonctions de lamda.

Alors je l'ai fait un truc avec combinateur point fixe:

len = λl.if (empty l) 0 (plus 1 (len (tail l))) 
len = λfl.if (empty l) 0 (plus 1 (f (tail l))) len 
len = Y λfl.if (empty l) 0 (plus 1 (f (tail l))) 

où Y = λf.(λx.f(x x))(λx.f(x x))
Juste la même chose pour la somme. Alors maintenant j'ai des versions non récursives. Mais je ne peux pas obtenir la forme bêta normale en utilisant la réduction bêta ici.
Je me demande s'il existe des formes bêta-normales de ces fonctions et à quoi elles ressemblent.

Answer 1

Ceux-ci peuvent être mis en œuvre beaucoup plus facilement étant donné qu'une liste est codée par son propre itérateur:

a := [1, 2, 3] = λcn.c 1 (c 2 (c 3 n)) 

signifie qu'une liste est fonction de deux arguments: un à utiliser sur cons noeuds et un à utiliser à la fin sur le constructeur nil.

En conséquence, vous pouvez mettre en œuvre length en disant:

• ignorer la valeur stockée dans un nœud cons et retour +1
• remplacer nil avec 0

qui se traduit par:

length := λl. l (λ_. plus 1) 0 

qui élargirait à (à chaque ligne, l'expression en gras est d'être soit déplié ou réduite):

length a 
(λl. l (λ_. plus 1) 0) a 
(λl. l (λ_. plus 1) 0) (λcn.c 1 (c 2 (c 3 n))) 
(λcn. c 1 (c 2 (c 3 n))) (λ_. plus 1) 0 
(λn. (λ_. plus 1) 1 ((λ_. plus 1) 2 ((λ_. plus 1) 3 0))) 0 
(λ_. plus 1) 1 ((λ_. plus 1) 2 ((λ_. plus 1) 3 0)) 
(plus 1) ((λ_. plus 1) 2 ((λ_. plus 1) 3 0)) 
(plus 1) ((plus 1) ((λ_. plus 1) 3 0)) 
(plus 1) ((plus 1) ((plus 1) 0)) 
(plus 1) ((plus 1) 1) 
(plus 1) 2 
= 3

De même, vous pouvez mettre en œuvre sum en disant:

• utilisation + de combiner la valeur stocké dans un cons et le résultat de l'évaluation de la queue
• remplacer nil par 0

qui se traduit par:

sum := λl. l plus 0 

qui élargirait à

sum a 
(λl. l plus 0) a 
(λl. l plus 0) (λcn.c 1 (c 2 (c 3 n))) 
(λcn. c 1 (c 2 (c 3 n))) plus 0 
(λn. plus 1 (plus 2 (plus 3 n))) 0 
plus 1 (plus 2 (plus 3 0)) 
plus 1 (plus 2 3) 
plus 1 5 
= 6