セマンティクス
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 などでのプログラミングを人に教えようとしても，どうしても誤解が発生してしまう，本質的原因だと思います）
形式意味論が無い言語は，何が正しいのか，という議論ができません．そんな言語を教えている時点で，大学の計算機科学の講義なんて，ちっとも科学と呼べるような代物では無いよな，と個人的には思ってます．
