Arithmétique avec l'Église Numerals

Question

Je travaille par SICP, et problème 2.6 m'a mis quelque chose d'une situation embarrassante. En traitant avec des chiffres Eglise, le concept de codage zéro et 1 à être des fonctions arbitraires qui répondent à certains axiomes semble logique. En outre, la formulation directe provenant de numéros individuels en utilisant la définition de zéro, et une fonction add-1 est logique. Je ne comprends pas comment on peut former un opérateur plus.

Jusqu'à maintenant, j'ai cela.

(define zero (lambda (f) (lambda (x) x)))
(define (add-1 n)
  (lambda (f) (lambda (x) (f ((n f) x)))))

(define one (lambda (f) (lambda (x) (f x))))
(define two (lambda (f) (lambda (x) (f (f x)))))

En regardant à travers l'entrée de wikipedia pour lambda calcul , je trouve que la définition de en plus était PLUS: = λmnfx.mf (NFX). En utilisant cette définition que j'ai pu formuler la procédure suivante.

(define (plus n m)
  (lambda (f) (lambda (x) ((m f) ((n f) x)))))

Ce que je ne comprends pas, comment cette procédure peut être obtenue directement en utilisant uniquement les informations données par les procédures dérivées précédemment. Quelqu'un peut-il répondre à cela dans une sorte de preuve comme forme rigoureuse? Intuitivement, je pense que je comprends ce qui se passe, mais comme Richard Feynman a dit: « Si je ne peux pas construire, je ne peux pas le comprendre ... »

Answer 1

Il est en fait assez simple. Ce sera probablement considéré comme flamebait, mais les parens rendent plus difficile à voir - une meilleure façon de voir ce qui se passe est soit imaginer que vous êtes dans une langue cari, ou tout simplement utiliser le fait que le schéma a des fonctions multiples arguments et embrasser que ... Voici une explication qui utilise lambdas et des arguments multiples où commode:

• Chaque nombre N est codé comme

  (lambda (f x) ...apply (f (f (f ... (f x)))) N times...)
  

• Cela signifie que le codage de N est en fait

  (lambda (f x) (f^N x))
  

  où f^N est exponentiation fonctionnelle.

• Une façon simple de le dire (en supposant corroyage): le nombre N est codé comme

  (lambda (f) f^N)
  

  N est en fait un "augmentation de la puissance de N" Fonction

