Lambda Calculus: construire une fonction qui prend plus d'arguments à chaque itération

Question

J'essaye de construire une fonction qui prend un nombre donné d'arguments et retourne toujours la même valeur.

Ceci fait partie d'un devoir. Il y a un indice fourni:

Le "k-way T" est une fonction qui prend k arguments et renvoie toujours T. A "0-way T" est juste T.

Où k est fourni en tant que numéro d'église et T est l'expression lambda pour True (\ x. \ yx).

La tâche complète consiste à fournir une expression lambda qui calcule une fonction OR de type K. Où le nombre d'arguments 'boolean' est fourni avant les arguments 'boolean'. par exemple:

((OR 3) F T F) 

Mais pour l'instant, je suis en train de créer qui prend k arguments et renvoie toujours T. Le k est fourni en tant que premier argument. Donc, fondamentalement, je ne voulais pas créer une fonction qui ait un argument de plus pour chaque «itération» de l'église.

Mais de toute façon je suis complètement coincé. Est-ce que je peux le faire avec seulement un numéro d'église? Ou ai-je besoin d'une récursivité (Y-Combinator)?

En général: existe-t-il de bons outils (par exemple pour la visualisation) qui prennent en charge la création d'expressions lambda.

Je suis vraiment étonné de la puissance du lambda-calcul et je veux vraiment l'apprendre. Mais je ne sais pas comment ...

Merci à l'avance

Answer 1

Je vais vous montrer comment mettre en œuvre la fonction TRUE. Puisque k n'est pas corrigé, vous avez besoin d'un combinateur à virgule fixe (Y ferait l'affaire, mais ce n'est pas le seul combinateur à virgule fixe). Tout d'abord quelques mots sur la notation que j'ai utilisée ci-dessous: iszero (prend un nombre d'église, vérifie si c'est l'église zéro et retourne un booléen d'église), T (la valeur booléenne vraie codée par l'église), pred (le fonction prédécesseur pour les numéros d'église), et Y (un combinateur à virgule fixe).

let TRUE = Y (λr. λn. (iszero n) T (λx. (r (pred n)))) 

Notez que let ne fait pas partie de la syntaxe de calcul lambda, il est métasyntaxe d'introduire un nom (pour nous).

Cela fonctionne comme suit: Y sorte deconvertit l'argument r en « soi » - lorsqu'une fonction appelle r il appelle lui-même.Pour illustrer cela, je vais réécrire ce qui précède en forme récursive (avertissement: c'est à des fins d'illustration seulement, lambda calcul ne permet pas cela, puisque toutes les fonctions sont anonymes, vous ne pouvez pas les appeler en utilisant leurs noms - il n'y a aucun moyen pour cela):

let TRUE = λn. (iszero n) T (λx. (TRUE (pred n))) 

J'ai dépouillé de la partie λr. et remplacé par rTRUE (encore une fois, s'il vous plaît ne le faites pas dans vos devoirs, il n'est pas valide lambda-calcul).

Et cette définition est plus facile à comprendre: si TRUE est appelé comme celui-ci TRUE 0 il retourne juste T, sinon il retourne une fonction d'un argument qui s'enroule autour d'une fonction de (n - 1) arguments, représentant essentiellement une fonction de n arguments. En ce qui concerne votre question sur les outils, vous pouvez utiliser Scheme/Racket, car cela vous aidera à vérifier que votre «code lambda calculus» fonctionne correctement. Par exemple, voici une implémentation de TRUE Racket:

(define (Y f) 
    ((lambda (x) (x x)) 
    (lambda (x) (lambda (a) ((f (x x)) a))))) 

(define TRUE 
    (Y (lambda (r) 
     (lambda (n) 
     (if (zero? n) 
      #t 
      (lambda (x) (r (sub1 n)))))))) 

;; tests 
> (TRUE 0) 
#t 
> ((TRUE 1) #f) 
#t 
> (((TRUE 2) #f) #f) 
#t 
> ((((((TRUE 5) #f) #f) #f) #f) #f) 
#t 

Je dois ajouter que j'utilisé ici INTÉGRÉE dans booléens, entiers, si l'expression, sub1, zero? au lieu de ceux codés Église. Sinon, cela rendrait cet exemple beaucoup plus grand (ou incomplet).