まず第一に、私はこれらのことや何かを勉強したことがないので、とてもばかげた質問をしているかもしれません.
私は必要に応じた評価でラムダ計算を実装して遊んでいます。関連するビットは、28ページで説明されている自然なセマンティクスのようです。
とにかく、この評価戦略について私が理解していないのは、私が理解している限り、実際の置換は変数を評価するときにのみ起こるということです。これらは値であるため、抽象化はそれ自体に評価され、アプリケーションは新しいエントリをキャッシュに追加するだけです。
しかし、それを考えると、次のような用語を正確に評価するにはどうすればよいですか
(λx.λy.x y) λa.a
リンクされた論文に記載されている自然なセマンティクスによれば、最初の評価ステップは、エントリx -> λa.aをキャッシュに追加し、アプリケーションの左辺で抽象化の本体を評価することですλy.x y。しかし、これは値なので、評価は終了します。その時点で、閉じていない項と空でないヒープがあります。この用語が に評価される必要があることは正確にわかっていますがλy.(λa.a) y。
私は何を誤解していますか？この評価戦略を実際に使用する言語では、これはどのように機能しますか?