コール別の評価を誤解していますか？

Question

まず、私はこれらのことを何も学んだことがないので、申し訳ありませんが、私は非常にばかげた質問をしているかもしれませんが、私に簡単に行ってください:)

私はラムダ計算必要に応じた評価を行います。私は、関連するビットが28ページに記載されている自然なセマンティクスであると思われる件名のthis paperに従おうとしています。

とにかく、私がこの評価戦略について理解していないことは、実際の置換は変数を評価するときにのみ起こります。抽象化は値であるため、それ自身を評価し、アプリケーションはキャッシュに新しいエントリを追加するだけです。

しかし、リンク論文に記載自然意味論によると、最初の評価ステップは、エントリーへx -> λa.aを追加することですどのように正確に一度

(λx.λy.x y) λa.a

のような用語を評価について、与えられたことをキャッシュを作成し、アプリケーションのlhsにある抽象の本体を評価します。これはλy.x yです。しかしこれは価値なので、評価は終了します。どの時点で閉じられていない用語と空でないヒープがあります。この用語がλy.(λa.a) yと評価されることは正確に分かりますが。

私は何を誤解していますか？この評価戦略を実際に使用する言語では、どのように機能しますか？

Answer 1

あなたの削減は正しいです。要点は、このペーパーで取り上げられた必要性戦略によるコールは、ラムダ式の下で決して減少しないという意味で弱い戦略に過ぎないということです。これは図1で明白です。式\ x.Mは値です。

ラムダ項を明示的に取得したい場合は、キャッシュ内のキャッシュ内の関連付けをターム内で代用する必要があります。

   λy.x y [x -> λa.a] = λy.(λa.a) y 

期待どおりです。