プログラム意味論を学ぶ意義
偉そうな事を書いていますが、私はプログラム意味論というのは全く分かりません。
ただ、以前"Semantics with Applications"という本をやる事が無かった時期に買って、これは真に何もやってない今読むチャンスなんじゃないかと思ったわけですが、こいつがどうもプログラム意味論というのを語っている本らしいです。
なのでまぁ正体不明の相手の事を英語で語られても意味分かるまいと思って取りあえずググってみるとwikipediaが出て来ました。
プログラミング言語の意味と計算モデルに関する厳密な数学的研究領域である。
そうするとなんて言うか、何で"数学的に"やるんだろうかとか考えてしまうわけです。表現、記述するのに十分に強い(??)とかっていう事なんだろうかと。
そこに何が在るのかを想像してみる事にします。
まず、私は構文解析は知ってます。こいつはプログラム(テキスト)をparseなりして形式的に定義とか処理し易い形(構文木)にする事だった気がするのですが。
少なくとも、実際にプログラミング言語を"実装"する場合は構文解析技法のお世話に成る事は多々あります。
じゃあ本題のプログラミング意味論は"実装"をも含むプログラミグ言語を"創る、創造"する為に必要なのだろうかっていう?
本当に必要かと考えると眉唾で、知らなくてもどうとでも成る気がします。感覚的に、とか既存のプログラミング言語からアイディアをパクって来るなどして、そのアイディアを上手く動く様に言語全体をどうにか形作るって事も出来ますし・・・。経験に基づく定義って事ですかね。
プログラム意味論を考えてないのに動くのは実は偶然なのか、考えなくても動くのかは分からないけど・・・。
で手元の本(横内寛文著 プログラム意味論)を見てると形式的に意味を定義するとか書いていて、そもそもこの「形式的」っつーのが混乱の元なんじゃないか、とか。
確か形式的というのは、上手く定義されていて、曖昧でない、とかそういう意味だったと思うのですが、もうこの時点で私の頭はダメだとして。
http://www.chimaira.org/docs/FormalReasoning.htm
ただまぁ、「あるプログラム言語について形式的に意味を定義する」意味はあるのかと考えるとちんぷんかんぷんに成ります。
形式的な定義手法に親しむ事は、プログラム検証とかモデル検査をやる時に非常に役に立つのでは無いかと妄想するのだけどプログラム意味論そのものには意味があるんだろうか??と頭に戻って来てしまった気が。
土台的なものであって、無くては成らないが単体では意味を捉えにくいとか、そういう事なんですかねぇ。
なんとなく掴めたかもしれない
http://twitter.com/ranha/status/1236654250
http://twitter.com/ranha/status/1236659698
http://twitter.com/ranha/status/1236662008
http://twitter.com/kinaba/status/1236683521
http://twitter.com/kinaba/status/1236689501
言語を作る側としては
コメントで書いてもらった通りになるんですが、理論/研究的成果を実際に取り入れる事は非常に重要な事だと思うのでそれは素晴らしい事だと思います。
新しく持ってくる部分が、今の意味論を崩す(??)事が無いかっていう事を調べるのも実装してからだとアレでしょうし。
まだあると思うのですが、ひとまずこれで私は満足出来る理由付けになります。
言語を使う側
この場合の"使う"というのは、ごく単純にその言語をツールとして使うという立場では無いと思います。
例えば検証、証明をその言語に対して行うという時。その場合は意味論が定義されていると嬉しい筈です。
そう直感的に思ったのは、XQueryのFormal Semanticsを見ていた時です。
形式的に記号を用いて十分な定義をしてやる事で実際にコードを"見なくても"済むっていう。もっと言うと、実装の時に湧き出たバグに苛まれなくても良いと。
どうでも良い所は抜きにして、本質的な所を議論する事が出来る。これは素晴らしい事なんじゃないでしょうか。
検証の方はSPINをちょびっと、証明の方はCoqとかAgdaをちょびっと弄った事があるぐらいですがその時には私は意味論を感じる事は出来ませんでした。
しかし、その対象とする言語から曖昧さを取り除く段階で意味論があると嬉しく、更に対象言語の意味論が存在する場合それを適切に移植してやることが元の言語を最大限尊重するという事に成ると思いますし、正しい検査/証明を行うというソレ自体であるとも思うのです。
ただ、私が足がかりとして乗り込むには具体例である検証、証明から行くと良いのでは無いかなとか思う次第です。
オススメしてもらえたSemantics with Applicationsは広く浅くのスタイルの様なので今の私には供給過多の様な気もしますが。
