Lambda hesabı (SML) Ben kilise rakamlarıyla ilgili üs alma işlevini anlamaya çalışıyorum başka

Question

bir kilise numarasını uygulayın. Bunun yanlış olduğunu biliyorum, çünkü çarpım:

ve bunu anladım. Sorun şu ki, hangi işlevin bir kilise numarasının diğerine uygulanmasını oluşturduğunu anlayamıyorum.

Örneğin, bu ifade ne üretir?

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

Teşekkür

Answer 1

senin hesaplamanın sonucu bir kilise sayısı, bir halef-fonksiyonu ve sıfır geçirmekle int değer hesaplayabilirsiniz ise: sizin örnekte

(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; 

sonucudur:

o hesaplamak, böylece

val it = 9 : int 

böylece

(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))))))))) 

Ama sml için azaltır Terim bu terime azaltamaz^2

3 hesaplanan bu parametreler ihtiyacı somut bir değer.

Lambda Calculus ile oynamak için daha iyi bir dil Haskell, çünkü tembel değerlendirme kullanır.

kendiniz terimini

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

azaltabilir:

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!