R6RS:翻訳:R6RS:A1 Background

R6RS:翻訳:R6RS:A1 Background

A.1 背景

我々は読者が文脈依存還元意味論について基本的な馴染みがあることを仮定している。このシステムに馴染みのない読者は Filleisen と Flatt のモノグラフ [10] や Wright と Felleisen [29] によるものを、関連する技術的な背景も含む完全な入門や、 PLT Redex [19] へのやや優しい手引きとして参照することが望ましいかもしれない。

大雑把な説明として、我々は言語の操作的意味論をプログラムの項を経由して定義する。このとき、関係は抽象機械の一段階に対応する。関係は評価文脈、すなわち、と呼ばれる文脈の中で区別される場所、次の段階の評価の起こる場所によって定義される。我々は、 eE と同一であり、 e′ と置き換えられる穴である場合、項 e は評価文脈 E と別の項 e′ に分解されると言う。 E 中の穴を e′ で置き換えられることによって得られる項を示すのに E[e′] と書く。

例えば、非終端記号として文脈(E)、式(e)、変数(x)、値(v)を含む文法が定義されている場合、 β_v 書き換え規則を(→ の一段階の関係の一部として)定義する場合次のように書く。

[image]

規則の適用を制約するために、書き換え規則中で非終端記号の名前を(時には下付き文字を付けて)使った。つまり、項の内部の対応する位置で、その文法によって生成されたある項が現れた場合にだけ適用される。同一の終端記号が同一の下付き文字とともに複数回現れた場合、その規則だけが対応する項が構造的に同一である場合に適用される(下付き文字のない非終端記号は互いに照合するときに制約を受けない)。したがって、上の規則で右辺と左辺の両方に現れる E_1 は、この規則をつかったときにこの適用式の文脈は変化しないことを意味している。省略記号はクリーネ閉包の一種であり、省略記号のついたパターンに一致した項の 0 個以上の出現が、省略記号とその前にあるパターンの場所に現れることを意味している。我々は補足を避ける置き換えのために { x1 ... ↦ v1 } e1 という記法を用いる。この場合 e1 中で各 x1 は対応する v1 に置き換えられる。最後に、我々は周辺条件を規則の脇の括弧の中に書く。上の規則の周辺条件は x1 の個数と v1 の個数は同一でなければならないことを示している。我々は周辺条件のなかで等価性を使うこともある。その場合は、単純に項の等価性、すなわち、ふたつの項が同一の構文上の形状をしていなければならないということを意味している。

評価文脈 E を規則中に明示することで、我々は文脈を操作する関係を定義できるようになった。簡単な例で言えば、手続きに誤った個数の引き数が適用された場合、規則の右辺の評価文脈を破棄して、違反を通知するような規則を別に追加することができるのである。

[image]

後に、我々は評価文脈の明示をより洗練された方法で利用する。


Last modified : 2008/04/13 12:38:36 UTC