- 1 名前：デフォルトの名無しさん mailto:sage [05/01/19 19:06:04 ]
- プログラミング言語処理系の開発に興味のある人達のスレッドです。
字句解析・構文解析から，データフロー解析，ループ並列化，タスク並列化，SSA変換，
CPS変換，レジスタ割付，命令スケジューリング，ソフトウェアパイプライン等各種最適化，
それにVM，GC，JIT，リンク時最適化，動的バイナリ変換などなど。
意味論に関する話題も歓迎です。
前スレ
1 pc.2ch.net/tech/kako/981/981672957.html
2 pc2.2ch.net/test/read.cgi/tech/1021136715/ (dat落ち)
3 pc5.2ch.net/test/read.cgi/tech/1070089173/
4 pc5.2ch.net/test/read.cgi/tech/1100097050/ (前スレ)
関連リンクは多分 >>2-10 あたり
- 91 名前：デフォルトの名無しさん mailto:sage [05/01/20 21:38:06 ]
- Cの文はCの規格が主張する文。
Cの式はCの規格が主張する式。
Cの関数はCの規格が主張する関数。
数学用語は借り物だし、日本語訳の言葉の定義は規格による。
これが現実だな。
- 92 名前：デフォルトの名無しさん mailto:sage [05/01/20 21:38:45 ]
- >>82はともかくとして、>>83は何か話がずれてる。
- 93 名前：デフォルトの名無しさん mailto:sage [05/01/20 21:40:29 ]
- >>86と>>91が結局正しい答えだな。
- 94 名前：デフォルトの名無しさん mailto:sage [05/01/20 21:44:13 ]
- >>83
話がずれてるが、ちょっと突っ込むと、BNFで定義してるのは、構文規則であって
意味じゃない。
意味を定義するには普通は人間の言葉を使う（意味論などを使うこともある）。
- 95 名前：デフォルトの名無しさん mailto:sage [05/01/20 21:45:50 ]
- Ruby厨だからどうしても斜めにずれるの >>92
- 96 名前：デフォルトの名無しさん mailto:sage [05/01/20 21:48:21 ]
- >>86は>>87の煽りだろ・・イイのか(w？
- 97 名前：デフォルトの名無しさん mailto:sage [05/01/20 21:53:57 ]
- 意味を定義するには普通は人間の言葉を使う
↑
自然言語の話かよ
- 98 名前：デフォルトの名無しさん mailto:sage [05/01/20 21:54:50 ]
- 文や式は一段落がついたので、次は関数の定義でお願いします。
- 99 名前：デフォルトの名無しさん mailto:sage [05/01/20 21:55:41 ]
- >>96
はぁ？
- 100 名前：デフォルトの名無しさん [05/01/20 21:56:06 ]
- >>91
なるほど、関数も考えるとその通りだね。（数学or一般的な関数とは明らかに
意味が違う。）
- 101 名前：デフォルトの名無しさん mailto:sage [05/01/20 21:56:41 ]
- 式＝Expression は和声英語?
- 102 名前：デフォルトの名無しさん mailto:sage [05/01/20 21:59:48 ]
- >>98
関数=プログラム
- 103 名前：デフォルトの名無しさん mailto:sage [05/01/20 22:01:22 ]
- お前らのスレでは情報数学の用語は借り物でｲｲのか（ｗ？
カッコいい言語出来そうだな。最高はやっぱRubyか？
- 104 名前：デフォルトの名無しさん mailto:sage [05/01/20 22:02:41 ]
- 関数fとは、定義域dom(f)と値域cod(f)の間の関係であって、
∀x ∈ dom(f). ∀y, z ∈ cod(f). f x = y ∧ f x = z ⇒ y = z
を満たすものを言う。
- 105 名前：デフォルトの名無しさん mailto:sage [05/01/20 22:07:43 ]
- void function(void)
- 106 名前：デフォルトの名無しさん mailto:sage [05/01/20 22:08:22 ]
- >>86は凄スレアンカーのつもりだったんだが・・ｲｲﾖｲｲﾖ～
- 107 名前：デフォルトの名無しさん mailto:sage [05/01/20 22:11:49 ]
- >104と>105は別に矛盾しないな。
- 108 名前：デフォルトの名無しさん mailto:sage [05/01/20 22:14:46 ]
- そしてmonadやstate transformerの話になるか。
- 109 名前：デフォルトの名無しさん mailto:sage [05/01/20 22:24:20 ]
- Cの関数は最強。
だって数学厨でもCには文句つけない。
- 110 名前：デフォルトの名無しさん mailto:sage [05/01/20 22:25:29 ]
- ｱｯﾀﾏﾜﾙｿｰなｽﾚ
、と思ったら実は中身はRubyスレか。
,riTl|l.il|..ll..|ll.i..lli､
ril l!|.|ｌ|.l||!.l|.|l|lil.l|l|l
||ｌ!ｉ!|州l|l|ll||lllﾐilｌll|l|
!|||ﾗ''' '´!|ll||l!lｿ|||l|| こ
`ｔ'_,,,ヽ i´l州 の
ﾞiｰ '' ／ｉ',ﾉ'ﾞ入 荒 ス
`ー'､´ ／,r'´ ,>､ れ レ
,ｲy' ／ ／,ｒ ヽ, 見 て
,ｒ'// / ／,i' ' ｉ ﾞ､ え い
／,/ｌｉ,/ ,/,i',i' ,ｒ ,ｒ7' ヽ,ｉ. 奥 る る
〃,//ｌ/ .// ,' /'´ / ﾊ. が が. よ
/,' / ｌ./ ,ｉ'ｉ ｌ// / / ｌ 深 う
/ ,ｉ ,i ,!/ ,i' l // ,/ ,/ l. い 案. に
,/ l l i l./ !i .l / _,/ ／ l! . ・ .外
,r'=‐､_ll_!j'_,_､-‐､‐' __,,. !l. . ・
/ﾉ /´/ ｀`ヽ､ ｀ ｀`''''"´ ,! l ・
/´ ,/-/ ｀` ｀`ヽ､､___,, i l
/ ,.ｲl / ,.r‐ ｀`ヽ､,__ ,! ./!l
/ jly' - '´ i i !.|
- 111 名前：デフォルトの名無しさん mailto:sage [05/01/20 22:27:08 ]
- 値はvoidだし…
- 112 名前：デフォルトの名無しさん mailto:sage [05/01/20 22:29:54 ]
- わざわざvoid用意するってことは…そういうことだな。
- 113 名前：デフォルトの名無しさん mailto:sage [05/01/20 22:37:39 ]
- void関数だけ使う数学に厳しい数学厨。
文法エラーのような気もするが。
- 114 名前：デフォルトの名無しさん mailto:sage [05/01/20 22:39:37 ]
- プログラムの実行過程に応じて関数の解釈が変化すると考えれば、値の一意性は
保たれるな。evolving algebraなんてのもあったっけ。
- 115 名前：83 mailto:sage [05/01/20 22:39:52 ]
- >>94
そう言ったつもりなんだけど……。
- 116 名前：デフォルトの名無しさん mailto:sage [05/01/20 22:40:56 ]
- 【結論】
日本人はコンパイラ・スクリプトエンジンを開発するには向いてない。
- 117 名前：デフォルトの名無しさん mailto:sage [05/01/20 22:42:14 ]
- bison++2.0ﾏﾀﾞｰ？
- 118 名前：デフォルトの名無しさん mailto:sage [05/01/20 22:43:29 ]
- Kripke構造を用いたpossible worlds semanticsとかもあるな。
60年代も今も余り苦労は変わらない。
- 119 名前：デフォルトの名無しさん mailto:sage [05/01/20 22:47:48 ]
- >>115
だから、、普通、プログラミング言語の用語の意味は人間の言葉で「定義」してる。
これが間違い。↓
>そもそも文や式の「定義」は、大抵の言語では文法の上で定義するよね (厳密には BNF とか) 。
>意味 (値を返すとか返さないとか) から「説明」することはできるけど、
>それは「定義」じゃないし。
- 120 名前：デフォルトの名無しさん mailto:sage [05/01/20 22:52:29 ]
- >>109
そりゃ、数学の関数とCの関数は別物なんだから当たり前。
分野によって言葉の定義が違うのが当たり前。
言語によっても定義が違うのが当たり前。
- 121 名前：デフォルトの名無しさん mailto:sage [05/01/20 22:56:22 ]
- >>119
あ、ひょっとして
BNF exp ::= digit+ | exp + exp | exp - exp | ...
ではなくて
「『式』とは上の exp のことである」
この日本語が「定義」だ、って言ってる？
それとも、用語は普通こんな日本語では定義しない、って言ってるのかな。
- 122 名前：デフォルトの名無しさん mailto:sage [05/01/20 23:00:02 ]
- >>121
>BNF exp ::= digit+ | exp + exp | exp - exp | ...
これは一応定義の一部と解釈できるかもしれないが、どちらにせよ、
「構文規則」を定義してるだけ。
意味を完全に定義してるわけじゃない。
用語の意味を定義するには、「これはここを繰り返す」「これは値を返す」
「この値がtrueの時にここを実行」等、人間の言葉で定義するのが普通。
Cもそう。
- 123 名前：デフォルトの名無しさん mailto:sage [05/01/20 23:05:42 ]
- >>122
えーと。
だから「式と文の違いを意味で説明することはできるかもしれないが、
それは別に式と文それぞれの定義ではない」とゆーたんですよ。
- 124 名前：デフォルトの名無しさん mailto:sage [05/01/20 23:08:36 ]
- >>121ではないが、>>122の想定してる定義は
swissnet.ai.mit.edu/~jaffer/r5rs-formal.pdf
の7.2節みたいな内容か？
まあすべての言語がalgolやsmlやschemeみたいな意味定義は持ってないわな。
- 125 名前：123 mailto:sage [05/01/20 23:12:34 ]
- あー！わかった。
漏れ「式とはこういう構文のことだ。そのように定義される式はこういう意味をもつ(これは式の定義ではなく式の意味の定義、のつもり)」
>122「式とはこういう構文であり、かつこういう意味をもつものだ」
とそれぞれ主張していたのか。多分。
この辺は趣味じゃないかなー。
- 126 名前：デフォルトの名無しさん mailto:sage [05/01/20 23:17:12 ]
- >>123 >>125
あのね、
>そもそも文や式の「定義」は、大抵の言語では文法の上で定義するよね (厳密には BNF とか) 。
>漏れ「式とはこういう構文のことだ。そのように定義される式はこういう意味をもつ(これは式の定義ではなく式の意味の定義、のつもり)」
これがとりあえず間違いなのね。文や式の定義って言う時は、普通、「意味」の定義のこと、あるいは、意味を含んだ定義を
言ってるわけで、文法上では定義されないの。
>意味 (値を返すとか返さないとか) から「説明」することはできるけど、
>それは「定義」じゃないし。
この「それ」は「違いを意味で説明すること」だったわけね・・・・
それはこちらが誤解してました。スマソ。
俺が定義だといってるのは、「値を返す」とかの説明がまさに意味の
定義だから。定義と言ってたわけ。
>>124
そうだよ。そういうふうに意味論で定義するか、もしくは自然言語で定義するわけだけど、
これは文法とは別物。
- 127 名前：デフォルトの名無しさん mailto:sage [05/01/20 23:23:28 ]
- >>124
しかしそれも今となっては古めかしいな。
言語に並行性を取り込もうとすると全面書き直しになりそうだ。
- 128 名前：デフォルトの名無しさん mailto:sage [05/01/20 23:25:43 ]
- 激論のとこ今更で悪いが、そもそもCの式は厳密には、値を”返さない”ぞ
operatorや関数が値を返すだけでなｗ
式は値を返すが、文は値を返さないとか言ってる奴はCでも間違いだぞｗ
- 129 名前：123 mailto:sage [05/01/20 23:31:17 ]
- >>126
うーん、考え直すとやっぱ
>122「式とはこういう構文であり、かつこういう意味をもつものだ」
の方が自然ですね。ごめん。
>>128
今度は「返す」「返さない」の意味定義の話？
- 130 名前：デフォルトの名無しさん mailto:sage [05/01/20 23:32:35 ]
- どうせ例をあげるならvoid型関数の呼び出し式にでもすればよかったのに。
- 131 名前：デフォルトの名無しさん mailto:sage [05/01/20 23:45:26 ]
- 値を持つ・値が定まる
- 132 名前：デフォルトの名無しさん mailto:sage [05/01/20 23:53:46 ]
- >>127
7.2節は意味関数で定義されてるが
それは人間の言葉で定義してるということでいいのか？
- 133 名前：デフォルトの名無しさん mailto:sage [05/01/20 23:56:42 ]
- Ruby厨の脳内仕様では値を持つも値を返すも同じ
- 134 名前：デフォルトの名無しさん [05/01/21 00:00:49 ]
- >>128
そうなのか？orz
ところで、式と文の関係は言語に関係なく、
式⊂文
でいいんだよなぁ？
これに反する言語ってある？
- 135 名前：デフォルトの名無しさん mailto:sage [05/01/21 00:00:58 ]
- void がイカンのは
( void ∈ dom(f) ) = false ∧ ( void ∈ ∈ cod(f) ) = false
が常に成立するからだとおもふ
- 136 名前：デフォルトの名無しさん mailto:sage [05/01/21 00:01:44 ]
- あっ、∈が一個多すぎた、まあ気にするな。
- 137 名前：デフォルトの名無しさん mailto:sage [05/01/21 00:05:20 ]
- >>126
煽りじゃなくて単に見解を聞きたいんだけど、
式のセマンティクスを定義するのに式という言葉を使いたくて
式という言葉をとりあえずBNFとかで定義しておいて、
「式は値を持つ」とかいう形でセマンティクス上の意味を付加していくことがある
（特に数学的にセマンティクスを定義したい場合）。
こういう場合、「式という言葉（の意味）」はBNFで定義され
「式の（セマンティクス上の）意味」は日本語とかで定義される、
といったことになると思うんだけど、どう？
- 138 名前：デフォルトの名無しさん mailto:sage [05/01/21 00:08:08 ]
- こんだけ暴れて何も学んでないんだなぁ。
- 139 名前：デフォルトの名無しさん mailto:sage [05/01/21 00:10:12 ]
- 「式という言葉（の意味）」はBNFで定義され
は
「式という言葉（の字面・パターン）」はBNFで定義され
じゃない？
- 140 名前：デフォルトの名無しさん mailto:sage [05/01/21 00:11:38 ]
- >>137
俺の見解としては、それは普通に間違い。
「式の意味」という言葉を人間が使う時、普通は「式の（セマンティクス上の）意味」を指すから。
あくまで、BNFで使っている名前は、構文規則を定義するための記号にすぎず、
人間が「式という言葉（の意味）」と言っているときでも、そのBNF上の記号を
指しているということはまず無い。
ここでのもともとの議論も無論、前者の意味で皆「式は～」と言っていた。
- 141 名前：デフォルトの名無しさん mailto:sage [05/01/21 00:12:58 ]
- >>134の
「 ところで、式と文の関係は言語に関係なく、
式⊂文
」はいいの？ またRuby論理？
- 142 名前：デフォルトの名無しさん mailto:sage [05/01/21 00:13:45 ]
- (ﾟ∈ﾟ )
- 143 名前：デフォルトの名無しさん mailto:sage [05/01/21 00:15:59 ]
- >>132
127じゃないが、良くないよ。
人間の言葉で定義している場合が多いというだけで、
Schemeの7.2節は例外。
Schemeは人間の言葉と、形式的な意味論と両方の定義が存在するな。
後者の方がより厳密かもしれない。
- 144 名前：123 mailto:sage [05/01/21 00:16:58 ]
- >>137
僕もそんな風に考えてたんだけど、どっちも「式」の定義だし、
「普通」は式の定義というと意味論的な意味のことを指すと言われれば
反論できないし、そんな気もしてきた。
>>141
漏れがそうでない言語を定義してあげよう。
- 145 名前：123 mailto:sage [05/01/21 00:18:22 ]
- ×意味論的な意味
○意味論的な定義
- 146 名前：デフォルトの名無しさん mailto:sage [05/01/21 00:19:04 ]
- 形式的意味論で定義していないプログラム言語は
意味関数で定義できないということを意味しているの？
- 147 名前：デフォルトの名無しさん mailto:sage [05/01/21 00:20:41 ]
- 意味関数の定義自体は人間の言葉で定義してるんだから
結局は人間の言葉で定義してることにならん？
>>146
意味関数で定義できるけどしてないだけの場合も。
- 148 名前：デフォルトの名無しさん mailto:sage [05/01/21 00:21:10 ]
- >>144
極端なこと言えば、式の構文を定義するのに、式という言葉を使わなくてもいいわけで。
もちろん、わかりにくいからそんなことは普通しないんだけど、例えば、stmtって略したり
する時もある。
だから、BNF上の記号はあくまで言葉の（意味の）定義とは別。
構文規則を定義するために便宜上わかりやすい名前をつけた記号に過ぎない。
- 149 名前：デフォルトの名無しさん mailto:sage [05/01/21 00:22:39 ]
- >>147
まあ、間接的には結局そういうことだよ。
数学だってそう言えてしまう。
でも、普通はそういう直接自然言語で定義してないものを
自然言語で定義してるとは言わないわな。
- 150 名前：デフォルトの名無しさん mailto:sage [05/01/21 00:23:43 ]
- Rubyの人が言うように仕様書で自由に決めたとき
意味関数に落とすと矛盾が発生することはないの？
- 151 名前：デフォルトの名無しさん mailto:sage [05/01/21 00:24:41 ]
- >>150
あるに決まってるだろ。その場合はもちろん無効だよ。
そういうバグが無いことを前提にみんな議論してるんだろ。
- 152 名前：デフォルトの名無しさん mailto:sage [05/01/21 00:25:27 ]
- >>150
矛盾が発生しないように意味関数を定義していくんじゃないかな。
ひょっとして意味関数を「日本語->意味」みたいな関数だと思ってる？
- 153 名前：デフォルトの名無しさん mailto:sage [05/01/21 00:26:22 ]
- Schemeの意味関数とRubyを形式意味論を用いて意味関数に落としたものは
互いに矛盾するってことはある？
- 154 名前：デフォルトの名無しさん mailto:sage [05/01/21 00:27:01 ]
- >>153
意味がわからない。矛盾するもなにも、別の言語の別の定義だからなんの関係もない。
- 155 名前：デフォルトの名無しさん mailto:sage [05/01/21 00:27:53 ]
- swissnet.ai.mit.edu/~jaffer/r5rs-formal.pdf
の7.2節の形式の意味関数を念頭においてますよ。
- 156 名前：デフォルトの名無しさん mailto:sage [05/01/21 00:30:16 ]
- >>154
同じ状態機械を想定して
同じ形式の意味関数を用いたらどうです？
- 157 名前：デフォルトの名無しさん mailto:sage [05/01/21 00:30:34 ]
- で？何が聞きたいの？
SchemeとRubyの間の矛盾って？
- 158 名前：デフォルトの名無しさん mailto:sage [05/01/21 00:32:59 ]
- 一方では文は値を持ち、他方では持たないと自由に定義されてると
抽象機械の遷移状態が異なってくることはないですか？
- 159 名前：デフォルトの名無しさん mailto:sage [05/01/21 00:34:43 ]
- 言語が違うんだから、形式（？）なるものが同じだとしても、意味関数や状態遷移機械は
もちろん違うし、全く関係ないんだが。
- 160 名前：デフォルトの名無しさん mailto:sage [05/01/21 00:37:01 ]
- >>159
なんだか見えない相手と戦っているドンキホーテのようだな。がんがれ。
- 161 名前：デフォルトの名無しさん mailto:sage [05/01/21 00:37:24 ]
- すみません、「形式（？）」って具体的にお願いします。
- 162 名前：デフォルトの名無しさん mailto:sage [05/01/21 00:38:43 ]
- >>161
俺が聞きたいよ。
お前が「形式が同じだとどうです？」と言ってるだろ。
察するに、表示的意味論なら表示的意味論、操作的意味論なら操作的意味論で、
似たような記号使うということか？
- 163 名前：デフォルトの名無しさん mailto:sage [05/01/21 00:38:46 ]
- 意味関数の記述形式のことでいいですか？
- 164 名前：デフォルトの名無しさん mailto:sage [05/01/21 00:39:38 ]
- >>163
いいですか？てなんだよ。お前が使ってる言葉だろ。
- 165 名前：デフォルトの名無しさん mailto:sage [05/01/21 00:40:23 ]
- とりあえず、俺に聞く前に意味論の本読んでください。
- 166 名前：137 mailto:sage [05/01/21 00:42:11 ]
- >>140
了解。㌧ｸｽ。
>>139
うーんと、式＝加算or減算etcって感じ。
数学的には
式の集合＝加算の集合∪減算の集合∪etc
みたいな。
- 167 名前：デフォルトの名無しさん mailto:sage [05/01/21 00:44:58 ]
- 言語が違っても処理が同じなら、ターゲットの抽象機械が同じで
同じ意味関数を用いれば、おなじ記述になるはずですが、
文の定義が異なるのなら両者の遷移状態は異なることになりませんか？
- 168 名前：デフォルトの名無しさん mailto:sage [05/01/21 00:49:34 ]
- 同じ記述結果が出来るはずなのに、遷移状態が異なるのは
問題ではないのか？ということだな。
- 169 名前：デフォルトの名無しさん mailto:sage [05/01/21 00:52:16 ]
- 言質を確かめられてるだけで、意味論のことをおまえに
聞いてる訳じゃなさそうだから答えてやれ >>165
- 170 名前：デフォルトの名無しさん mailto:sage [05/01/21 00:54:09 ]
- 文の定義とは勿論「文」の意味論的定義な
- 171 名前：デフォルトの名無しさん mailto:sage [05/01/21 00:54:20 ]
- >>167-168
偶然同じ処理で同じ記述になろうが、別の処理で別の記述になろうが、
別の世界の別の定義同士は何の関係も無いぞ。
あと、表示的意味論と操作的意味論ごっちゃになってるだろ。
- 172 名前：デフォルトの名無しさん mailto:sage [05/01/21 00:57:37 ]
- 同じ抽象機械で同じ目的の処理なら関係ないとホントにいえるのか？
- 173 名前：デフォルトの名無しさん mailto:sage [05/01/21 01:04:53 ]
- ていうか、SchemeとRuby全然違うだろ。
同じ目的の処理とかほとんどありえない。そもそもSchemeに文なんて無いだろ。
- 174 名前：デフォルトの名無しさん mailto:sage [05/01/21 01:06:46 ]
- >>173
ふふん？？
- 175 名前：デフォルトの名無しさん mailto:sage [05/01/21 01:10:15 ]
- 仮に、操作的意味論で、同じ抽象機械が対象で同じ目的の処理なら、同じ記述にできるよ。
違う目的なら違う記述になるよ。
で？それが何？
- 176 名前：デフォルトの名無しさん mailto:sage [05/01/21 01:13:17 ]
- gcでlazy sweepについて知りたいんだけど
なにかいい文献ない？
- 177 名前：デフォルトの名無しさん mailto:sage [05/01/21 02:03:20 ]
- くだらない質問なんですが、
構文解析器のことを英語で"parser"と言いますが、
字句解析器は英語で何と言うのでしょうか？
- 178 名前：デフォルトの名無しさん mailto:sage [05/01/21 02:04:36 ]
- >>177
lexer
# 数時間でえらい書き込みだと思ったら案の定・・・
- 179 名前：デフォルトの名無しさん mailto:sage [05/01/21 03:03:07 ]
- scannerてのも見るけど
- 180 名前：デフォルトの名無しさん mailto:sage [05/01/21 03:09:37 ]
- スキャナだと意味が広すぎるんでは
知らんけど
- 181 名前：デフォルトの名無しさん [05/01/21 03:47:45 ]
- 死ね。
- 182 名前：デフォルトの名無しさん mailto:sage [05/01/21 03:53:25 ]
- lexというツールもあるくらいだし、lexerですかね。
ありがとうございます。
- 183 名前：デフォルトの名無しさん mailto:sage [05/01/21 03:56:15 ]
- そういえば、Schemeに文はありませんでしたね。
- 184 名前：デフォルトの名無しさん [05/01/21 03:59:22 ]
- う
- 185 名前：デフォルトの名無しさん mailto:sage [05/01/21 04:04:47 ]
- >>176
定番のあの青い本にのってない？
- 186 名前：デフォルトの名無しさん [05/01/21 04:49:21 ]
- ん
- 187 名前：デフォルトの名無しさん [05/01/21 05:02:26 ]
- う
- 188 名前：デフォルトの名無しさん mailto:sage [05/01/21 05:14:58 ]
- なんでもいいから早く誰か俺言語さらせよ
- 189 名前：デフォルトの名無しさん mailto:sage [05/01/21 07:38:01 ]
- 俺言語I(cbt)
[syntax]
x ∈ Var
n ∈ Nat
Exp e ::= n | x | e1 e2 | e(x)
[semantics]
s ∈ State = Var -> Exp
[[e]]s = n iff s |- e => n
s |- n => n
s |- x => s(x)
s |- e1(x) e2 => e1[e2/x] <- capture avoiding substitution
s |- e(x) => e(x)
- 190 名前：デフォルトの名無しさん mailto:sage [05/01/21 08:29:37 ]
- ぜんぜん意味わかんないから説明ｷﾎﾞﾝ。
∈ってなん？
- 191 名前：デフォルトの名無しさん mailto:sage [05/01/21 08:34:52 ]
- くちばし
|
 |
