プログラム意味論

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

参考書リスト
(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/

これだから広島は

これって何する分野

>>3
プログラム意味論

トートロジーはなにも語らない。

とりあえずwikipedia(ja)に項目が無いんですが、・・・

formal methodについてもここで語っておｋ？

.

意味論って型とか変数の有効範囲とかの研究だよね？

プログラムの意味を記述する方法論の研究でしょ？

領域理論なら中島玲二(うろおぼえ)さんの本とかあったような
図書館ですら見た事ないけど

>7
公理的意味論の範囲ならいいんでないかい。
でも、形式手法でもモデル検査とかはちょうんじゃないの。

新板出来たのに誰もこないね

学生のとき習ったけどわからなかった。
プログラマだけど改めて勉強しようかと思っている。
Davey & Priestley「Introduction to Lattices and Order」っていう本もこの分野に関係あるよね。

>>14
関係あるんだけど、意味論関係では表示的意味論の道具立てに焦点を当てた本だね。
ドメインや不動点の話をきっちりやるのにはいいかも。
最近は操作的意味論が主流っぽいので、実用性を考えると回り道になる可能性もある。

CやC++で書かれたプログラムの、厳密な意味を考えるために、
プログラム意味論を勉強することは役立ちますか？

「CやC++で書かれたプログラムの、厳密な意味」
ってなんなんだろう。

その意味自体を定義するのが、また厄介だなぁ……

ようはほとんど役立たないってことね

というより、C/C++ は後付けで意味をどんどん変更できるから(；´Д｀)

>>20どういうこと？

プログラム言語論で言うところの意味とプログラム意味論で言うところの意味をごっちゃにしてるだけ

ログイン名って何ですか

彼の場合は仕事自体よりも、ちょっとはみ出した人間が許せないのだろう。
一歩も引かない性格だし。今までもいろいろな職場でそういう人間関係の
もつれから辞職、またはクビになって流されてきたのだと思う。
そういう点でヘルパーを思い立ったのだろうが、残念ながら軌道には全く
乗っていないようだ。
そもそもヘルパー職自体も、やりたい事というより老人や身障者を介護している
ほうが、くだらん人間関係に振り回されることがないから選んだにすぎないと思う。
本当に生活できない現状なら、どこかと掛け持ちするか、もう少し収入源になることを
考えないと、将来はホームレスにも成りかねない。

領域理論スレが落ちたのでこっちで。
むこうで紹介されてたS. Abramsky, A. Jung: Domain theoryを読んでるんだが、

Proposition 2.2.10
Dが基底Bを持つcontinuous domainで、x, yがDの要素のとき、以下の三つはすべて同値である
1. x ≦ y　（本当は四角の不等号）
2. B[x] ⊆ B[y]
3. B[x] ⊆ ↓y

で、2から1、3から1はどうやって示せば良い？

操作的意味論、表示的意味論、公理的意味論
それぞれの意味の違いって何なんですか？

操作的意味論は計算手順を与える
表示的意味論は数学的対象への対応を与える
公理的意味論は規則により等しさを与える

かなあ
答えになってるかどうかわからんけど

レスどうも。
ところで、領域理論に出てくる領域方程式というのは
いったい何を表しているのですか？解けるのかな？

>>28
例えば型なしラムダ計算においては 値=関数 なので
ラムダ項全体を数学的な対象 D と考えようとすると
D から D への関数全体が D と同型になっていてほしくて、
D^D=D みたいなのが成り立たないかなーと思うわけだ。
こういうふうにして出てくる等式が領域方程式だ。
ちなみに D^D=D は集合の圏では解がないが、CPO の圏でなら解ける。

と思うけど、実はあんまりよく知らないんで間違ってたら突っ込んでください

>>29
へー、ＤからＤへの関数全体がＤと同型になったりするんですか。
なかなか面白そうなので自分も勉強してみようと思っています。
いろいろありがとうございます。非常に参考になりました。

ちょっと訂正

× 解がない
○ 自明な解しかない

なんの役にもたたんな。
大学は株式会社されるんだから、儲かる研究しなさい。
東大の教授はすでに年収６００万円から６０００万円まで広がってるぞ。

抽象数学に対して無粋なことを言ってもダメ

プログラム意味論って数学や数理論理学をよく勉強してないとちゃんと理解することはできないんだね

女子高生・OL・素人の○○を全部見せます！
画像掲示板（エロ画像可）
http://katamichi.homeip.net/imgbbs/index.htm

>>34
数学の素養は意味論に限らず必須だね。
とはいえ、純粋数学の人間ほどには深入りしなくていいかな。
むしろ、深入りしすぎると時間ばっかりかかって何もできなかったりする。

意味論をやるにしても、教科書によっては必要な数学的素養が平行して身に付く
構成になってる本もあるよ。別に気合いを入れて集合、代数、数理論理の専門書を
精読しなくても、ある程度までは大丈夫ではないかと。

　　　　　　 , 　----‐ 二二ﾆ 丶 、
　　　 　 ／ 　 　　／ _, ----ミｧ､ ＼
　　　 ／　　 / 　/‐'´　 　　　　　 ヾコ　　　　　　　　　　　　　　　　　　　　　　　　　　(ﾟдﾟ)ｼﾞｮﾊｰ
　　 / rー- / 　 l　j 　､ヽ　 ヽ 　　 ヽヽ＼　　　　　　 　　　　 　　　　　　　 　 　 　 　 　r‐､
　　,'　ヾ /7　,'　l .ﾊ`トﾑ､＼　 X.　 　|く　 l　　　　　　　　　　　　　　　　　　　　　　 　 　|　）
　 ,'　 　/L|　 |　lﾚ ,ィ≠ﾐヽ ` ' .ﾑヽ　 } |ヽ! 　　　　　　　　　　　　　　　　　　　　　 　　 /　|_____
　.! , 　//| l　 |　|　` ﾄ:::ﾘ 　　　 ﾋ:}l !丿 }ヽ＼　　　　　　　　　　　　　　　　　 　 　 　 , '　´　＿ﾉ
　|│ // | l　 |　|　　｀''"　　　 ,　´|　| |/ | | V　　　　　　　　　　　　　　 ,, --､＿__ ／ 　 　 --ｲ
　|│ Ｖ　| |　 |　|　　　　r― ‐, 　 } .| |　 Ｖ!　　　 　　　　　　　 _,　-‐''´　　 / ///　　 　　 ‐‐ｲ
　| .l 　　 Ll 　 !　| 　　　ヽ _ /　, ´| |│|ヽ ! 　　　　　, -─‐'"´　　　　　　　l　| | {　　 　　 　,ノ
　|　! 　　ｉ　! 　 !　ﾄ ､　 　 　 ／|　| ! ﾊl　ヾ 　 ＿ ／　　　　　　　 　 　　　│ ! | ヽ ,----‐'´
　|　ﾊ　　! | .!　 ｉ .|ゝ　 ￣/¨ , ┴ ､ﾘ_ﾆ--, -' 　／　　　　　　 　　 　 　 　 　ヽヾ丶ﾉ
　ﾚ' 　|　 l ! ﾊ　ﾉﾘ ＞≠==- ､ ／　　　／ 　　´　　　　　　　　　　　　　　　　 ﾌ￣
　　　 | 　/ﾚ　レ ／　　　 　／ 　　　　´　　　　　　　　　　　 　　　 ＿, -‐ '⌒
　　　 レ' | 　〃/|　　　 　　　　　　　　　　　　　　　　　　　　_, -'"
　　　　　│　|| | |　　　　 　 　 　 　 　 ---=≠------─'''´
　　　　　/　 .|| ! ヽ　　　　　　　 ,　-‐'ヾ￣
　　　 　 |　 〃 |　　ヽ 　　　 ／l　 　＼ ＼

>>36
その「教科書によっては必要な数学的素養が平行して身に付く 構成になってる本」が知りたいです。

俺も知りたい

俺も俺も

じゃあオレがやるよ !

これがあるじゃないか。
http://www.amazon.co.jp/Categories-Computer-Science-Cambridge-Texts/dp/0521419972

通読してはいないんだけど、
The Formal Semantics of Programming Languages - An Introduction
Glynn Winskel, MIT.
なんかはどうなんだろ。領域理論あたりまで読んだけど、親切な本だよ。

授業で
キーボードから３つの数値を入力して、平均値を計算して画面に表示する。
っていうプログラムを作れと言われたんですけど、誰か教えていただけませんか？お願いしますm(_._)m

表示的意味論のいい教科書を紹介して欲しいんだけど、ある？
当方、連続関数やcpoなんかは一通り理解してるつもり。

BASIC言語のスロットのプログラムなんですけど、

10CLEAR :CLS
20DIM A(2),B(2)
30FOR J=0 TO 2
40A(J)= RND 6-1
50NEXT
60*MAIN
70LOCATE 0,0
80FOR J=0 TO 2
90IF B(J)=0 LET A(J)=(A(J)+1) MOD 6
100PRINT MID$ ("$*＼7+&",A(J)+1,1);
110NEXT
120C= ASC INKEY$ -49
130IF C>-1 AND C<3 IF B(C)=0 LET D=D+1,B(C)=1
140IF D<3 GOTO *MAIN
150IF A(0)=A(1) AND A(1)=A(2) PRINT " GOOD"
160CALL 48381
170GOTO 10

どの命令がどのような意味を持っているのか教えてください。

>>1
愛い奴だなぁ。
俺がもう何年も前に２ｃｈで教えてやった参考書を
未だに参考書リストに入れてるとは・・・

お前っていつになったら自力で勉強できるようになるの？

>>47
http://science6.2ch.net/test/read.cgi/informatics/1165506353/80

おまえってさぁ、もしかして２ちゃんの運用かなんかやってるクズ？
おまえとクズ議論して、いろんな知識を授けてやった事、
今じゃ後悔してるよ。

おまえみたいなバカでも粘着力だけはバカみたいにずば抜けてるから
参考書教えたり、新しい知識を教えたり、最新の情報を知らせて
教育してやれば、ちょっとはまともな人間に生まれ変わる事を期待していた。
それが何？おまえは人に教えてもらった参考書をさも読破したかのように
Amazonでレビューしたり、2chでもったいぶってひけらかすだけで、
頭の中身は相変わらず空っぽときたもんだ。

お前のようなクズは、最後の頼みの綱にも裏切られて惨めな死に方をするのがお似合いだ

プログラム意味論って何の役に立つかおしえてくれ！
もうすでに終わった学問じゃないのか？

>>50
何を根拠に終わったと

どうかんがえたっておわってるだろ
自己完結しすぎ

>>52
自己完結の何が悪いの？

悪くはないが、発展はない、つまり、おわってるんだよ。

>>54
どういう意味で自己完結してるのか

結局操作いがいは糞

ＳＯＳ ＳＯＳ ほらほら　呼んでいるわ ♪

意味論ってもはや本買って勉強する人すらいないの？

うちは普通に輪講させられたけど、卒論とは何の関係もないな

関連スレが落ちとる。

む、意味論か。

日本語のプログラム意味論の本は３冊しかなくて、今や本屋で買えるのは
１個だけ。これ豆知識ね（以下ｒｙ

「数理情報学入門」　中島玲二
「プログラム意味論」　横内寛文
「コンピュータサイエンス入門 ―論理とプログラム意味論 」　田辺誠

イマサラ　イミロン？　
シュウリョウ　

>>62
「プログラミング言語の意味論入門」 M.ヘネシー著 荒木啓二郎・程京徳 共訳

ああ

誤爆

a

意味の無い情報を意味の無いまま扱う系のプログラムって
あるでしょうか？
つまり非論理系ということです。
非ノイマン型で行う情報処理という話を調べています。

情報の意味と、非ノイマン型であることと、全く関係がないと思うのだが。

ついでに言うとプログラム意味論とはなんの関係もないな。

どなたか、
「プログラミング言語の意味論入門」 M.ヘネシー著 荒木啓二郎・程京徳 共訳 の
4章の章末問題（115〜117ページ）の、問10、11、12の解答を教えてはいただけないでしょうか？
古本でこの本を購入し読みつつ、問題も解いていっているのですが
周りに意味論について詳しい人が誰もいないので困っています。

>>70
とりあえず、問題を丸書き込みするんだ。
そしたら、頭のいい人が解いてくれるかもしれない。

>>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の型は
変わらなければならないことに注意せよ．

>>2->>5

1











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

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

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