ラムダ計算（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 

がそのようにあなたが

(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に軽減用語は、この用語に減らすことはできません^ 2

3を計算し、それがパラメータを必要とします具体的な価値

Lamby Calculusで遊ぶのに適した言語は、遅延評価を使用するため、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!