プログラム意味論

**名無しさん＠お腹いっぱい。** · 2006/08/21(月) 02:43:29

操作的意味論、表示的意味論、公理的意味論、なんでもウェルカム。
教科書読んでて意味不明になったら、質問するのもいいね。
プログラムの理論をやるなら教養の部類に入る分野なんで、ガンバロー。

参考書リスト
(1) 和書
(a) プログラム意味論横内寛文共立出版
(2) 洋書
(b) The Formal Semantics of Programming Languages : An Introduction,
Glynn Winskel, MIT Press.
(c) Semantics of Programming Languages : Structures and Techniques,
Carl A. Gunter, MIT Press.

他にも適切なものがあったら、追加をお願いします。

関連スレ
Domain Theory 領域理論
http://science4.2ch.net/test/read.cgi/informatics/1156004424/

**名無しさん＠お腹いっぱい。** · 2009/06/15(月) 16:41:59

>>71
書き込んでおきます。

問１０
x,y := e,e' のような並列代入命令を持つようにWhileL言語を拡張せよ．
この新しい構成要素に対して評価意味論を拡張せよ．
x,y := e,e' は必ずしも常にx := e ; y := e' と同じ振舞いをするわけではないことを
示す例を与えよ．

問１１
PASCALのcase命令を持つようにWhileL言語を拡張せよ．
ガード付きリストと呼ばれる新しい構文カテゴリ Guarded Listが必要であり，
その抽象構文は次のように与えられる．

G ::= n : C | n : C, G'

そして，新しい命令

case e of G end

が導入される．
直感的に，この命令の効果は，式eを数字に評価し，
この数字に対応してリストG中にある命令を実行することである．
この新しい構成要素に対して評価意味論を拡張せよ．
評価意味論にはガード付きリストのために
評価関係→Gを含むべきである．

問１２
式と論理式の抽象構文定義に次のような節を加えてWhileL言語を拡張せよ．

e ::= ... | Run C Then e | ...
be ::= ... | Run C Then be | ...

直観的に，記憶sにおいて文Run C Then eを評価するとき，
まずsにおいて命令Cを評価し，そしてその結果を反映した記憶において
eを評価する．この言語に新しい操作意味論を与えよ．
式の評価が記憶に影響を与えるようになるので，→Aおよび→Bの型は
変わらなければならないことに注意せよ．

**名無しさん＠お腹いっぱい。** · 2009/06/19(金) 12:01:04

>>2->>5

**名無しさん＠お腹いっぱい。** · 2009/06/26(金) 05:51:58

1

http://gac.main.jp/numbers/index.html

**名無しさん＠お腹いっぱい。** · 2009/07/30(木) 06:52:10

>>70
まだ見てんの？
ちょっと解答っぽいの書けそうなんだが。

**名無しさん＠お腹いっぱい。** · 2009/09/11(金) 06:49:36

意味論って外から囲うとすると破綻するよね。
破綻というか定型化してそれが意味論を阻害する。