PowerPoint

プログラム理論特論
第９回
亀山幸義
[email protected]
http://logic.is.tsukuba.ac.jp/~kam/progtheory
中間レポートについて


すべて返事したつもりです。
レポートの解答等は web page に掲載しました。
講義のまとめー基礎編

型付ラムダ計算（Church流、Curry流）
型付け規則と計算規則
 型検査と型推論
 単一化アルゴリズムと型推論アルゴリズム
 型の健全性定理

講義のまとめー応用編


スローガン：いろいろなプログラム言語の型システム
は、型付ラムダ計算の体系の拡張と考えることがで
きる
拡張１：




拡張２


直積型
リスト型
（直和型） cf C言語のunion型
多相型 cf ML言語
拡張３


レコード型 cf C言語のstruct型、OO言語のクラス
サブタイピング cf OO言語におけるクラスの継承
講義のまとめー応用編の補足

いろいろな拡張で、「良い性質」は失われていない
のか？



個別のケースごとに確認しなければならない.
型検査、型推論アルゴリズムの存在： C, ML, Javaなどで
はOK
型の健全性定理: 多くの場合問題ないと信じられている
が、プログラム言語全体に対する健全性定理は証明され
てないことが多い.


ML言語で、多相型＋代入、あるいは、多相型＋例外機構、を入
れると、単純にやるとすぐに型の健全性がくずれてしまう
きちんとした foundation が必要
講義のまとめ

プログラム言語における型
型とは何か？
 型は必要なのか？
 型は有益なのか？

型の必要性１

コンピュータ上の表現形式からの必要性
あらゆるデータを２進数（あるいは１６進数）での
表現へ符号化する必要。
 どの符号化を選択したかを区別するタグとしての
型情報
 例：“AB 86 C9 BB”というデータは、EUCコードな
のかSJISコードなのかで表現しているテキストが
異なる
 例：“ff ff ff ff” は、整数か実数かで異なる。

型の必要性２

プログラムの記述における必要性

N. Wirth “Data Structure + Algorithm = Program”
どんな問題が与えられても、それを解くプログラ
ムを書くためにはデータ構造を適切に設計しなけ
ればならない
 データ構造（データの構成方法）としての型
 型の概念のないプログラム言語であっても、この
ような意味でのデータ構造（広い意味での型）は
必要

型の有用性（説明済み）

Documentation


Abstraction



a safe language is one that protects its own abstractions [Pierce]
Efficiency


コンパイラが型の整合性を自動的にチェック
整数型の変数に関数へのポインタを代入しようとする、等の誤りの
発見
Language Safety


大規模プログラミングにおけるモジュールのインタフェースの記述、
より抽象的なレベルのモジュールの記述
Detecting Errors


プログラムの意味がわかりやすくなる
型情報を用いて、より高速なコードを生成できる可能性がある
型システムの健全性
型とはなにか？
具体的（構成的）な定義

以下の４項目をきちんと定義すれば、型が１
つきちんと定まる
型の構成方法（および２つの型の間の同等性）
 その型を持つデータの構成方法
 その型を持つデータの使用方法
 その型を持つデータの計算方法

例：リスト型の定義
型とはなにか？素朴な定義

型とは



データの集合であって、
その集合の要素すべてに同じ操作（関数）が適用できるも
の
型と集合は違うのか？




型は集合の一種
すべての集合が型と見なせるわけではない
「整数の型」はよいが、「素数の型」は考えにくいのはなぜ
だろう？
あるデータがその型をもつかどうか機械的に（しかも普通
は短い時間で）判定できなければいけないｃｆ型検査、
型推論のアルゴリズムの存在
型とはなにか？素朴な定義の発展

型とは



データの集合であって、
その集合の要素であるかどうかがすぐに判定できるもの
「すぐに」とは？




プログラムを実行することなく
すなわち、静的に判定できるもの
静的：プログラムの論理構造
動的：プログラムの（計算としての）ふるまい
型＝プログラムの静的性質
「整数」「整数をもらって実数を返す関数」と
いった普通の型情報以外にも静的に記述し
たい性質はたくさんある
 さまざまな性質を表現する型システムを構築
して、『プログラムの実行前に型検査をパス
すれば、実行中にはずっと○○という性質が
保たれる』ということを保証する。（型システム
の健全性）
 Safety Property の保証

型システムの発展

拡張された型を用いたプログラムの静的解析

情報の機密度


「機密度の高い整数型」「機密度の低い整数型」などを
導入し、機密度の高い整数型の値を機密度の低い変
数に代入することがない、ということを型検査でチェッ
クする。
Java byte code verfier （昨年の講義資料を参照）

スタックの深さなど、単純な型情報以外のものも型とし
て表現して、型検査を行うことにより、「スタックを無限
に消費しない』等の性質を保証する
おわりに
今回の授業では、コントロールオペレータ、CPS
変換等はカバーできなかった（来年こそは。。。）
 レポートは７月７日締め切り。




電子メイルにて提出
テキスト、PS, PDF, WORD、日本語または英語
Subject欄に report-2 といれてください。

Download Report