プログラム理論特論 第８回 亀山幸義 kam@is.tsukuba.ac.jp http://logic.is.tsukuba.ac.jp/~kam/progtheory

中間レポートについて 必ず返事します。５日以上たって返事がこないときはもう一度メイルしてください。 書式上の問題がいくつか散見されました。 ６月２日１７：００までに到着したレポートについては受理した旨の返事をメイルしました。 それ以降も順次メイルします。 書式上の問題がいくつか散見されました。 「テキスト、PS, PDFのどれか」と指定しているのにWORDで送ってくる 学籍番号と名前をレポートに冒頭に書かない（メイル自身の署名とは別に、レポートのファイルにも名前を書くのは当然） メイル本文に、何の断り書きもなく、いきなりレポートが添付されている。（当然、どの授業の何というレポートを提出しようとしているか、書くべき。書類を誰かに郵送するときには、必ず「送り状」をつけるべきであるのと同様） ただ、中間レポートの採点で問題にすることはありません。 レポートの解答等は後に web page　に掲載します。

今日のあらすじ 今回： オブジェクト指向言語の型システム 抽象データ型 6月10日は休講です。 次回は6月17日です。

Pointクラスのオブジェクトたち ｙ （３，５） （－１，２） （１，１） ｘ

ColoredPointクラスのオブジェクトたち ｙ （３，５） （－１，２） （１，１） ｘ

オブジェクト指向 Object-Oriented 制御中心ではなくデータ中心の記述 プログラムは、手続きや関数の定義の集まりではなく、データ定義の集まり 特徴 情報の隠蔽、カプセル化 クラスの定義で列挙された操作関数（メソッド）以外では、オブジェクトの内部構造をさわることはできない 継承：プログラムの再利用 Pointクラスの定義を利用してColoredPointクラスを定義する サブタイピング Pointクラスのオブジェクトを引数にとる関数には、ColoredPointクラスのオブジェクトも適用できる self/super　を用いた再帰呼び出し

抽象データ型 「普通」のデータ型（具体的なデータ型、抽象データ型でないデータ型） この講義でこれまで対象としてきたデータ型 どのように型を構成するかを具体的に指定することによって、データ型を定める。 例：　real ×(int→ string) 型の構成方法から自動的に以下のことが定まる その型をもつデータ（プログラム）をどうやって構成するか　　例　MとNから（M,N)を構成する その型をもつデータをどうやって使うか　例　(M,N)からその left　や right　をとる

抽象データ型 Abstract Data Type, ADT 型をどのように構成するか、ではなく、その型を持つデータをどうやって構成するか、どうやって使うかを定める [逆転の発想] データ型の実現ではなく、データ型の仕様

例：「学生名簿」データ型 具体的データ型 学籍番号と氏名のペアをリストにしたもの 学生を一人追加、学籍番号に対応する学生の氏名を探す

例：「学生名簿」データ型 抽象データ型 学生名簿型のデータには以下の操作だけを使う 空の学生名簿を作る new 学生を一人追加 add 学籍番号に対応する学生の氏名を探す assoc

例：「学生名簿」データ型 具体的なデータ型と抽象データ型の関係 具体的なデータ型は、抽象データ型の条件（仕様）を満たす。 抽象データ型の条件を満たす具体的なデータ型の構成方法は、ここで与えたものに限らない。

例：「スタック」抽象データ型 スタックは、new, push, pop　操作と、スタックトップの要素を知る関数、スタックが空かどうか知るための関数が備わっているデータ構造 これ以外の性質は一切 仮定しない pop(new)、top(new)の値 は何でも良い

抽象データ型の有用性 抽象データ型は「（外部）仕様」、具体的なデータ型は「実装」 記述された型情報、等式は外から見え、それ以外のこと（その抽象データ型をどう実装しているか）は見えない[情報の隠蔽, information hiding] 具体的なデータ型 実装方法を外から見ることができる meibo型データにおいて、「”Nakajima”　の次に　“Ito”　が登録されているかどうか」を知ることはできるか？ ソフトウェアの段階的開発 stepwise refinement 最初に、抽象データ型を用いてアルゴリズムを設計し、 次に、これを具体的なデータ型で置き換える ソフトウェアの保守（更新）において 同じ抽象データ型を満たす、より高速のデータ型に置き換えることが可能（ソフトウェアの性能向上） 大規模ソフトウェアの分散開発 ソフトウェア部品の再利用

抽象データ型の理論[参考] 等式のみで記述されている場合、抽象データ型を満たす「最も一般的な（具体的な）データ型」が存在することが保証できる。[initial algebra, 始代数] 最も一般的 OBJなどの言語では、ADTを書けばそのまま具体的な定義と思って実行してくれる 抽象データ型を満たす 具体的なデータ型

ADTからオブジェクトへ オブジェクトは、ADTの考え方に影響されている しかし、ADTと同じではない。 クラスの定義には、「具体的な実装方法」も記述されている。 さらに、JAVA言語などでは、「外に見せるもの」「外に見せないもの」を細かく指定できるようになっている。

継承inheritanceとサブタイピング 一番上の クラス Pointクラス ColoredPoint クラス ○○Point ○○ColoredPoint f: Point → int　 f(x)　の　ｘ の位置に 書けるオブジェクトの クラスは？ x: ColoredPoint f: Point→int から f(x): int を導けるようにしたい

OO言語を型理論で表現・理解する OO言語 型理論 クラス レコード型 オブジェクト レコード型をもつ項 メソッド 関数 継承 サブタイプ

OO言語の型理論：レコード型

ＯＯ言語の型理論：サブタイピング１

ＯＯ言語の型理論：サブタイピング２

サブタイピングの例 int ≦ real と仮定する int →int ≦ int →real {x:int,y:real,z:real} ≦ {x:int,y:real,z:real} real→int ≦ int→int real→int ≦ int→real ! int→int　と　real→real　の間に≦関係は成立しない {x:int,y:int,z:int} ≦ {x:int} {xy:{x:int,y:real}, z:int} ≦ {xy:{x:real,y:real},z:real}

例（の準備） 要素を1つしか持たない型 Unit 要素の値に意味がないときに使用する 0引数の関数を、1引数の関数とみなしたいとき print文を、関数とみなしたいとき Unit型はレコード型の一種とみなすこともできる。Unit =｛｝

例：Pointクラス

例：ColoredPointクラス

例：ColoredPointクラス

例：ColoredPointクラス

例

OO言語の型理論 型付きラムダ計算に、レコード型とサブタイピングを加えた体系 型の健全性定理は成立する 型推論は困難

OO言語の型理論 ここで述べた方法は、基本的な仕組みのみ定式化した 副作用をもたない部分に限定 サブタイピングと継承の違い 代入文を定式化していないので、get_x などのメソッドの中身を項として表現できなかった サブタイピングと継承の違い 型情報が失われることがある moving_color_point の例 継承した側で、メソッドの中身を書き換えることができる その場合、どのメソッドが適用されるべきかは型情報（静的な情報）だけではわからない。－＞　型を動的に決める必要がある

次回（以降） 次回（6月17日、6月24日） やり残した事 講義のまとめ 最終レポートの出題 6月10日は休講です。