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

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

1 プログラム理論特論 第８回 亀山幸義 kam@is.tsukuba.ac.jp

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

21 サブタイピングの例 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}

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

23 例：Pointクラス

24 例：ColoredPointクラス

25 例：ColoredPointクラス

26 例：ColoredPointクラス

27 例

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

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

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