calcul Lambda (SML) - Appliquer un numéro d'église à l'autre

Question

J'essaie de comprendre la fonction d'exponentiation sur les chiffres de l'Église:

fun power m n f = n m f; 

Dans ce document, je vois une multiplication. Je sais que c'est faux, parce que la multiplication est:

fun times m n f = m (n f); 

et je pense l'avoir compris. Le problème est que je ne suis pas capable de comprendre quelle fonction produit l'application d'un numéro d'église à un autre.

Par exemple, que produit cette expression?

(fn x => fn y => x (x y)) (fn x => fn y => x (x (x y))); 

Merci

Answer 1

si le résultat de votre calcul est un numéro d'église, vous pouvez calculer sa valeur int en passant une fonction successeur et zéro:

(fn x=> x+1) 0 

Dans votre exemple:

(fn x => fn y => x (x y)) (fn x => fn y => x (x (x y))) (fn x=> x+1) 0; 

le résultat est:

val it = 9 : int 

si vous avez calculé 3^2

Le terme

(fn x => fn y => x (x y)) (fn x => fn y => x (x (x y))) 

réduit à

(fn x => fn y => x (x (x (x (x (x (x (x (x y))))))))) 

Mais sml ne peut pas réduire à ce terme, il a besoin des paramètres afin qu'il puisse calculer une valeur concrète.

Un meilleur langage pour jouer avec Lambda Calculus est Haskell, car il utilise une évaluation paresseuse.

Vous pouvez réduire la durée

(fn x => fn y => x (x y)) (fn x => fn y => x (x (x y))) 

par vous-même:

fn x => fn y => x (x y) (fn x => fn y => x (x (x y))) 
reduce x with (fn x => fn y => x (x (x y))): 
fn y => (fn x => fn y => x (x (x y))) ((fn x => fn y => x (x (x y))) y) 
rename y to a in the last (fn x => fn y => x (x (x y))) 
and rename y to b in the first (fn x => fn y => x (x (x y))): 
fn y => (fn x => fn b => x (x (x b))) ((fn x => fn a => x (x (x a))) y) 
reduce x in (fn x => fn a => x (x (x a))) with y: 
fn y => (fn x => fn b => x (x (x b))) (fn a => y (y (y a))) 
reduce x in (fn x => fn b => x (x (x b))) with (fn a => y (y (y a))): 
fn y => fn b => (fn a => y (y (y a))) ((fn a => y (y (y a))) ((fn a => y (y (y a))) b)) 
we reduce a with b in the last term: 
fn y => fn b => (fn a => y (y (y a))) ((fn a => y (y (y a))) (y (y (y b)))) 
we reduce a with (y (y (y b))) in the last term: 
fn y => fn b => (fn a => y (y (y a))) (y (y (y (y (y (y b)))))) 
we reduce a with (y (y (y (y (y (y b)))))) in the last term: 
fn y => fn b => y (y (y (y (y (y (y (y (y b)))))))) 
we are done!