プログラム理論特論 第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 といれてください。
© Copyright 2024 ExpyDoc