プログラム理論特論 第3回 亀山幸義 [email protected] http://logic.is.tsukuba.ac.jp/~kam/progtheory 型のないλ計算(復習) 構文論と意味論 「関数」の概念のみを定式化 構文。。。どういう文字列が(正しく構成された)ラムダ 式であるか、を定める 意味。。。ラムダ式がどうふるまうか(計算するとどうな るか)を定める 変数 関数の構成(λ式、λ抽象) 関数呼び出し(関数適用) 非常に小さなプログラム言語 しかし、計算機で表現できるあらゆる関数を表現でき ることが知られている [Church’s Thesis, TuringCompleteness] 型付きλ計算 -Informal Introduction- 型付きλ計算とは? 型のないラムダ計算に型の概念を加えたもの 型とは? データ型の概念の一般化 同じ操作ができるデータの集合 具体的には‥ 操作とは何か? 基本型: int, real, etc. 型構成子: array, record, variable record, pointer (PASCAL言 語), array, struct, union, pointer (C言語) 基本型から型構成子を使って構成したもの 計算機上の表現(実装)から考えると 同じサイズおよび同じ形式で表現できるデータの集合 型の有用性 Documentation プログラムの意味がわかりやすくなる Abstraction 大規模プログラミングにおけるモジュールのインタフェースの記述 [Abstract Data Type] より抽象的なレベルのモジュールの記述 抽象的とは? 抽象=何かを捨て去ること 型の有用性 Detecting Errors コンパイラが型の整合性を自動的にチェック 整数型の変数に関数へのポインタを代入しようとする、 等の誤りの発見 型の有用性 Language Safety a safe language is one that protects its own abstractions [Pierce] unsafeの例 配列のサイズを超え てアクセスする 型の有用性 Efficiency 型情報を用いて、より高速なコードを生成でき る可能性がある x+y という式の計算 x,yが整数の場合と実数の場合とで異なるコード (機械語)を使わなければならない x,yが整数か実数かあらかじめ決められず、実行し た段階で決まる場合は、その都度、場合分けをす る必要がある。 最初から(実行前に)整数とわかっていれば機械語 の加算命令を使えばよい 型の有用性(つづき) 型システムの健全性 型システムがきちんとできている場合、型検査 をプログラム実行前にしておけば、プログラム 実行中に型エラーは起きない 関数の型とは? 実は、関数のない場合の型の整合性検査 はやさしい 本質的なのは、関数に対する型があるとき 関数の型の整合性とは? f(x)=x+1 という関数定義に対して、 f(“abc”) という呼び出しはエラー f(f(3)) はOK f(x,g)=g(x) という定義の場合は? 型付きλ計算 -Formal Introduction- 構文 型(Type) 有限個の型定数 例: int, real, bool 以下では α, β 等であらわす A,Bが型ならば、A→Bは型 (型構成子は→だけ) 一般の型を以下では、A, B であらわす A : Type α : Type B : Type A→B : Type 型の例 構文 変数 定数 型Aごとに、0個以上有限個の定数cAがある。 文脈 型Aごとに、変数 xA, yA, … がある(無限個の変数が ある) 変数の有限集合を文脈と呼び、Γ、Δ等であらわす 例: Γ={xα, y(α→β)→(α→β)} 判断 Γ|- M : A と言う形の表現 Γという文脈のもとで、項Mは型Aをもつλ式である 項Mは型Aをもつλ式であり、その自由変数はΓである。 構文 項の構成規則 Γ|- M : B 例題 Δ|- f : α→α Δ|- x : α Δ|- f : α→α Δ|- f x : α Δ|- f (f x) : α Γ|- λx. f (f x) : α→α {}|- λf. λx. f (f x) : (α→α) →(α→α) Γ={fα→α} Δ={fα→α, xα} 定義 以下の定義は配布資料を参照のこと 自由変数、束縛変数 α同値(束縛変数を一斉に名前換え) 代入 計算規則 変数の自由な出現と束縛された出現 1つ1つの変数の出現は、 一番近いλで束縛されているか、 どのλでも束縛されていない(自由である)か のいずれかである。 束縛されている変数は、一斉に名前をかえて も「同じ」λ式である 例: λf. f(λy.fy) と λg. g(λx.gx) は同じ 計算:例題 (λfint→int. λxint. f (f x))(λyint. y+5) ⇒λxint.(λyint.y+5)((λyint.y+5)x) ⇒λxint.(λyint.y+5)(x+5) ⇒λxint.(x+5)+5 int→int. λxint. f (f x))(λyint. y+x) (λf ⇒λzint.(λyint.y+x)((λyint.y+x)z) ⇒λzint. (z+x)+x 型があると何が違うか? 型のないλ式Mに対して Γ|- M:A となるようなΓとA を見つけることはいつでもできるだろうか? 答え: NO (λx.xx)(λx.xx)に型をつけることはできない A=A→Bとなる型Aは(この範囲では)存在しない 型付きλ計算は、ωのような式を排除 型のないλ式であるかどうかの判定は容易であった が、型がつけられるかどうかの判定は容易とは限ら ない(考える必要がある)
© Copyright 2024 ExpyDoc