私は型とプログラミング言語を使って作業しています。Pierceは、値削減戦略による呼び出しについて、用語の例を示していid (id (λz. id z))ます。内側のリデックスid (λz. id z)は最初に減少し、最初の減少の結果として、外側のリデックスが通常の形式に減少する前にλz. id z与えられます。id (λz. id z)λz. id z
ただし、値による呼び出しの順序は、「最も外側のレデックスのみが削減される」、「レデックスは、右側がすでに値に削減されている場合にのみ削減される」と定義されています。この例id (λz. id z)では、最も外側のredexの右側に表示され、縮小されています。これは、最も外側のレデックスのみが削減されるというルールとどのように二乗されますか？
「最も外側」と「最も内側」という答えは、ラムダ抽象化のみを指しているのでしょうか。したがって、の項についてtはλz. t、t減らすことはできませんが、redexs tでは、可能であればt値に減らしてから、減らしますか？vs v
簡単な答え：はい。ラムダタームの内側で減らすことはできません。右から始めて、外側のタームだけを減らすことができます。
値によるラムダ計算の評価コンテキストのセットは、次のように定義されます。
E = [ ] | (λ.t)E | Et
Eはあなたが評価できるものです。
たとえば、名前によるラムダ計算では、評価コンテキストは次のとおりです。
E = [ ] | Et | fE
用語が値でなくても、アプリケーションを減らすことができるためです。たとえば(λx.x)(z λx.x)、値による呼び出しでスタックしますが、名前による呼び出し(z λx.x)では、通常の形式であるに減少します。
コンテキストでは、文法fは次のように定義される通常の形式（名前で呼び出す）です。
f = λx.t | L
L = x | L f
コンテキストの別の定義は、Pierceの19.5.3章で確認できます。
「最も外側」と「最も内側」という答えは、ラムダ抽象化のみを指しているのでしょうか。したがって、λzの項tについて。t、tを減らすことはできませんが、redex stでは、可能であればtを値vに減らしてから、svを減らしますか？
はい、その通りです。