PowerPoint - tsukuba.ac.jp

プログラム理論特論
第３回
亀山幸義
[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ごとに、０個以上有限個の定数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α}
定義

以下の定義は配布資料を参照のこと
自由変数、束縛変数
 α同値（束縛変数を一斉に名前換え）
 代入
 計算規則

変数の自由な出現と束縛された出現

１つ１つの変数の出現は、
一番近いλで束縛されているか、
 どのλでも束縛されていない(自由である）か
のいずれかである。


束縛されている変数は、一斉に名前をかえて
も「同じ」λ式である

例： λ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は（この範囲では）存在しない
型付きλ計算は、ωのような式を排除
型のないλ式であるかどうかの判定は容易であった
が、型がつけられるかどうかの判定は容易とは限ら
ない（考える必要がある）

Download Report