Redexで評価コンテキストが必要なのはなぜですか？

Question

評価コンテキストを使用せずに自分の言語の評価ルールを書くことは完全に可能です。私のセマンティクスは完全に価値によって呼び出され、ラムダの中でその言葉が前進していくことを許さない。それにもかかわらず、私が見たすべてのリソースは、何らかの形で還元コンテキストを使用しています。私が紛失している文脈を使う良い理由はありますか？

Answer 1

短い答え：あなたはそうではありませんが、その方がずっと簡単です。

長い答え：評価コンテキストを使用することはほとんどありません。リレーションシップリレーションの異なるリダクションルールで自分自身を実行することができます。特に、言語の最小限のものをモデリングする場合は、非常に不快になります。

ここで、コールを値λ計算によってモデル化したいとします。 （評価コンテキストなしで）それのための言語は次のようになります。

(define-language Lv 
    (v (λ (x) e)) 
    (e v 
    (e e)) 
    (x variable-not-otherwise-mentioned) 
    #:binding-forms 
    (λ (x) e #:refers-to x)) 

（ここでは、最後の2行はを活用するために使用されている可約式のcapture avoiding substitution

今、することなく、この言語のためのセマンティクスを作ってみることができます。評価コンテキストを使用して、我々は部分式、演算子と関数適用のオペランドを拡張することができる2つの場所がありますので、通常のベータ削減が私たち与えていることを含む：。。

(define red 
    (reduction-relation 
    Lv 
    (--> (e_1 e_2) 
     (v_1 e_2) 
     (where v_1 ,(first (apply-reduction-relation red (term e_1))))) 
    (--> (v_1 e_2) 
     (v_1 v_2) 
     (where v_2 ,(first (apply-reduction-relation red (term e_2))))) 
    (--> ((λ (x) e) e_2) 
     (substitute e x e_2)))) 

をこれも悪くないです、しかし、サブ式を評価できる場所ごとにルールを追加する必要があります。したがって、独自の規則などが必要な場合は、独自の規則が必要になります。これは、これらの形式のそれぞれの規則の上にあることを忘れないでください。

これを実行する方がはるかに簡単ですが、評価コンテキストを使用するだけで、ステップを実行できるサブ式と実行順序を指定できます。Lv言語を次のように書き直してみましょう。評価コンテキスト：

(define-language Lv2 
    (v (λ (x) e)) 
    (e v 
    (e e)) 
    (x variable-not-otherwise-mentioned) 
    (E hole 
    (E e) 
    (v E)) 
    #:binding-forms 
    (λ (x) e #:refers-to x)) 

それは今、長い三行だが、これは我々が評価コンテキストで私たちの式を評価することでしょう可約式を伝え、E、及びその式を評価完了時には、（ここで、文脈にそれを置きますholeは話すトップレベルのコンテキストです）。したがって、私たちはただ一つのルール、ベータ削減に至るまで、当社の削減関係を減らすことができます：ここでは

(define red2 
    (reduction-relation 
    Lv2 
    (--> (in-hole E ((λ (x) e) e_2)) 
     (in-hole E (substitute e x e_2))))) 

我々は上記のようにE次のホールにあると言ってin-holeを使用しています。穴はアプリケーションの左から右にしか表示されないため、値のセマンティクスによる呼び出しが続きます。

多くのサブ式を含むはるかに大きな計算をすると、非常に大量の削減ルールを書くことができなくなることが想像できます。

したがって、要するに、モデルをずっと短くするだけです。