лямбда-исчисление (SML) - Нанести церковный номер другого

Question

Я пытаюсь понять функцию возведения в степени на Чёрче:

fun power m n f = n m f; 

В нем я вижу умножение. Я знаю, что это неправильно, потому что умножение:

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

и я думаю, что понял это.

Проблема в том, что я не могу понять, какая функция вызывает применение номера церкви к другому.

Например, что производит это выражение?

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

Благодаря

Answer 1

, если результат вашего расчета является церковь число, вы можете вычислить его Инт-значение, передавая правопреемника-функции и нуль:

(fn x=> x+1) 0 

В вашем примере:

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

результат:

val it = 9 : int 

так что вы рассчитывали 3^2

Срок

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

сводится к

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

Но SML не может сократить к этому сроку, он должен параметры так, он может вычислить конкретное значение.

Лучшим языком для игры с исчислением лямбда является Haskell, потому что он использует ленивую оценку.

Вы можете сократить срок

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

сами:

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!