R6RS:翻訳:R6RS:A Formal semantics

R6RS:翻訳:R6RS:A Formal semantics

付録 A 形式的意味論

本付録では、以前提案された意味論 [18] にもとづいた、非規範的で、形式的な Scheme の操作的意味論を与える。これは言語全体を網羅するものではない。欠けている機能として主なものはマクロシステム、入出力、数値の階層である。本意味論に含まれている機能の精確なリストは R6RS:翻訳:R6RS:A2 Grammar に与えられている。

本仕様の本体は(抽象)機械がいかに振る舞うか示す一段階の項書き換え関係である。一般に、本報告書は完全な仕様ではなく、実装系に異なる振る舞いをする自由を与え、典型的には最適化を行なうことを認めている。この未規定部分は意味論中でふたつの方法で示される。

ひとつには「unknown: 文字列」状態に還元される還元規則である(ここで、文字列は未知の状態についての説明を与える)。この強みは、そのような状態に還元される規則は任意の還元規則に置き換えられることである。それらの規則の置き換え型の精確な仕様は R6RS:翻訳:R6RS:A12 Underspecification? に与えられている。

もうひとつには、一段階の関係はプログラムひとつを複数の異なるプログラムに対応づけ、それぞれが抽象機械のとりうる適当な遷移になる。そのため、我々は一段階の関係の推移閉包 →* を意味論 [image] プログラム ([image]) から観測可能な結果 ([image]) への関数としてを定義するのに用いる。

 [image] : [image] → 2[image]
 [image]([image]) = { [image]([image]) | [image] →* [image] }

ここで、[image] は意味論から答 [image] を観測可能な結果に変更する。大雑把に言えば、 [image] は単純な基底値における恒等関数であり、手続きや対のような、より複雑な値には特別なタグを返す。

したがって、それぞれのプログラム [image] について、実装系が [image]([image]) の結果のひとつを生成すれば、実装系は意味論に合致しているか、もしくは実装系が無限ループに陥った場合、 [image] に始まる無限の還元列があり、還元関係 → は unknown: 状態に置き換えられるよう仮定される。

[image][image][image][image] の精確な定義もまた R6RS:翻訳:R6RS:A2 Grammar で与えられる。

この意味論とその振る舞いを理解することを助けるため、我々はこれを PLT Redex で実装した。この実装は本報告書の Web サイト http://www.r6rs.org/ から手に入れられる。本意味論中の還元規則やメタ関数はすべてこのソースコードから自動生成された。

  1. R6RS:翻訳:R6RS:A1 Background
  2. R6RS:翻訳:R6RS:A2 Grammar
  3. R6RS:翻訳:R6RS:A3 Quote
  4. R6RS:翻訳:R6RS:A4 Multiple values?
  5. R6RS:翻訳:R6RS:A5 Exceptions?
  6. R6RS:翻訳:R6RS:A6 Arithmetic and basic forms?
  7. R6RS:翻訳:R6RS:A7 Lists?
  8. R6RS:翻訳:R6RS:A8 Eqv
  9. R6RS:翻訳:R6RS:A9 Procedures and application?
  10. R6RS:翻訳:R6RS:A10 Call/cc and dynamic wind?
  11. R6RS:翻訳:R6RS:A11 Letrec?
  12. R6RS:翻訳:R6RS:A12 Underspecification?
More ...