1

ラムダ計算について読んでいます。セクション 2.1 の最後からhttp://www.toves.org/books/lambda/ :

(λx.(λx.λy.x × y) 3 ((λz.x + z) 2)) 1   ⇒   (λx.λy.x × y) 3 ((λz.x + z) 2)   where x = 1
⇒   (λy.x × y) ((λz.x + z) 2)   where x = 3
⇒   x × y   where x = 3 and y = (λz.x + z) 2
⇒   x × y   where x = 3 and y = x + z and z = 2
⇒   x × y   where x = 3 and y = 5 and z = 2
⇒   15

それは言う

ただし、実際には、y は 5 ではなく 3 の値を取得する必要があります。これは、最初のベータ還元で 1 が式の x の位置に差し込まれるためです。このため、遅延パラメーターは、各リダクションで現在の変数コンテキストを保持する必要があります。この場合、式 λy.x × y 内では x = 3 ですが、式の外では x = 1 であるという事実を維持します。

しかし、ベータ削減中の操作の順序について混乱しています。残念ながら、説明があいまいです。x は (λx.λy.x × y) 内で 1 である必要があり、次に y = 3 を渡す必要があることを意味する可能性があります。これは、次に渡されるパラメーターであり、x が既に設定されている (間違っていると感じます)、または以下のルートに進むことを意味します。 :

(λx.(λx.λy.x × y) 3 ((λz.x + z) 2)) 1
は (λx.(λt.λy.t × y) 3 ((λz. x + z) 2)) 1

x はここで境界ですか? 1でいいんじゃない？

つまり、これを減らすと、 (λt.λy.t × y) 3 ((λz.1 + z) 2)) x = 1 (λy.3 × y) ((λz.1 + z) 2)) x = 1、t = 3 3 × ((λz.1 + z) 2)) x = 1、t = 3、y = ((λz.1 + z) 2)) 3 × ((λz.1 + z) 2)) x = 1、t = 3、y = ((λz.1 + z) 2))、z = 2 3 × (1 + 2) x = 1、t = 3、y = ((λz.1 + z) 2)), z = 2 3 x 3 = 9

あれは正しいですか？それとも、間違って減らしましたか？

4

2 に答える 2

2

式では

(λx.(λx.λy.x × y) 3 ((λz.x + z) 2)) 1

あなたが正しく書き直したもの

(λx.(λt.λy.t × y) 3 ((λz.x + z) 2)) 1

x変数は外側のラムダ抽象化に結合されますλx。実際、用語の削減によって用語が変更
される可能性はありません。これは、redex ツリーの別のブランチにあるためです。(λx.λy.x × y) 3(λz.x + z)

この本は、15 が間違った結果であることを明確に述べています。

与えられた例は、 Lazy 評価が単純に実装された場合に何が起こるかの反例です。

遅延評価は理論的には通常の順序で実現されますが、これは理論上の構築にすぎず、実際にはいくつかの欠点があります。そのため、 call-by-need
などの戦略が代わりに使用されます。

この本は、前述の評価戦略の可能な、抽象的な実装を示したかっただけです。

参考までに、式の通常の順序を使用した完全な削減をここに示します。

(\x.(\x.\y.x * y) 3 ((\z.x + z) 2)) 1


          ()
         /  \
       \x    1
        | 
       ()
      /   \
    ()     ()
   /  \   /  \
 \x    3 \z   2
  |       |
 \y       +
  |      x z
  *
 x y



---------------------------------------

(\x.\y.x * y) 3 ((\z.1 + z) 2)


       ()
      /   \
    ()     ()
   /  \   /  \
 \x    3 \z   2
  |       |
 \y       +
  |      1 z
  *
 x y


---------------------------------------


\y.3 * y ((\z.1 + z) 2)


       ()
      /   \
    .'     ()
   /      /  \
 \y      \z   2
  |       |
  *       +
 3 y     1 z

---------------------------------------


3 * ((\z.1 + z) 2)


     *
   /  \
  3   ()
     /  \
    \z   2
     |
     +
    1 z


---------------------------------------


3 * (1 + 2)


     *
   /  \
  3   1 + 2

---------------------------------------

3 * 3

  *
 / \
3   3

---------------------------------------

9
于 2016-08-21T09:24:14.020 に答える