プログラム理論特論第３回亀山幸義 [email protected] http://logic.is.tsukuba.ac.jp/~kam/progtheory 型のないλ計算（復習）  「関数」の概念（のみ）を定式化変数  関数の構成（λ式、λ抽象）  関数呼び出し（関数適用）  非常に小さなプログラム言語  構文論と意味論  理論的な性質  計算規則の健全性  非決定的な計算と合流性  停止性は不成立  計算の健全性  計算規則の健全性 Γ|- M：Λ かつ M⇒。。。⇒Nならば  Γ|- N:Λ である  プログラムを計算（式の変形）をしている途中でプログラムでないものが現れない（おかしな状態になったりしない）ことを保証  証明は、計算列の長さに関する帰納法  合流性  非決定的な計算と合流性  λ式Mからはじめて複数の経路で計算できる   （λx.x)((λｙ.y)z) しかし、どの経路も合流させることができる   M⇒。。。⇒N かつ M⇒。。。⇒L ならば、あるλ式Pがあって、  N⇒。。。⇒P かつ L⇒。。。⇒P とできる計算が停止すれば、その値（計算結果となるλ 式）は一意的である、どういう順番で計算してもよい  プログラムの最適化などに応用（定数のみを含む式などはコンパイル時に計算）  停止性  停止しない計算がある ω ≡ (λx. x x)(λx. xx) とすると  {} |- ω:Λ が成立する  ω ⇒ ω ⇒ … (無限ループ）   このようなωはいったいどういう計算をあらわしているのだろうか？答え１：無意味だからプログラムとして認めるべきでない  答え２：意味を与えるべき  型付きλ計算ーInformal Introductionー型付きλ計算とは？   型のないλ計算に型の概念を加えたもの型とは       データ型の概念（の一般化）データの種類；同じ操作ができるデータの集合基本型：Int （整数型）、real （実数型）、、、、型構成子： array, record, variable record, pointer (PASCAL言語）, array, struct, union, pointer (C言語) 基本型から型構成子を使って構成したもの計算機上の表現（実装）から考えると  同じサイズおよび同じ形式で表現できるデータの集合型の有用性  型の有用性プログラムがわかりやすくなる  プログラムにおけるバグが早期に発見できる     コンパイラが型の整合性を自動的にチェック整数型の変数に関数へのポインタを代入しようとする、等の誤りの発見型情報を用いて、より高速なコードを生成できる可能性がある  x+y という式は整数の場合と実数の場合とを見分けなければならないが、整数とわかっていれば機械語の加算命令をいきなり呼べばよい型の有用性（つづき）  型の有用性  型システムがきちんとできている場合、以下の性質が成立する    型検査をプログラム実行前にしておけば、プログラム実行中は型エラーは起きないこれが、この講義の眼目詳細は後で関数の型とは？  実は、関数のない場合の型の整合性検査はやさしい   本質的なのは、関数に対する型があるとき関数の型の整合性とは？ f(x)=x+1 という関数定義に対して、  f(“abc”) という呼び出しはエラー  f(f(3)) はOK  f(x,g)=g(x) という定義の場合は？  型付きλ計算ーFormal Introductionー構文  型(Type)   型定数 α, β, …は型（有限個または無限個） A,Bが型ならば、A→Bは型（型構成子は→だけ） A : Type α : Type B : Type A→B : Type 構文  変数   文脈    型Aごとに、変数 xA, yA, … がある（無限個の変数がある）変数の有限集合を文脈と呼び、Γ、Δ等であらわす例： Γ＝｛xα, y（α→β）→（α→β）} 判断    Γ|- M : A と言う形の表現 Γという文脈のもとで、項Mは型Aをもつλ式である項Mは型Aをもつλ式であり、その自由変数はΓである。構文  項の構成規則 Γ|- M : B Γ|-x : A (xA∈Γ) Δ|- λxA.M : A→B Δ=Γ－{xA} Γ|- M : A→B Γ|- N : A Γ|- MN : B 例題 Δ|- f : α→α Δ|- x : α Δ|- f : α→α Δ|- f x : α Δ|- f (f x) : α Γ|- λx. f (f x) : α→α {}|- λf. λx. f (f x) : (α→α) →(α→α) Γ={fα→α} Δ={fα→α, xα} 定義  型なしλ計算と同じ定義自由変数、束縛変数  束縛変数を一斉に名前換え  計算規則  代入  計算:例題 (λ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) ⇒λxint. (x+z)+z  型があると何が違うか？   型のないλ式Mに対して Γ|- M:A となるようなΓとA を見つけることはいつでもできるだろうか？答え： NO     前述のωに型をつけることはできない A=A→Bとなる型Aは（この範囲では）存在しない型付きλ計算は、ωのような式を排除型のないλ式であるかどうかの判定は容易であったが、型がつけられるかどうかの判定は容易とは限らない（考える必要がある）型の整合性の検査  型検査入力：Γ,M,A  出力：Γ|-M：A が成立するかどうかの情報   型推論入力：型がつくかどうかわからない式M  出力：Γ|-M：AとなるΓ、A が存在するかどうかの情報と、存在する場合はそのΓとA  型検査や型推論が自動的にできることが、望ましいプログラム言語としての必要条件  型推論が自動的にできれば、型検査も自動的にできる  型検査  単純型付きλ計算の体系に対して、型検査のアルゴリズムが存在する入力：Γ, M, A  出力：Γ|-M：A が成立するかどうか   Mの構成に応じて場合わけをすればよい  その際に、定まっていない型をあらわす型変数を導入する必要がある型推論  単純型付きλ計算の体系に対して、型推論のアルゴリズムが存在する入力：型がつくかどうかわからない式M  出力：Γ|-M：AとなるΓ、A が存在するかどうかの情報と、存在する場合はそのΓとA  次回までに考えてください式Mが与えられたとき、Γ|-M:Aが成立するΓ、 Aはいくつあるか？  たくさんあるとき、それらをうまく表現する方法はあるか？  Mが与えられたとき、その、うまい表現を計算するアルゴリズム（型推論アルゴリズム）は？ 