R6RS:翻訳:R6RS:A3 Quote

R6RS:翻訳:R6RS:A3 Quote

A.3 quote

(store (sf₁ …) S₁['sqv₁])→                           [6sqv]
(store (sf₁ …) S₁[sqv₁])

(store (sf₁ …) S₁['()]) →                           [6eseq]
(store (sf₁ …) S₁[null])

(store (sf₁ …) S₁['seq₁])→                         [6qcons]
(store (sf₁ …) ((lambda(qp) S₁[qp]) 𝔔ᵢ⟦seq₁⟧))  (qp fresh)

(store (sf₁ …) S₁['seq₁])→                        [6qconsi]
(store (sf₁ …) ((lambda(qp) S₁[qp]) 𝔔ₘ⟦seq₁⟧))  (qp fresh)

図 3: quote

任意のプログラムに最初に適用される還元規則は図 3 の quote された式を取り除く規則である。最初のふたつの規則は対を導入しない quote された式の quote を取り除く。最後のふたつの規則は quote されたデータを式のいちばん上まで昇格させ一度だけ評価されるようにし、メタ関数 [image]_i と [image]_m を経由して、 cons か consi の一方が呼び出されるようにする。

[6qcons] と [6qconsi] の規則の左辺が同一であることに注意。これは一方の規則が項に適用されたら、もう一方も適用されることを意味している。したがって、 quote された式は cons 式の列の外に取り出され、変更可能な対を作成するか、 consi 式の列の中に取り出され、変更不可能な対を作り出すかする(その起こり方の規則については R6RS:翻訳:R6RS:A7 Lists? を参照)。

これらの規則は、この規則やその他のすべての規則を適用する文脈があるため他のすべての規則よりも先に適用される。特にこれらの規則は文脈 S で適用される。図 2 は、文脈 S 内で、左の部分式に quote された式がなく、右側に quote された式はある場合にかぎり、 e の任意の部分式にこの還元規則を適用してもよいことを示している。したがって、この規則がプログラム中の quote された式それぞれに一回適用され、プログラムの始まりの外側に移動する。残りの規則は quote された式をまったく含まない文脈で適用され、これらの規則が、他の規則が適用される前にすべての quote されたデータをリストに変換することを保証している。

識別子 qp には下付き文字がないが、 PLT Redex の「fresh」宣言は規則の右辺にある qp は実際には周辺条件にあるものと実際には同一であると保証するよう、特別な扱いをする。


Last modified : 2016/08/28 06:15:28 UTC