関数型言語Part IV

【表示的意味論】　http://kaiunix.cs.shinshu-u.ac.jp/Lesson/ProgLangT/2004/denotationalsemantics.html

表示的意味論ではプログラムに対して、既定義の数学オブジェクトを対応付ける
(プログラムオブジェクトから数学オブジェクトへの変換を定義する) 事により意味を定義する。
具体的にはここのプログラムオブジェクトに対して意味関数を対応付ける。
　　　　 ┌──────┐
　　　　 │　プログラム.　│
　　　　 └───┬──┘
　　　　 　　　　　　│
　　　　 　　　　　　│　　意味関数
　　　　 　　　　　　│
　　　　 　　　　　　↓
　　　　 ┌──────┐
　　　　 │数学的な表示│
　　　　 └──────┘

具体的には構文要素に対応付けられる意味関数の集合として定義する。

　Ｍ ： Ｔ → Ｄ

Ｔは構文要素であり、Ｄは表示の集合であり、意味ドメインと呼ばれる。

【操作的意味論】http://kaiunix.cs.shinshu-u.ac.jp/Lesson/ProgLangT/2004/operationalsemantics.html

プログラムの実行結果を判定できるような仕組みを与える事で意味を定義する。
すなわちプログラムを解釈実行できるようなオートマトン(自動機械)を定義する事にな る。
しかしながら何らかの意味では、実行すると言う事で、実装等の関わりが強くな りすぎるという欠点を持つ。

　　　　 ┌──────┐　　　　　　　　　　　　┌──────┐
　　　　 │　プログラム.　│　　　　　　　　　　　　│　　　 入力 　　│
　　　　 └───┬──┘　　　　　　　　　　　　└───┬──┘
　　　　 　　　　　　└───────┬───────┘
　　　　　　　　　　　　　　　　 　　　　　　│操作的仕様に基づく解釈実行
　　　　　　　　　　　　　　　　 　　　　　　↓
　　　　　　　　　　　　　　　　 ┌──────┐
　　　　　　　　　　　　　　　　 │　 実行結果 　│
　　　　　　　　　　　　　　　　 └──────┘

一般には次のようなイメージになる。定義域をNとしてProgram pを実行する

　program_effect(p:Program, input:N): N* is
　　do
　　　result := instruction_effect(p.body, input, <>);
　　end

rを入力、fを内部状態として、命令iを実行する

　instruction_effect(i:Instruction, r:N, f:N*): N x N* is
　　do
　　　inspect i
　　　when Double_to_even then result := <2*r, f>
　　　.......
　　end

この様にプログラムをその構成要素に分割し、構成要素毎にどの様な動作をするかを定義する。
この様な定義であるので、必要以上に動作に依存してしま うと言う欠点がある。

【公理的意味論】http://kaiunix.cs.shinshu-u.ac.jp/Lesson/ProgLangT/2004/axiomaticsemantics.html

公理的意味論では意味をプログラムのセオリーとして記述する。
そしてセオリー の証明という作業を通じて、意味の正しさを確かめる。
セオリーは以下の３ つの要素から構成される

　　・構文規則
　　・公理
　　・推論規則

そして、プログラムαを次のような形式で表現する

　　　　　　　　　　　　　　{事前条件}α{事後条件}

これをpre-post式と呼ぶ。公理と推論規則はこのpre-post式を利用する。
この式は、事前条件が成り立っている(真である)という条件下でαを実行すると 事後条件が成り立つ、
と言う事を表現している。そして公理的意味論はこの 式を証明する(真偽を判定する)手段を提供している。
具体的にはαが文の列とするし、それをα1、α2、....、αnとすると、次のような式の列を順次証明する事になる

　　　　　　　　　　　　　　{事前条件1}α1{事後条件1}
　　　　　　　　　　　　　　{事前条件2}α1{事後条件2}
　　　　　　　　　　　　　　......
　　　　　　　　　　　　　　{事前条件n}αn{事後条件n}

ここで事後条件iは事前条件i+1と同じものである。
公理としては、プログラミン グ言語の各基本要素に対して、pre-post式を与える事になる。

---------------------------------------------------------------------------------------------

では例題のプログラミング言語の定義を考える。公理的意味論の場合も個々の命 令に対してpre-post式を定義する事になる

　{P(register,file)} Double_to_even {even(register) ∧ P(register/2 ,file)}

　{P(register,file)} Double_to_odd {odd(register) ∧ P((register-1)/2 ,file)}

　{P(register,file)} Halve {P(2*register ,file) ∨ P(2*register+1, file)}

registerは入力として与えられた変数であり、fileは実行環境における局所的な 値の集合である。またpre、postの条件におけるregisterとfileは各々 Double_to_evenの実行前と実行後の値を意味する。

--------------------------------------------------------------------------------

公理的手法はこの様に意味を定義するためのものとしてだけではなく、
プログラ ムの証明のための手段としても使われている。
すなわちプログラム全体を以下の様にpre-post式で表し、
プログラムが満たすべき条件を事後条件として、
この式を分割し、各式を証明する事により、
プログラムが正しいと言う事が 証明できた事になる、という物である

　　　　　　　　　　　　　　　{事前条件}プログラム{事後条件}

例えばa,b,cを入力として、それを係数とする二次方程式の解をx,yに求めるプログラムをＰとすると、
その証明のための式は次の様に書ける

