Ads by Google
新しい記事を書く事で広告が消せます。
セマンティクス
soutaroにっき 2008-05-30 ■セマンティクス
ひげぽん OSとか作っちゃうかMona- 2008/05/30 セマンティクスって？
セマンティクスを議論するためには，計算モデルを決めないといけません．
計算モデルが決まれば，状態の表現方法が決まり，「計算」という概念が決まります．
計算というのは，状態変化の列のことです．
計算が決まれば，計算とプログラムの対応関係を決定することができます．
その，対応関係のことが 「意味論 (semantics)」だと思います．
任意のプログラム空間 P 内のプログラム p ∈ P と，任意の計算空間 C 内の計算（状態の変化列） c ∈ C の組 ＜p, c＞ が意味論という気がします （いや，メチャクチャテキトーで，個人的なイメージですけど）
ここらへんを真面目に考えているのは，たぶん等価変換計算モデル(Equivalent Transformation Computation Model) だけで，他の計算モデルは，一つに決め打ちされた，ET 計算モデルという枠組みの具体例の一つ（インスタンス）に過ぎない（と考えられるかもしれない）．
個人的には，構文論(syntax) ってのは，「プログラムが文字列の形で書かれる」 ことに由来するもので，本質では無いと考えています．
プログラムと，計算という構造のマッピングである，意味論こそが本丸であると．プログラムの見た目などどうでも良いのです (意味論さえ明確ならば)．
操作的意味論ってのは，まぁ定式化にはいろんなスタイルがあるわけですけど，TAPL とかでは，状態を項(term)で表現して，それを書き変える推論規則の集合で意味論（プログラムと計算の対応）が定義されるのかなと．推論規則が，term を値にするものか，term から term にするものかの違いで，big step とか small step とかスタイルがあるそうです．
表示的意味論ってのは，文字列（プログラム）と数学的オブジェクトの対応関係を定義することで，意味論を与えるものだと思います．soutaro さんが，別のプログラムに変換する規則を与えることで，意味論を与える方法があるとか書いてますけど，ある意味でこれは，プログラムを数学というプログラミング言語に変換することによって，意味論を与えているのと同じこと（かもしれません）．
公理的意味論は，論理プログラミングという，証明=計算というパラダイムと強く結びついているので，わりとそのまんまです．プログラムは公理であり，そこから演繹できる全ての項が意味であると．んで，与えられたクエリ項が，その中に含まれていれば真．いなければ偽という，単純明快．
等価変換計算モデルにおいては，確定節で仕様が記述され，そこから任意有限回の変換で得られるアトムの集合で仕様の意味が与えられます．公理的意味論とかなり似てますが，論理式の証明というパラダイムに依存しない，より一般的で包括的な計算モデルになってます （論理・制約プログラミングやCHR も，ET モデルの具体例の一つであることが証明されています．たぶん，命令型プログラミングやオブジェクト指向プログラミングや関数プログラミングなども）．例えば，論理プログラミングにおける単一化は，特殊化というより一般的な概念のインスタンスです．データ構造も，論理式（一階の項）に限らない，豊富なものを特殊化システムという枠組みによって扱うことができます．同じ意味を得られる変換列（= 計算）は，同じ意味を持つ計算と定義されるので，豊富なプログラムの空間の中から，最適なプログラムを自動探索することが可能になります （詳しくはFormalization of the Equivalent Transformation Computation Modelあたりを）．
形式意味論が無い言語の場合は，人間の頭の中に計算の舞台が存在して，その舞台の変化を頭の中でシミュレートすることで，個人の脳内でソースコードに対して意味論を与えていることになるわけですね．これでは，もちろん自動検証できませんし，何の客観性も無いわけで，正確なコミュニケーションは不可能です （これが，どれだけ正確さを心がけて，アセンブラやプログラミング言語 C などでのプログラミングを人に教えようとしても，どうしても誤解が発生してしまう，本質的原因だと思います）
形式意味論が無い言語は，何が正しいのか，という議論ができません．そんな言語を教えている時点で，大学の計算機科学の講義なんて，ちっとも科学と呼べるような代物では無いよな，と個人的には思ってます．
ひげぽん OSとか作っちゃうかMona- 2008/05/30 セマンティクスって？
セマンティクスを議論するためには，計算モデルを決めないといけません．
計算モデルが決まれば，状態の表現方法が決まり，「計算」という概念が決まります．
計算というのは，状態変化の列のことです．
計算が決まれば，計算とプログラムの対応関係を決定することができます．
その，対応関係のことが 「意味論 (semantics)」だと思います．
任意のプログラム空間 P 内のプログラム p ∈ P と，任意の計算空間 C 内の計算（状態の変化列） c ∈ C の組 ＜p, c＞ が意味論という気がします （いや，メチャクチャテキトーで，個人的なイメージですけど）
ここらへんを真面目に考えているのは，たぶん等価変換計算モデル(Equivalent Transformation Computation Model) だけで，他の計算モデルは，一つに決め打ちされた，ET 計算モデルという枠組みの具体例の一つ（インスタンス）に過ぎない（と考えられるかもしれない）．
個人的には，構文論(syntax) ってのは，「プログラムが文字列の形で書かれる」 ことに由来するもので，本質では無いと考えています．
プログラムと，計算という構造のマッピングである，意味論こそが本丸であると．プログラムの見た目などどうでも良いのです (意味論さえ明確ならば)．
操作的意味論ってのは，まぁ定式化にはいろんなスタイルがあるわけですけど，TAPL とかでは，状態を項(term)で表現して，それを書き変える推論規則の集合で意味論（プログラムと計算の対応）が定義されるのかなと．推論規則が，term を値にするものか，term から term にするものかの違いで，big step とか small step とかスタイルがあるそうです．
表示的意味論ってのは，文字列（プログラム）と数学的オブジェクトの対応関係を定義することで，意味論を与えるものだと思います．soutaro さんが，別のプログラムに変換する規則を与えることで，意味論を与える方法があるとか書いてますけど，ある意味でこれは，プログラムを数学というプログラミング言語に変換することによって，意味論を与えているのと同じこと（かもしれません）．
公理的意味論は，論理プログラミングという，証明=計算というパラダイムと強く結びついているので，わりとそのまんまです．プログラムは公理であり，そこから演繹できる全ての項が意味であると．んで，与えられたクエリ項が，その中に含まれていれば真．いなければ偽という，単純明快．
等価変換計算モデルにおいては，確定節で仕様が記述され，そこから任意有限回の変換で得られるアトムの集合で仕様の意味が与えられます．公理的意味論とかなり似てますが，論理式の証明というパラダイムに依存しない，より一般的で包括的な計算モデルになってます （論理・制約プログラミングやCHR も，ET モデルの具体例の一つであることが証明されています．たぶん，命令型プログラミングやオブジェクト指向プログラミングや関数プログラミングなども）．例えば，論理プログラミングにおける単一化は，特殊化というより一般的な概念のインスタンスです．データ構造も，論理式（一階の項）に限らない，豊富なものを特殊化システムという枠組みによって扱うことができます．同じ意味を得られる変換列（= 計算）は，同じ意味を持つ計算と定義されるので，豊富なプログラムの空間の中から，最適なプログラムを自動探索することが可能になります （詳しくはFormalization of the Equivalent Transformation Computation Modelあたりを）．
形式意味論が無い言語の場合は，人間の頭の中に計算の舞台が存在して，その舞台の変化を頭の中でシミュレートすることで，個人の脳内でソースコードに対して意味論を与えていることになるわけですね．これでは，もちろん自動検証できませんし，何の客観性も無いわけで，正確なコミュニケーションは不可能です （これが，どれだけ正確さを心がけて，アセンブラやプログラミング言語 C などでのプログラミングを人に教えようとしても，どうしても誤解が発生してしまう，本質的原因だと思います）
形式意味論が無い言語は，何が正しいのか，という議論ができません．そんな言語を教えている時点で，大学の計算機科学の講義なんて，ちっとも科学と呼べるような代物では無いよな，と個人的には思ってます．
コメント
こんにちは。解説ありがとうございます。
すべて理解できたかは怪しいですが勉強になりました。
＞個人的には，構文論(syntax) ってのは，「プログラムが文字列の形で書かれる」 ことに由来するもので，本質では無いと考えています．
このあたりが特に頭の中でふわふわしていたのですが、やはりという感じでなっとくです。
すべて理解できたかは怪しいですが勉強になりました。
＞個人的には，構文論(syntax) ってのは，「プログラムが文字列の形で書かれる」 ことに由来するもので，本質では無いと考えています．
このあたりが特に頭の中でふわふわしていたのですが、やはりという感じでなっとくです。
> ひげぽん さん
文字列の形で表現されるソースコードの裏には，対応する何らかの構造があると．
それこそが意味なんじゃないかと思います．
字面だけ見て，不正なコードを排除できるから，構文論も重要なんですが，本質は意味論なのではないか，と．
要するに，コンパイラも，近代的なインタプリタも，一番最初に，プログラム全体を文字列処理して，ソースコードからデータ構造を作りますよね．
なので，構文論は，その段階で invalid なプログラムをはじけるから，実用的には便利 (というだけのこと，かと)
仮に，文字列以外の形で，ちょくせつ構造を処理系に流し込めたら，そもそも構文論とか要らなくなりますしね．
いや，まぁ，我々の思考は，文字と強く結びついているのだから，それは詭弁で，構文論も重要だよ！という意見も正しいとは思います．
それこそが意味なんじゃないかと思います．
字面だけ見て，不正なコードを排除できるから，構文論も重要なんですが，本質は意味論なのではないか，と．
要するに，コンパイラも，近代的なインタプリタも，一番最初に，プログラム全体を文字列処理して，ソースコードからデータ構造を作りますよね．
なので，構文論は，その段階で invalid なプログラムをはじけるから，実用的には便利 (というだけのこと，かと)
仮に，文字列以外の形で，ちょくせつ構造を処理系に流し込めたら，そもそも構文論とか要らなくなりますしね．
いや，まぁ，我々の思考は，文字と強く結びついているのだから，それは詭弁で，構文論も重要だよ！という意見も正しいとは思います．
>構文論は，その段階で invalid なプログラムをはじけるから，実用的には便利 (というだけのこと，かと)
良い説明ですね。納得納得！
＞いや，まぁ，我々の思考は，文字と強く結びついているのだから，それは詭弁で，構文論も重要だよ！という意見も正しいとは思います．
はい。ぼくもそう思います。
良い説明ですね。納得納得！
＞いや，まぁ，我々の思考は，文字と強く結びついているのだから，それは詭弁で，構文論も重要だよ！という意見も正しいとは思います．
はい。ぼくもそう思います。
専門的な議論の中に混じるスパムの違和感に吹いた(本気で人を呼び込みたいならセックスとプログラム意味論を絡めて論じないと……)。
すいません、素人のむちゃむちゃ、てきとーな質問ですが、
とんちかんな質問であれば流しちゃって下さい。
> 計算モデルが決まれば，状態の表現方法が決まり，「計算」という概念が決まります．
計算の概念っていろいろとあるのでしょうか。
チューリング等価であることが計算だと考えていますが。
> セマンティクスを議論するためには，計算モデルを決めないといけません．
各言語がそれぞれの特有の計算モデルを使用するより、
各言語が、ひとつの計算モデルに対して意味論を構築した方が
言語間の翻訳作業がすんなりいくように思えます。
それが
> 等価変換計算モデル... より一般的で包括的な計算モデルになってます
などに掛かるのでしょうか。
> 計算が決まれば，計算とプログラムの対応関係を決定することができます．
> その，対応関係のことが 「意味論 (semantics)」だと思います．
マシン語を計算と捉え、C言語をプログラムと捉えた場合、
コンパイラは意味論といえますか。
加えていえば、結局、C言語は正しいコンパイラなど存在しないと
言えるのでしょうか。
とんちかんな質問であれば流しちゃって下さい。
> 計算モデルが決まれば，状態の表現方法が決まり，「計算」という概念が決まります．
計算の概念っていろいろとあるのでしょうか。
チューリング等価であることが計算だと考えていますが。
> セマンティクスを議論するためには，計算モデルを決めないといけません．
各言語がそれぞれの特有の計算モデルを使用するより、
各言語が、ひとつの計算モデルに対して意味論を構築した方が
言語間の翻訳作業がすんなりいくように思えます。
それが
> 等価変換計算モデル... より一般的で包括的な計算モデルになってます
などに掛かるのでしょうか。
> 計算が決まれば，計算とプログラムの対応関係を決定することができます．
> その，対応関係のことが 「意味論 (semantics)」だと思います．
マシン語を計算と捉え、C言語をプログラムと捉えた場合、
コンパイラは意味論といえますか。
加えていえば、結局、C言語は正しいコンパイラなど存在しないと
言えるのでしょうか。
> 田辺さん
いや〜，もちろん，究極的に抽象的にはチューリング等価何ですけど．
より具体的なレベルの計算モデルにおいては，メモリモデル（チューリングマシン，ポストマシン）とか項簡約(ラムダ計算，書き換えシステム)とか帰納関数とかいろいろあって，それぞれが計算能力が等価ってのは，対応関係が存在するというだけのことなので，実際に計算という概念を表現する際の方法にはいろいろありますよね．
計算モデルをどのように定式化するか．状態をどうやって表現して，どういう初期化をして，どうやって計算を進めて，どうやって答えを得るか．さらにもっと上のレベルの，豊富なデータ構造のレベル（ラムダ計算とか論理式は抽象的過ぎて，データ構造という概念は存在しません．全て項．ある意味統一的なんですけど，現実的なプログラムの表現のための理論としては不十分かと） をどのようにして統一的に扱うか．そして，何を持って仕様に対して正しいプログラムと定義し，正当かつ十分に効率的なプログラムを，いかにして正しい変換の繰り返しによって得るか．
それらの，プログラム構築において理論化可能と考えられる部分の，上から下まで全ての理論化をやってるのが，等価変換理論ということ （だと，少なくとも我々は信じています）
C とアセンブラは，同じ計算モデル （メモリ空間を命令で状態遷移させていく） なので，対応関係を定式化するまでもなく，素直に完璧に正しいコンパイラが（少なくとも原理的には）作れるはずです．ただし，C にもアセンブラにも形式意味論が存在しないので，それぞれ（の，おそらくサブセット）に形式的意味を与えてやり，両方のプログラムが同じ意味(= 状態遷移)を行うことを証明する必要があると思います （実際にそういう研究があるみたいです）
http://d.hatena.ne.jp/sumii/20060418/1145330147
> Theoria さん
スパム，ホント困ります… 最近急に増えてきて，キーワードとかも，なんだか効いてないみたい… FC2 のバグかなんかなんですかね ?
より具体的なレベルの計算モデルにおいては，メモリモデル（チューリングマシン，ポストマシン）とか項簡約(ラムダ計算，書き換えシステム)とか帰納関数とかいろいろあって，それぞれが計算能力が等価ってのは，対応関係が存在するというだけのことなので，実際に計算という概念を表現する際の方法にはいろいろありますよね．
計算モデルをどのように定式化するか．状態をどうやって表現して，どういう初期化をして，どうやって計算を進めて，どうやって答えを得るか．さらにもっと上のレベルの，豊富なデータ構造のレベル（ラムダ計算とか論理式は抽象的過ぎて，データ構造という概念は存在しません．全て項．ある意味統一的なんですけど，現実的なプログラムの表現のための理論としては不十分かと） をどのようにして統一的に扱うか．そして，何を持って仕様に対して正しいプログラムと定義し，正当かつ十分に効率的なプログラムを，いかにして正しい変換の繰り返しによって得るか．
それらの，プログラム構築において理論化可能と考えられる部分の，上から下まで全ての理論化をやってるのが，等価変換理論ということ （だと，少なくとも我々は信じています）
C とアセンブラは，同じ計算モデル （メモリ空間を命令で状態遷移させていく） なので，対応関係を定式化するまでもなく，素直に完璧に正しいコンパイラが（少なくとも原理的には）作れるはずです．ただし，C にもアセンブラにも形式意味論が存在しないので，それぞれ（の，おそらくサブセット）に形式的意味を与えてやり，両方のプログラムが同じ意味(= 状態遷移)を行うことを証明する必要があると思います （実際にそういう研究があるみたいです）
http://d.hatena.ne.jp/sumii/20060418/1145330147
> Theoria さん
スパム，ホント困ります… 最近急に増えてきて，キーワードとかも，なんだか効いてないみたい… FC2 のバグかなんかなんですかね ?
ご説明ありがとうございます。毎度ながら勉強になります。
> 十分に効率的な..
この辺りが面倒そうですね。
> 十分に効率的な..
この辺りが面倒そうですね。
素朴な疑問なのですが、公理的意味論と論理プログラミングって、そんなに強い結びつきがあるのでしょうか?
公理的意味論と論理プログラミングの関係は良く知らないのですが、公理的意味論は、ホーア論理にしても、述語変換子意味論にしても、dynamic logic にしても、手続き型言語を対象として発展してきた印象があるので……
公理的意味論と論理プログラミングの関係は良く知らないのですが、公理的意味論は、ホーア論理にしても、述語変換子意味論にしても、dynamic logic にしても、手続き型言語を対象として発展してきた印象があるので……
> さかいさん
そうですね，制約（契約）関係の記述なので，LP に限定されるものでは無いですね… （単に私が，手続き型言語の方の意味論とか全然知らないだけ．あと，公理と聞くとロジックを連想するという）
