プログラム理論特論 第７回 亀山幸義 [email protected] http://logic.is.tsukuba.ac.jp/~kam/progtheory 前回 前回：型付きラムダ計算の拡張 直積、リスト 多相型（導入のみ） 今回：型付きラムダ計算の拡張 多相型（続き） サブタイピング、レコード型 型システムの拡張１ーリスト リストのプログラミング 基本的な操作関数 nil あるいは [ ] 空リスト cons(M, L) リストＬの先頭に要素Ｍを追加する head(L) リストＬの先頭要素 tail(L) リストＬの先頭要素を取り除いたリスト empty?(L) リストＬが空リストであるかどうか？ head(nil)やtail(nil)の値がどうなるかはここでは気にしないこ とにする（本来ならば、エラーにすべき） 省略形 cons(a, cons(b, cons(c, nil))) を [a, b, c] と書く。 head([a,b,c]) = a, tail([a,b,c]) = [b, c] リストのプログラミング リスト２つの連結 append と リストの反転reverse リストのプログラミング appendと reverseの計算 リストのプログラミング appendを 型付きラムダ計算で記述すると。。。 リストのプログラミング appendの型は多相型 リストのプログラミング リストの長さlength, ２つのリストの併合merge リストのプログラミング リストを使ったQuick Sort リストのプログラミング リストを使ったQuick Sort リストのプログラミング qsort を「less-thanをもらって sortを行う関数」として 定式化したら。。。 多相型の効用 一般的なqsortの利用 データを順番に並べて保管したい（e.g. 学生の成績） データは、いくつかの性質の記述からなる。 学籍番号、英語の成績、算数の成績 種々の変更 ある時、データの形式が変わった 比較基準が変わった １００点満点のデータがＡ，Ｂ，Ｃ，Ｄの４段階評価になった ＴＯＥＩＣと情報処理技術者試験の点数もいれることにした ８０点以上の科目の個数で並べていたが、Ａの個数で比較することになった それでも、qsortアルゴリズムには変更がないので、プログラムを書き 換えたり、コンパイルしなおさなければいけないのだろうか？ 解決策 型のないプログラム言語、いい加減な型システムを持っているプログ ラム言語では問題ない（が、プログラムの安全性、保守性が悪くな る。） 型のあるプログラム言語では多相型 ＭＬ言語における多相型 ＭＬでは多相型関数は、let宣言（あるいは、関数定 義）に伴ったときのみ、定義できる。 ＭＬ言語における多相型 ＭＬでは多相型関数は、let宣言（あるいは、関数定 義）に伴ったときのみ、定義できる。 １９８０年代の話です。 （新しい）プログラミング・パラダイム 新しいプログラミング・スタイルの記述 論理型 logic programming （制限された一階）述語論理の定理証明手続きをそのまま プログラムの実行と見なそう、という立場 関数型 functional programming Prolog, GHC, ... Lisp/Scheme, ML, ... 「プログラム＝関数＝ラムダ式」 オブジェクト指向 Object-Oriented Programming SmallTalk, ABCL, .. （今ではもちろんＪａｖａ など） オブジェクトを中心にプログラムを組み立てる 論理型プログラム言語のその後 もう終わった（基本的なスタイルは確立された） e.g. ＩＣＯＴプロジェクト 広い範囲で使える実用的な言語としての地位は得られな かった 特定の分野では使える 基本的なスタイルからの脱却 制約（Constraint)プログラミング いろいろな問題を制約の集合として記述し、問題解決を制約解消 に帰着する 型推論も、α＝β→γなどの制約の集合を解く問題と考えられる 帰納学習との関連： 帰納論理プログラミング f(3)=9, f(5)=25, f(6)=36 から ｆ を求める問題 関数型プログラム言語のその後 まずまずの成功 型システムと結びついて、プログラム言語の基礎的な研究はほとんど すべて関数型プログラムに基づいて行われるようになった 他のパラダイム（オブジェクト指向など）も関数型をベースとして理解 する方向 e.g. この授業 実用性は？ 今のところ、成功しているとはいいがたい（教育、研究用の言語にとど まる） 日々のプログラムをML, Lispで書いている人は研究者ぐらい？ 現在のコンピュータのアーキテクチャ上ではＣ言語などで書いた方が高 速に実行される ヨーロッパでは、高い信頼性を持ったプログラムを欲するPhilipsなど のメーカーがErLang言語などを使いはじめている アプリケーション・プログラムのためのプログラム言語ではなく、システ ムの背後にひそむプログラム（コンパイラ、プログラムの検証システム etc.) を書く用途には適している オブジェクト指向プログラム言語 のその後 実用的には大成功 プログラム言語の主流 一方で、、、 プログラムの信頼性の向上のためにはまだまだ考えなけ ればいけないことが多い 意味論や形式的取り扱いが（関数型や論理型に比べて）不透明 な部分がある オブジェクト指向言語（ＯＯ）における オブジェクト Object ありふれた例だが。。。 ｙ ２次元平面上の１点をあらわす （３，５） ｘ座標、ｙ座標を知りたい あるベクトルにそって動かしたい ｘ オブジェクト指向言語（ＯＯ）における オブジェクト Object ｙ （３，５） ｘ オブジェクト Object ところが、色のデータも 持たせたくなった ｙ （３，５） ｘ オブジェクト Object Point も ColoredPoint も、get_x や move という 関数（ＯＯ言語ではメソッドと呼ばれる）が使えるこ とにはかわりがない。 このf をＣｏｌｏｒｅｄＰｏｉｎｔに適用するのは、エラーだ ろうか？ オブジェクト Object ＯＯ言語： オブジェクト いくつかの（０個以上の）データと、それに対する操作関数（メソッ ド）から構成される そこに列挙された操作関数以外で内部データをさわることはでき ない[情報の隠蔽 これが大事] クラス：オブジェクトを生成するための「ひな形」 型理論でＯＯ言語を理解するためには クラス＝型、オブジェクト＝プログラム（項） オブジェクトは、いくつかのデータおよび関数（これもλ計 算では単なるデータ）から構成される。ただし、名前がつ いている。 ＯＯ言語の型理論 レコード型 名前つき、順番のない直積 Subtyping 来週 ＯＯ言語の型システムの詳細 中間レポートの解説 時間があれば、コントロールオペレータの型理論 名前つき、順番のない直積
© Copyright 2024 ExpyDoc
