プログラム理論特論 第８回 亀山幸義 [email protected] 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)の値 は何でも良い 抽象データ型の有用性 抽象データ型は「（外部）仕様」、具体的なデータ型は「実装」 抽象データ型 具体的なデータ型 実装方法を外から見ることができる meibo型データにおいて、「”Nakajima” の次に “Ito” が登録されてい るかどうか」を知ることはできるか？ ソフトウェアの段階的開発 stepwise refinement 記述された型情報、等式は外から見え、それ以外のこと（その抽象データ 型をどう実装しているか）は見えない[情報の隠蔽, information hiding] 最初に、抽象データ型を用いてアルゴリズムを設計し、 次に、これを具体的なデータ型で置き換える ソフトウェアの保守（更新）において 同じ抽象データ型を満たす、より高速のデータ型に置き換えることが 可能（ソフトウェアの性能向上） 大規模ソフトウェアの分散開発 ソフトウェア部品の再利用 抽象データ型の理論[参考] 等式のみで記述されている場合、抽象データ型を満 たす「最も一般的な（具体的な）データ型」が存在する ことが保証できる。[initial algebra, 始代数] 最も一般的 OBJなどの言語 では、ADTを書 けばそのまま 具体的な定義 と思って実行し てくれる 抽象データ型を満たす 具体的なデータ型 ADTからオブジェクトへ オブジェクトは、ADTの考え方に影響されて いる しかし、ADTと同じではない。 クラスの定義には、「具体的な実装方法」も記述 されている。 さらに、JAVA言語などでは、「外に見せるもの」 「外に見せないもの」を細かく指定できるように なっている。 継承inheritanceとサブタイピング 一番上の クラス Pointクラス ColoredPoint クラス ○○ColoredPoint クラス ○○Point クラス 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日は休講です。
© Copyright 2025 ExpyDoc
