関数型言語Part IV

1 名前：デフォルトの名無しさん [04/05/04 14:53] Lisp Scheme ML Haskell FP Mirranda など 関数型言語について話し合いましょう 関連スレ 関数型プログラミング言語ML pc3.2ch.net/test/read.cgi/tech/1012445015/ 関数型プログラミング言語Haskell pc3.2ch.net/test/read.cgi/tech/1013846140/ LISP Scheme Part6 pc3.2ch.net/test/read.cgi/tech/1031560687/ Emacs Lisp pc3.2ch.net/test/read.cgi/tech/1004551074/ 7 名前：デフォルトの名無しさん [04/05/04 15:04] 【表示的意味論】　kaiunix.cs.shinshu-u.ac.jp/Lesson/ProgLangT/2004/denotationalsemantics.html 表示的意味論ではプログラムに対して、既定義の数学オブジェクトを対応付ける (プログラムオブジェクトから数学オブジェクトへの変換を定義する) 事により意味を定義する。 具体的にはここのプログラムオブジェクトに対して意味関数を対応付ける。 　　　　 ┌──────┐ 　　　　 │　プログラム.　│ 　　　　 └───┬──┘ 　　　　 　　　　　　│ 　　　　 　　　　　　│　　意味関数 　　　　 　　　　　　│ 　　　　 　　　　　　↓ 　　　　 ┌──────┐ 　　　　 │数学的な表示│ 　　　　 └──────┘ 具体的には構文要素に対応付けられる意味関数の集合として定義する。 　Ｍ ： Ｔ → Ｄ Ｔは構文要素であり、Ｄは表示の集合であり、意味ドメインと呼ばれる。 8 名前：デフォルトの名無しさん [04/05/04 15:12] 【操作的意味論】kaiunix.cs.shinshu-u.ac.jp/Lesson/ProgLangT/2004/operationalsemantics.html プログラムの実行結果を判定できるような仕組みを与える事で意味を定義する。 すなわちプログラムを解釈実行できるようなオートマトン(自動機械)を定義する事にな る。 しかしながら何らかの意味では、実行すると言う事で、実装等の関わりが強くな りすぎるという欠点を持つ。 　　　　 ┌──────┐　　　　　　　　　　　　┌──────┐ 　　　　 │　プログラム.　│　　　　　　　　　　　　│　　　 入力 　　│ 　　　　 └───┬──┘　　　　　　　　　　　　└───┬──┘ 　　　　 　　　　　　└───────┬───────┘ 　　　　　　　　　　　　　　　　 　　　　　　│操作的仕様に基づく解釈実行 　　　　　　　　　　　　　　　　 　　　　　　↓ 　　　　　　　　　　　　　　　　 ┌──────┐ 　　　　　　　　　　　　　　　　 │　 実行結果 　│ 　　　　　　　　　　　　　　　　 └──────┘ 9 名前：デフォルトの名無しさん [04/05/04 15:13] 一般には次のようなイメージになる。定義域を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 この様にプログラムをその構成要素に分割し、構成要素毎にどの様な動作をするかを定義する。 この様な定義であるので、必要以上に動作に依存してしま うと言う欠点がある。 10 名前：デフォルトの名無しさん [04/05/04 15:15] 【公理的意味論】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式を与える事になる。 --------------------------------------------------------------------------------------------- 11 名前：デフォルトの名無しさん [04/05/04 15:17] では例題のプログラミング言語の定義を考える。公理的意味論の場合も個々の命 令に対して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} 12 名前：デフォルトの名無しさん [04/05/04 15:19] 【意味論】kaiunix.cs.shinshu-u.ac.jp/Lesson/ProgLangT/2004/Semantics.html ２つの観点から、意味が明確に定められている必要がある。 プログラマの視点：自分の書いたプログラムがどの様な動作をするの かを正確に理解する必要がある。これが曖昧であれば、作成したプログ ラムの動作は実行によってしか確認できない コンパイラ作成者の視点：プログラムに対してどの様な目的コードを 生成すればよいかを正確に理解する必要がある。これが曖昧であれば、同 じプログラムでもコンパイラによって動作が異なる可能性がある。 ユーザはコンパイラは全て正しくコンパイルすると考えているが、コンパイラの 作成者の立場から考えるならば、作成したコンパイラの正しさを何に基 づいてテストするのか？ 例えば次のような命令列を考える 　x = 2; 　x = x++; x++はxの値を評価した後、その値を１増やすと言う事であるので、... このように自然言語だけによっていた場合、種々の曖昧性が生じる。この様に意味を正確に定義する事は重要であるが、定義の仕方によって次のよう な手法が考えられている 意味論について述べる前に理解するために必要となる数学 基礎について解説しておく。 　　・操作的意味論 >>8-9 　　・公理的意味論 >>10-11 　　・表示的意味論 >>7 13 名前：デフォルトの名無しさん [04/05/04 15:20] 本章では次の様な極めて簡単なプログラミング言語を例とする。 <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 このプログラムに対して入力が１の場合、２を出力する。

---

---

[ 続きを読む ] / [ 携帯版 ]

read.cgi ver5.27 [feat.BBS2 +1.6] / e.0.2 (02/09/03) / eucaly.net products.
担当:undef