　　　　　{a,b,cは任意の実数、但しb*b-4.0*a*c>0}P{a*x*x+b*x*c=0 AND a*y*y+b*y+c=0}

【意味論】http://kaiunix.cs.shinshu-u.ac.jp/Lesson/ProgLangT/2004/Semantics.html

２つの観点から、意味が明確に定められている必要がある。
プログラマの視点：自分の書いたプログラムがどの様な動作をするの かを正確に理解する必要がある。これが曖昧であれば、作成したプログ ラムの動作は実行によってしか確認できない
コンパイラ作成者の視点：プログラムに対してどの様な目的コードを 生成すればよいかを正確に理解する必要がある。これが曖昧であれば、同 じプログラムでもコンパイラによって動作が異なる可能性がある。
ユーザはコンパイラは全て正しくコンパイルすると考えているが、コンパイラの 作成者の立場から考えるならば、作成したコンパイラの正しさを何に基 づいてテストするのか？
例えば次のような命令列を考える

　x = 2;
　x = x++;

x++はxの値を評価した後、その値を１増やすと言う事であるので、...
このように自然言語だけによっていた場合、種々の曖昧性が生じる。この様に意味を正確に定義する事は重要であるが、定義の仕方によって次のよう な手法が考えられている
意味論について述べる前に理解するために必要となる数学 基礎について解説しておく。

　　・操作的意味論 >>8-9
　　・公理的意味論 >>10-11
　　・表示的意味論 >>7

本章では次の様な極めて簡単なプログラミング言語を例とする。
<Program> ::= PROGRAM <Instruction> END
<Instruction> ::= Double_to_even | Double_to_odd |
Halve | Print | <Compound>
<Compound> := COMPOUND <Instruction>* END

Double_to_evenは入力を２倍する。Double_to_oddは２倍して、１を足す。 Halveは半分にする。そしてPrintは値を表示する。プログラム例としては以 下の様なものがある。
PROGRAM
COMPOUND
Double_to_even; Double_to_odd; Havlve; Print
END
END

このプログラムに対して入力が１の場合、２を出力する。

>>7-13
長々とコピペご苦労だが、ようするに>>6ってことだろ？

>>14 頭のおかしい人、ｷﾀｰ
　　　　ｶﾜｲｿｳだから放置放置・・・

煽りは厳禁、頭のおかしい人はスルーでどぞー。

【プログラミング言語の意味論】http://kaiunix.cs.shinshu-u.ac.jp/Lesson/ProgLangT/2004/Semantics.html

では、意味はどの様に定義されるのか？

--------------------------------------------------------------------------------
【プログラムの正しさ】


構文と意味で述べたように「プロ グラムが正しい」という内容には種々のレベルがある。
しかしながら一般的 にはっきりしている事は、
正しいとは「何らかの形式で定められたルール、 条件に則っている」という事である。
逆に言うならば則っているルール を用意しない限り、正しい、正しくない、という議論は成立しない。
この様 な観点から、意味に関わるルール、条件を記述するものが意味論である。

--------------------------------------------------------------------------------

【意味とは】http://kaiunix.cs.shinshu-u.ac.jp/Lesson/ProgLangT/2004/Semantics.html


プログラミング言語の世界では意味とは一般には以下の様な物と考えられている。

　　　　　　　　　　　　　　　　　　　　 ┌───────┐
　　　　　　　┌──────┐　 │ プログラム又は.│　 ┌──────┐
　　　　　　　│実行前の状態├→│ プログラム要素.├→│実行後の状態│
　　　　　　　└──────┘　 │ 　　の実行　　　 │　 └──────┘
　　　　　　　　　　　　　　　　　　　　 └───────┘

プログラムの実行前にある状態(内部状態：プログラムが持つ変数の値の集合)にある時に、
実行後にどの様な状態になるか。普通は実行前の状態に基づいて実行後の状態を記述する。
例えば、変数ａの値を２倍にするプログラムであれば、実行後の状態は次の様に書ける。
正確にはａ以外の変数の値は変化していない事を記述する必要がある。

　実行後のａ＝実行前のａ＊２

ここで注意すべき事は実行後の状態の記述において、実行前の変数の値を利用すると言う事である。
そのためにａに対して実行前のａと実行後のａを区別する表記が必要となる。
意味とはこの様に各命令の効果を記述する物であるが、
プログラムは基本的な構成要素およびその組み合わせ規則からなる物と言える。
その観点から考えるならば、意味の記述は以下の２つのものの記述からなることになる：

1. 基本構成要素の意味
　 例えば++という演算子は何を意味するか
2. 組み合わせ規則の意味
　 例えば、IF C THEN S1 ELSE S2 というIF文はC,S1,S2の意味に基づき、どの様な動作をするのか？

【まとめ】http://kaiunix.cs.shinshu-u.ac.jp/Lesson/ProgLangT/2004/Semantics.html

1. 意味論の目的は次の２点である
　　1) プログラマにプログラムの一律で、曖昧性のない正しい解釈を提供する
　　2) コンパイラの作成者にプログラムの一律で、曖昧性のない正しい解釈を提供する
2. プログラムの意味は基本構成要素の意味と組み合わせ規則の意味からなる
3. プログラムの意味とは内部状態がどの様に変わるかの記述である
4. 意味は構文的に認識された対象に対してのみ考える事ができる
5. 意味が定義されているプログラミング言語で書かれたプログラムは、その意味を定義する事ができる