PowerPoint

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