• Maintenant, prenez votre expression (regarder à l'intérieur des lambdas ici):

  ((m f) ((n f) x))
  

  depuis n est est un codage d'un certain nombre, il est que exponentiation, donc c'est en fait:

  ((m f) (f^n x))
  

  et la même chose pour m:

  (f^m (f^n x))
  

  et le reste devrait être évident ... Vous avez des applications m de f appliquées sur les applications n de f appliquée sur x.

• Enfin, quitter certains amusant - est ici une autre façon de définir plus:

  (define plus (lambda (m) (lambda (n) ((m add1) n))))
  

  (Eh bien, pas trop de plaisir, puisque celui-ci est probablement plus évidente.)

Answer 2

^{(Assurez-vous que vous comprenez fonctions d'ordre supérieur ) .} Alonzo Church 's non typé lambda calcul fonction est le seul type de données primitive. Il n'y a pas de chiffres, booléens, des listes ou toute autre chose, seules les fonctions. Les fonctions peuvent avoir seulement 1 argument, mais les fonctions peuvent accepter et / ou retour fonctions non valeurs de ces fonctions, mais les fonctions elles-mêmes. Par conséquent, pour représenter des nombres, des booléens, des listes et d'autres types de données, vous devez trouver une façon intelligente pour les fonctions anonymes de se tenir pour eux. chiffres Église est la façon de représenter nombres naturels . Trois constructions primitives dans la plupart des calculs typées lambda sont:

1. λx.x, une fonction identité , accepte une fonction et retourne immédiatement.
2. λx.x x, l'auto-application.
3. λf.λx.f x, application de fonction, prend une fonction et un argument, et applique une fonction à un argument.

Comment vous encodez 0, 1, 2 comme rien d'autre que des fonctions? Nous avons besoin d'une certaine façon de construire la notion de système dans le quantité . Nous avons des fonctions que, chaque fonction peut être appliquée que pour 1 argument. Où peut-on voir la quantité quoi que ce soit ressemblante? Hé, on peut appliquer une fonction à un paramètre plusieurs fois! Il y a évidemment un sentiment de quantité en 3 invocations répétées d'une fonction: f (f (f x)). Donc, nous allons dans le calcul il encodent lambda:

• 0 = λf.λx.x
• 1 = λf.λx.f x
• 2 = λf.λx.f (f x)
• 3 = λf.λx.f (f (f x))

Et ainsi de suite. Mais comment allez-vous de 0 à 1 ou 1 à 2? Comment voulez-vous écrire une fonction qui, étant donné un certain nombre, renverrait un nombre incrémentée de 1? Nous voyons le modèle dans l'église des chiffres que le terme commence toujours par λf.λx. et une fois que vous avez une application répétée fini de f , donc nous avons besoin d'obtenir en quelque sorte dans le corps de λf.λx. et l'envelopper dans une autre f. Comment changer un corps d'une abstraction sans réduction? Eh bien, vous pouvez appliquer une fonction, envelopper le corps dans une fonction, puis envelopper le nouveau corps dans l'ancienne abstraction lambda. Mais vous ne voulez que des arguments au changement, donc vous appliquez des abstractions aux valeurs du même nom:. ((λf.λx.f x) f) x → f x, mais ((λf.λx.f x) a) b) → a b, ce qui est pas ce que nous avons besoin

C'est pourquoi add1 est λn.λf.λx.f ((n f) x): vous appliquez n à f et x ensuite de réduire l'expression du corps, puis appliquer f à ce corps, puis abstrait nouveau avec λf.λx.. Exercice: aussi voir qu'il est vrai, apprendre rapidement β-réduction et réduire (λn.λf.λx.f ((n f) x)) (λf.λx.f (f x)) à incrément 2 par 1.

comprendre maintenant l'intuition derrière envelopper le corps dans un autre appel de fonction, comment pouvons-nous mettre en œuvre plus de 2 chiffres? Nous avons besoin d'une fonction qui, λf.λx.f (f x) donné (2) et λf.λx.f (f (f x)) (3), retournerait λf.λx.f (f (f (f (f x)))) (5). Regardez 2. Et si vous pouviez remplacer son x avec le corps de 3, qui est f (f (f x))? Pour obtenir le corps de 3, il est évident, il suffit d'appliquer à f puis x. Maintenant, appliquez 2 à f, mais appliquer ensuite au corps de 3, pas x. ensuite wrap dans λf.λx. à nouveau. λa.λb.λf.λx.a f (b f x)

Conclusion: Pour ajouter 2 numéros a et b ensemble, qui sont tous deux représentés en chiffres Église, vous voulez remplacer x en a avec le corps de b, de sorte que f (f x) + f (f (f x)) = f (f (f (f (f x)))). Pour ce faire, appliquez a à f, puis à b f x.

Answer 3

La réponse de Eli est techniquement correcte, mais depuis au point que cette question est posée à la procédure de #apply n'a pas été mis en place, je ne pense pas que les auteurs destinés à l'étudiant d'avoir une connaissance de ce ou de concepts tels que taitement être en mesure de répondre à cette question.

Ils un guide à peu près à la réponse en suggérant que l'on applique la méthode de substitution, puis à partir de là il faut remarquer que l'effet de l'addition est une composition d'un numéro sur l'autre. La composition est un concept a été introduit dans l'exercice 1,42; et que tout ce qui est nécessaire pour comprendre comment une procédure additif peut fonctionner dans ce système.

; The effect of procedure #add-1 on `one`, and `two` was the composition of `f` 
; onto `one` and `f` onto `two`.
;
; one   : (λ (f) (λ (x) (f x)))
; two   : (λ (f) (λ (x) (f (f x))))
; three : (λ (f) (λ (x) (f (f (f x)))))
;
; Thus one may surmise from this that an additive procedure in this system would
; work by composing one number onto the other.
;
; From exercise 1.42 you should already have a procedure called #compose.
;
; With a little trial and error (or just plain be able to see it) you get the
; following solution.

(define (adder n m)
  (λ (f)
    (let ((nf (n f))
          (mf (m f)))
      (compose nf mf))))