トップページ⇒informatics
76コメント24KB

プログラム意味論

■ このスレッドは過去ログ倉庫に格納されています
0001名無しさん＠お腹いっぱい。2006/08/21(月) 02:43:29ID:9ON/vMbD0
操作的意味論、表示的意味論、公理的意味論、なんでもウェルカム。
教科書読んでて意味不明になったら、質問するのもいいね。
プログラムの理論をやるなら教養の部類に入る分野なんで、ガンバロー。

参考書リスト
(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/
0002名無しさん＠お腹いっぱい。2006/08/21(月) 05:07:17ID:T61q1iqZ0
これだから広島は
0003名無しさん＠お腹いっぱい。2006/08/21(月) 15:25:55ID:OBpgt44Y0
これって何する分野
0004名無しさん＠お腹いっぱい。2006/08/21(月) 17:01:24ID:ihiFOZ5Z0
>>3
プログラム意味論
0005名無しさん＠お腹いっぱい。2006/08/21(月) 23:51:59ID:OPfMty750
トートロジーはなにも語らない。
0006名無しさん＠お腹いっぱい。2006/08/22(火) 00:24:59ID:Oqth4tQD0
とりあえずwikipedia(ja)に項目が無いんですが、・・・
0007名無しさん＠お腹いっぱい。2006/08/22(火) 19:28:15ID:CUK16Hgr0
formal methodについてもここで語っておｋ？
0008名無しさん＠お腹いっぱい。2006/08/22(火) 19:54:46ID:df9avIV20
.
0009名無しさん＠お腹いっぱい。2006/08/23(水) 16:31:30ID:gEutl4VN0
意味論って型とか変数の有効範囲とかの研究だよね？
0010名無しさん＠お腹いっぱい。2006/08/23(水) 19:43:55ID:AVIF32Vp0
プログラムの意味を記述する方法論の研究でしょ？
0011名無しさん＠お腹いっぱい。2006/08/23(水) 21:36:19ID:KcM2nNux0
領域理論なら中島玲二(うろおぼえ)さんの本とかあったような
図書館ですら見た事ないけど
0012名無しさん＠お腹いっぱい。2006/08/24(木) 00:23:08ID:0vuDRuaJ0
>7
公理的意味論の範囲ならいいんでないかい。
でも、形式手法でもモデル検査とかはちょうんじゃないの。
0013名無しさん＠お腹いっぱい。2006/08/24(木) 19:37:25ID:iu69rIVY0
新板出来たのに誰もこないね
0014名無しさん＠お腹いっぱい。2006/08/26(土) 21:05:34ID:KFleSFe30
学生のとき習ったけどわからなかった。
プログラマだけど改めて勉強しようかと思っている。
Davey & Priestley「Introduction to Lattices and Order」っていう本もこの分野に関係あるよね。
0015名無しさん＠お腹いっぱい。2006/08/27(日) 01:23:08ID:U3zQgGbU0
>>14
関係あるんだけど、意味論関係では表示的意味論の道具立てに焦点を当てた本だね。
ドメインや不動点の話をきっちりやるのにはいいかも。
最近は操作的意味論が主流っぽいので、実用性を考えると回り道になる可能性もある。
0016名無しさん＠お腹いっぱい。2006/09/04(月) 16:39:53ID:fwVd6ZyO0
CやC++で書かれたプログラムの、厳密な意味を考えるために、
プログラム意味論を勉強することは役立ちますか？
0017名無しさん＠お腹いっぱい。2006/09/04(月) 18:58:14ID:nwOv6SXO0
「CやC++で書かれたプログラムの、厳密な意味」
ってなんなんだろう。
0018名無しさん＠お腹いっぱい。2006/09/04(月) 22:07:49ID:bvfKYMe50
その意味自体を定義するのが、また厄介だなぁ……
0019名無しさん＠お腹いっぱい。2006/09/04(月) 22:25:27ID:fwVd6ZyO0
ようはほとんど役立たないってことね
0020名無しさん＠お腹いっぱい。2006/09/04(月) 22:44:19ID:bvfKYMe50
というより、C/C++ は後付けで意味をどんどん変更できるから(；´Д｀)
0021名無しさん＠お腹いっぱい。2006/09/04(月) 23:14:54ID:QCif2R510
>>20どういうこと？
0022名無しさん＠お腹いっぱい。2006/09/04(月) 23:16:27ID:uo5hLqfS0
プログラム言語論で言うところの意味とプログラム意味論で言うところの意味をごっちゃにしてるだけ
0023φ(.. )2006/09/05(火) 14:04:03ID:UTvl3hn/O
ログイン名って何ですか
0024名無しさん＠お腹いっぱい。2006/10/06(金) 11:42:05ID:AXK5tR8H0
彼の場合は仕事自体よりも、ちょっとはみ出した人間が許せないのだろう。
一歩も引かない性格だし。今までもいろいろな職場でそういう人間関係の
もつれから辞職、またはクビになって流されてきたのだと思う。
そういう点でヘルパーを思い立ったのだろうが、残念ながら軌道には全く
乗っていないようだ。
そもそもヘルパー職自体も、やりたい事というより老人や身障者を介護している
ほうが、くだらん人間関係に振り回されることがないから選んだにすぎないと思う。
本当に生活できない現状なら、どこかと掛け持ちするか、もう少し収入源になることを
考えないと、将来はホームレスにも成りかねない。
0025名無しさん＠お腹いっぱい。2006/10/11(水) 11:21:14ID:HT1Qi2ZX0
領域理論スレが落ちたのでこっちで。
むこうで紹介されてた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はどうやって示せば良い？
0026名無しさん＠お腹いっぱい。2006/11/03(金) 18:58:44ID:0DkjYKix0
操作的意味論、表示的意味論、公理的意味論
それぞれの意味の違いって何なんですか？
0027名無しさん＠お腹いっぱい。2006/11/03(金) 19:03:58ID:Za/5Vww80
操作的意味論は計算手順を与える
表示的意味論は数学的対象への対応を与える
公理的意味論は規則により等しさを与える

かなあ
答えになってるかどうかわからんけど
0028名無しさん＠お腹いっぱい。2006/11/03(金) 19:47:14ID:0DkjYKix0
レスどうも。
ところで、領域理論に出てくる領域方程式というのは
いったい何を表しているのですか？解けるのかな？
0029名無しさん＠お腹いっぱい。2006/11/03(金) 21:15:20ID:Za/5Vww80
>>28
例えば型なしラムダ計算においては 値=関数 なので
ラムダ項全体を数学的な対象 D と考えようとすると
D から D への関数全体が D と同型になっていてほしくて、
D^D=D みたいなのが成り立たないかなーと思うわけだ。
こういうふうにして出てくる等式が領域方程式だ。
ちなみに D^D=D は集合の圏では解がないが、CPO の圏でなら解ける。

と思うけど、実はあんまりよく知らないんで間違ってたら突っ込んでください
0030名無しさん＠お腹いっぱい。2006/11/04(土) 07:13:49ID:op6LTC1y0
>>29
へー、ＤからＤへの関数全体がＤと同型になったりするんですか。
なかなか面白そうなので自分も勉強してみようと思っています。
いろいろありがとうございます。非常に参考になりました。
0031名無しさん＠お腹いっぱい。2006/11/04(土) 18:17:44ID:fAhkPK9Z0
ちょっと訂正

× 解がない
○ 自明な解しかない
0032名無しさん＠お腹いっぱい。2006/11/11(土) 22:25:04ID:WiVe2eyl0
なんの役にもたたんな。
大学は株式会社されるんだから、儲かる研究しなさい。
東大の教授はすでに年収６００万円から６０００万円まで広がってるぞ。
0033名無しさん＠お腹いっぱい。2006/11/11(土) 23:43:52ID:aoIBAFR20
抽象数学に対して無粋なことを言ってもダメ
0034名無しさん＠お腹いっぱい。2006/11/14(火) 13:32:29ID:gVqNCS4o0
プログラム意味論って数学や数理論理学をよく勉強してないとちゃんと理解することはできないんだね
0035名無しさん＠お腹いっぱい。2006/11/16(木) 13:44:23ID:ppOhpKAm0
女子高生・OL・素人の○○を全部見せます！
画像掲示板（エロ画像可）
http://katamichi.homeip.net/imgbbs/index.htm
0036名無しさん＠お腹いっぱい。2006/11/24(金) 01:35:45ID:34P2afeW0
>>34
数学の素養は意味論に限らず必須だね。
とはいえ、純粋数学の人間ほどには深入りしなくていいかな。
むしろ、深入りしすぎると時間ばっかりかかって何もできなかったりする。

意味論をやるにしても、教科書によっては必要な数学的素養が平行して身に付く
構成になってる本もあるよ。別に気合いを入れて集合、代数、数理論理の専門書を
精読しなくても、ある程度までは大丈夫ではないかと。
0037名無しさん＠お腹いっぱい。2006/11/28(火) 09:12:13ID:Hl6Nn6kQ0
　　　　　　 , 　----‐ 二二ﾆ 丶 、
　　　 　 ／ 　 　　／ _, ----ミｧ､ ＼
　　　 ／　　 / 　/‐'´　 　　　　　 ヾコ　　　　　　　　　　　　　　　　　　　　　　　　　　(ﾟдﾟ)ｼﾞｮﾊｰ
　　 / rー- / 　 l　j 　､ヽ　 ヽ 　　 ヽヽ＼　　　　　　 　　　　 　　　　　　　 　 　 　 　 　r‐､
　　,'　ヾ /7　,'　l .ﾊ`トﾑ､＼　 X.　 　|く　 l　　　　　　　　　　　　　　　　　　　　　　 　 　|　）
　 ,'　 　/L|　 |　lﾚ ,ィ≠ﾐヽ ` ' .ﾑヽ　 } |ヽ! 　　　　　　　　　　　　　　　　　　　　　 　　 /　|_____
　.! , 　//| l　 |　|　` ﾄ:::ﾘ 　　　 ﾋ:}l !丿 }ヽ＼　　　　　　　　　　　　　　　　　 　 　 　 , '　´　＿ﾉ
　|│ // | l　 |　|　　｀''"　　　 ,　´|　| |/ | | V　　　　　　　　　　　　　　 ,, --､＿__ ／ 　 　 --ｲ
　|│ Ｖ　| |　 |　|　　　　r― ‐, 　 } .| |　 Ｖ!　　　 　　　　　　　 _,　-‐''´　　 / ///　　 　　 ‐‐ｲ
　| .l 　　 Ll 　 !　| 　　　ヽ _ /　, ´| |│|ヽ ! 　　　　　, -─‐'"´　　　　　　　l　| | {　　 　　 　,ノ
　|　! 　　ｉ　! 　 !　ﾄ ､　 　 　 ／|　| ! ﾊl　ヾ 　 ＿ ／　　　　　　　 　 　　　│ ! | ヽ ,----‐'´
　|　ﾊ　　! | .!　 ｉ .|ゝ　 ￣/¨ , ┴ ､ﾘ_ﾆ--, -' 　／　　　　　　 　　 　 　 　 　ヽヾ丶ﾉ
　ﾚ' 　|　 l ! ﾊ　ﾉﾘ ＞≠==- ､ ／　　　／ 　　´　　　　　　　　　　　　　　　　 ﾌ￣
　　　 | 　/ﾚ　レ ／　　　 　／ 　　　　´　　　　　　　　　　　 　　　 ＿, -‐ '⌒
　　　 レ' | 　〃/|　　　 　　　　　　　　　　　　　　　　　　　　_, -'"
　　　　　│　|| | |　　　　 　 　 　 　 　 ---=≠------─'''´
　　　　　/　 .|| ! ヽ　　　　　　　 ,　-‐'ヾ￣
　　　 　 |　 〃 |　　ヽ 　　　 ／l　 　＼ ＼
0038sage2006/12/25(月) 23:22:55ID:WlutsqjQ0
>>36
その「教科書によっては必要な数学的素養が平行して身に付く 構成になってる本」が知りたいです。
0039名無しさん＠お腹いっぱい。2006/12/30(土) 22:03:21ID:vMgChu3M0
俺も知りたい
0040名無しさん＠お腹いっぱい。2006/12/30(土) 23:30:26ID:kn721qIE0
俺も俺も
0041名無しさん＠お腹いっぱい。2006/12/31(日) 10:04:22ID:juQL2oOhP
じゃあオレがやるよ !
0042名無しさん＠お腹いっぱい。2007/01/03(水) 16:52:10ID:TzNfjEkE0
これがあるじゃないか。
http://www.amazon.co.jp/Categories-Computer-Science-Cambridge-Texts/dp/0521419972
0043名無しさん＠お腹いっぱい。2007/01/20(土) 01:29:50ID:3LDLYWaD0
通読してはいないんだけど、
The Formal Semantics of Programming Languages - An Introduction
Glynn Winskel, MIT.
なんかはどうなんだろ。領域理論あたりまで読んだけど、親切な本だよ。
0044名無しさん＠お腹いっぱい。2007/02/02(金) 14:30:56ID:E0JXnBFwO
授業で
キーボードから３つの数値を入力して、平均値を計算して画面に表示する。
っていうプログラムを作れと言われたんですけど、誰か教えていただけませんか？お願いしますm(_._)m
0045名無しさん＠お腹いっぱい。2007/02/03(土) 01:52:32ID:70ceOPpy0
表示的意味論のいい教科書を紹介して欲しいんだけど、ある？
当方、連続関数やcpoなんかは一通り理解してるつもり。
0046名無しさん＠お腹いっぱい。2007/02/03(土) 13:41:18ID:zTPBuNAJ0
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

どの命令がどのような意味を持っているのか教えてください。
0047名無しさん＠お腹いっぱい。2007/03/14(水) 19:04:07ID:ds7xgK/t0
>>1
愛い奴だなぁ。
俺がもう何年も前に２ｃｈで教えてやった参考書を
未だに参考書リストに入れてるとは・・・

お前っていつになったら自力で勉強できるようになるの？
0048名無しさん＠お腹いっぱい。2007/03/14(水) 22:19:20ID:U+Zqa20O0
>>47
http://science6.2ch.net/test/read.cgi/informatics/1165506353/80
0049名無しさん＠お腹いっぱい。2007/03/14(水) 23:14:22ID:ds7xgK/t0
おまえってさぁ、もしかして２ちゃんの運用かなんかやってるクズ？
おまえとクズ議論して、いろんな知識を授けてやった事、
今じゃ後悔してるよ。

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

お前のようなクズは、最後の頼みの綱にも裏切られて惨めな死に方をするのがお似合いだ
0050名無しさん＠お腹いっぱい。2007/03/28(水) 22:07:32ID:MTB52o6f0
プログラム意味論って何の役に立つかおしえてくれ！
もうすでに終わった学問じゃないのか？
0051名無しさん＠お腹いっぱい。2007/03/29(木) 02:24:15ID:mYqjR1Q00
>>50
何を根拠に終わったと
0052名無しさん＠お腹いっぱい。2007/03/30(金) 16:46:33ID:lhJeQYvdO
どうかんがえたっておわってるだろ
自己完結しすぎ
0053名無しさん＠お腹いっぱい。2007/03/30(金) 17:29:16ID:gSKDG9by0
>>52
自己完結の何が悪いの？
0054名無しさん＠お腹いっぱい。2007/03/30(金) 20:17:01ID:kIS6WhR30
悪くはないが、発展はない、つまり、おわってるんだよ。
0055名無しさん＠お腹いっぱい。2007/03/31(土) 00:15:31ID:aVjqK6OM0
>>54
どういう意味で自己完結してるのか
0056名無しさん＠お腹いっぱい。2007/04/16(月) 05:25:50ID:hW2X57W3O
結局操作いがいは糞
0057名無しさん＠お腹いっぱい。2007/06/03(日) 22:05:41ID:M8r7WIcq0
ＳＯＳ ＳＯＳ ほらほら　呼んでいるわ ♪
0058名無しさん＠お腹いっぱい。2007/10/16(火) 15:54:57ID:zubr5owl0
意味論ってもはや本買って勉強する人すらいないの？
0059名無しさん＠お腹いっぱい。2007/11/08(木) 23:09:21ID:4vAL+msN0
うちは普通に輪講させられたけど、卒論とは何の関係もないな
0060電脳プリオン2007/12/30(日) 00:00:55ID:LhDmtenF0?2BP(1466)
関連スレが落ちとる。
0061名無しさん＠お腹いっぱい。2008/02/22(金) 00:55:13ID:7V3ZA782O
む、意味論か。
0062名無しさん＠お腹いっぱい。2008/03/10(月) 09:39:37ID:jwHET6d80
日本語のプログラム意味論の本は３冊しかなくて、今や本屋で買えるのは
１個だけ。これ豆知識ね（以下ｒｙ

「数理情報学入門」　中島玲二
「プログラム意味論」　横内寛文
「コンピュータサイエンス入門 ―論理とプログラム意味論 」　田辺誠
0063名無しさん＠お腹いっぱい。2008/03/27(木) 03:39:31ID:l7crpifn0
イマサラ　イミロン？　
シュウリョウ　
0064名無しさん＠お腹いっぱい。2008/07/15(火) 09:36:47ID:IEOW9KQb0
>>62
「プログラミング言語の意味論入門」 M.ヘネシー著 荒木啓二郎・程京徳 共訳
0065名無しさん＠お腹いっぱい。2009/02/18(水) 15:40:56ID:G+GAXaov0?PLT(13579)
ああ
0066名無しさん＠お腹いっぱい。2009/02/18(水) 15:42:27ID:G+GAXaov0?PLT(13579)
誤爆
0067首◇AiUeo2009/04/19(日) 06:47:59ID:oQScX42b0
a
0068名無しさん＠お腹いっぱい。2009/05/09(土) 03:49:41ID:dCrg2+CX0
意味の無い情報を意味の無いまま扱う系のプログラムって
あるでしょうか？
つまり非論理系ということです。
非ノイマン型で行う情報処理という話を調べています。
0069名無しさん＠お腹いっぱい。2009/05/09(土) 19:07:50ID:SwrwuETw0
情報の意味と、非ノイマン型であることと、全く関係がないと思うのだが。

ついでに言うとプログラム意味論とはなんの関係もないな。
0070名無しさん＠お腹いっぱい。2009/06/14(日) 23:59:38ID:m+cxVYEp0
どなたか、
「プログラミング言語の意味論入門」 M.ヘネシー著 荒木啓二郎・程京徳 共訳 の
4章の章末問題（115～117ページ）の、問10、11、12の解答を教えてはいただけないでしょうか？
古本でこの本を購入し読みつつ、問題も解いていっているのですが
周りに意味論について詳しい人が誰もいないので困っています。
0071名無しさん＠お腹いっぱい。2009/06/15(月) 04:59:15ID:ifHlBbmuO
>>70
とりあえず、問題を丸書き込みするんだ。
そしたら、頭のいい人が解いてくれるかもしれない。
0072名無しさん＠お腹いっぱい。2009/06/15(月) 16:41:59ID:cUx9rPGX0
>>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の型は
変わらなければならないことに注意せよ．
0073名無しさん＠お腹いっぱい。2009/06/19(金) 12:01:04ID:ep7y7w9QO
>>2->>5
0074名無しさん＠お腹いっぱい。2009/06/26(金) 05:51:58ID:PVuRGFSm0
1











http://gac.main.jp/numbers/index.html
0075名無しさん＠お腹いっぱい。2009/07/30(木) 06:52:10ID:FGKZk9q40
>>70
まだ見てんの？
ちょっと解答っぽいの書けそうなんだが。
0076名無しさん＠お腹いっぱい。2009/09/11(金) 06:49:36ID:A5S65loT0
意味論って外から囲うとすると破綻するよね。
破綻というか定型化してそれが意味論を阻害する。
■ このスレッドは過去ログ倉庫に格納されています