lambda - ラムダ計算の構文木

Question

以下の式の構文木をどのように描画するかを理解しようとしています。まず、これはどの程度正確に動作していますか？パラメータとして1と2を使用しているように見えますが、nが0の場合は、を返しmます。

また、誰かがツリーまたは例を解析するための開始点を示すことができますか？見つかりませんでした。

Answer 1

関数が定義されたら、関数自体に引数を適用し、適用された引数の結果である新しい関数を返します。

そのコードを作成するために使用した言語はわかりませんが、アプリケーションの結果は次のようになります。

\f.\n.\m.if isZero n then m else f (pred n) (succ m)

は関数の定義なので\f、上記は次のように記述できます。

add = (\n.\m.if (isZero n) then m else add (pred n) (succ m))

そしてアプリケーション：

add = (\n.\m.if (isZero n) then m else add (pred n) (succ m))
add 1 2
(\n.\m.if (isZero n) then m else add (pred n) (succ m)) 1 2

最も外側の変数を最も内側の引数（この場合はn1）に置き換えます。

((**\n**.\m.if (isZero n) then m else f (pred **n**) (succ m)) **1**) 2
(\m.if (isZero 1) then m else add (pred 1) (succ m)) 2

それを少し解決します：

(\m.if (isZero 1) then m else add **(pred 1)** (succ m)) 2
(\m.if (isZero 1) then m else add 0 (succ m)) 2

2番目の引数を適用し、解決します。

(**\m**.if (isZero 1) then **m** else add 0 (succ **m**)) **2**
(if (isZero 1) then 2 else add 0 (succ 2))
(if (isZero 1) then 2 else add 0 **(succ 2)**)
(if (isZero 1) then 2 else add 0 3)

（isZero 1）がfalseであることはわかっています。したがって、上記の式を解くと、次のようになります。

(if **(isZero 1)** then 2 else add 0 3)
(if False then 2 else add 0 3)
add 0 3

これは、関数fに0を適用し、次に結果に3を適用するのと同じです。上記の式は次のように読み取ることができます。「f」は「f」に0が適用され、前のアプリケーションの結果に3が適用されます。

しかし、fは以前は次のように定義されていました。

(\f.\n.\m.if (isZero n) then m else f (pred n) (succ m))

したがって、この場合、次のようになります。

add = (\f.\n.\m.if (isZero n) then m else f (pred n) (succ m))

add 0 3 = \n.\m.if (isZero n) then m else add (pred n) (succ m)) 0 3
    = **\n**.\m.if (isZero **n**) then m else add (pred **n**) (succ m)) **0** 3
    = \m.if (isZero 0) then m else add (pred 0) (succ m)) 3
    = **\m**.if (isZero 0) then **m** else add (pred 0) (succ **m**)) **3**
    = if (isZero 0) then 3 else add (pred 0) (succ 3))
    = if **(isZero 0)** then 3 else add (pred 0) (succ 3))
    = if True then 3 else add (pred 0) (succ 3))
    = 3

構文ツリーでは、単純に展開を表示して、結果3に到達します。

アプリケーションプロセスのより簡単な例として、（\x。\yx + y）として定義される関数 "sum"を考慮すると、（sum 3 2）の結果は次のようになります。

(sum 3 2)
((sum 3) 2)
(((sum) 3) 2)
(((\x.\y.x + y) 3) 2)
((\y.3 + y) 2)
(3 + 2)
5

式を解く順序に制限はありません。ラムダ計算は、使用される削減の順序が何であれ、同じ結果をもたらすことが証明されています。 参考文献を参照してください。

Giorgioが指摘しているように、Yは固定小数点コンビネータであり、アプリケーションが同じ式に戻った場合に、特定の時点で反復を停止できます。

アプリケーションは有限の反復回数を必要とするため、解決策は同じであり、固定ポインターの組み合わせマークに注意するだけです。

Y = (\f.\n.\m.if (isZero n) then m else f (pred n) (succ m))
Y add = (\f.\n.\m.if (isZero n) then m else f (pred n) (succ m)) add
Y add = (**\f**.\n.\m.if (isZero n) then m else **f** (pred n) (succ m)) **add**
Y add = \n.\m.if (isZero n) then m else add (pred n) (succ m)

Y add 0 3 = \n.\m.if (isZero n) then m else add (pred n) (succ m)) 0 3
    = **\n**.\m.if (isZero **n**) then m else add (pred **n**) (succ m)) **0** 3
    = \m.if (isZero 0) then m else add (pred 0) (succ m)) 3
    = **\m**.if (isZero 0) then **m** else add (pred 0) (succ **m**)) **3**
    = if (isZero 0) then 3 else add (pred 0) (succ 3))
    = if **(isZero 0)** then 3 else add (pred 0) (succ 3))
    = if True then 3 else add (pred 0) (succ 3))
    = 3

不動点コンビネータへの参照。