情報科学概論 Ⅱ プログラム言語と型システムメタプログラミング 亀山幸義 http://logic.cs.tsukuba.ac.jp/~kam 今日の話題 1. プログラム特化とは 2. プログラム特化の技法 3. メタプログラミング言語 1 2 べき乗の関数 ( 定義 ) 1. プログラム特化とは power(x, n) = x if n=1 x * power(x, n 1) if n>1 power (5,3)=5*power(5,2) =5*(5*power(5,1))=5*(5*5)=125 3 4 べき乗の関数 (C 言語 ) int power(int x, n) { if (n == 1) return x; } else return x*power(x, n 1); べき乗の関数 (in OCaml) 関数型言語 OCaml プログラム = 関数 ( または 部分関数 ) 変数の宣言 ( 型宣言 ) が不要 5 6 1
べき乗の関数 ( 問題 1) べき乗の関数 (12 乗 ) if n=1 then x let power12 x = x*x*x*x*x*x*x*x*x*x*x*x 問題 1: 様々な x に対して その 12 乗を計算したい どうすれば効率的に計算できるか? 7 (power12 x) は (power x 12) より高速 1. 関数呼出しがない 2. 条件式 (if) や比較 (n=1) がない 3. 引数 nの値を覚えるためのメモリも不要 8 べき乗の関数 ( 問題 2) プログラム特化 program specialization if n=1 then x let power12 x = x*x*x*x*x*x*x*x*x*x*x*x 問題 2: power 関数と n=12 という情報から power 関数 一般的なプログラム 入力データ power12 関数 特化されたプログラム 入力データ n=12 x=2 実行結果 4096 power12 関数を自動的に得る方法は? 9 10 特化の方法 (1) 特化の方法 (2) プログラム特化における仮定 n の値 : この時点で分かっている x の値 : この時点では分からない n のみに依存した計算 (x に依存しない計算 ) は 実行する 11 12 2
特化の方法 (3) 特化の方法 (3) n のみに依存した計算 (x に依存しない計算 ) は 実行する n のみに依存した計算 (x に依存しない計算 ) は 実行する 13 14 特化の方法 (4) n のみに依存した計算 (x に依存しない計算 ) は 実行する 特化の方法 (5) 赤色 : 今 できる計算 ( 静的 ) 青色 : 後に残す計算 ( 動的 ) 15 16 べき乗関数の特化 power の再帰呼び出しも赤色 ( 静的 ) とする ただし 関数の色分けはそう単純にはできないので これは暫定的なもの ( 後述 ) 17 べき乗関数の特化 power x 12 if 12=0 then 1 else x * (power x (12-1)) x * (power x 11) x * (x * (power x 10))... x*x*x*x*x*x*x*x*x*x*x*x 18 3
特化された関数の利用 let power12 x = x*x*x*x*x*x*x*x*x*x*x*x power12 2 4096 power12 3 531441 特化されたプログラム 1. 実行性能が高い ( 高速 低メモリ ) 2. 特定のケースにしか使えない プログラム特化 ( 部分計算 ) power 関数 一般的なプログラム 記号計算 プログラム特化器 入力データ power12 関数 特化されたプログラム 入力データ n=12 x=2 実行結果 4096 19 20 プログラム特化はメタプログラミングの一例 メタプログラム プログラムを入力として受け取ったり プログラムを生成して返したりするプログラム 2. プログラム特化の技法 メタプログラムの例 コンパイラ インタプリタ 構文解析器生成プログラム 実は我々の身の回りにあふれている 21 22 特化の方法 = 赤青の塗り分け? 赤色 : 今 できる計算 ( 静的 ) 青色 : 後に残す計算 ( 動的 ) 特化の方法 プログラム塗り分け -map 関数の例 - let inc x = x + 1 ;; map inc [1; 2; 3] ;; [2; 3; 4] map inc [10; 20; 30; 40; 50] ;; [11; 21; 31; 31; 51] 23 24 4
特化の方法 プログラム塗り分け -map 関数の例 - map func lst に対する特化の可能性 1. lst は動的 2. lst の要素は動的だが 長さは静的 3. lst は静的 (i) func は すべての可能性を プログラムに対する 2 色の塗り分けでは表現できない 特化の方法の 1 つ = 型の塗り分け 10: 整数型 (int) abc : 文字列型 (string) [1; 2; 3] : 整数のリスト の型 (int list) xi : int のとき [x1; x2; x3] : int list xi : int のとき [x1; x2; x3] : int list それ以外に lst : int list 25 26 型システム (1) power : int int int, x : int, n : int のもとで n-1 : int power x (n-1) : int if n=1 then x else : int 型システム (2) e1 : int e2 : int e1 - e2 : int n : int 1 : int n-1 : int 27 28 型システム (3) f : a b f e : b e : a power : int (int int) x : int power x : int int power x n : int n : int 型システム (4) power : int int int, x : int, n : int if n=1 then x else x * (power ) : int 29 30 5
型推論 (1) プログラム ( 型についての情報なし ) から プログラム全体の型を推論しつつ 型が整合するかの検査をすることを型推論 (type inference) という 型推論 (2) 型推論アルゴリズムは 主に 関数型言語で発展してきた Hindley-Milner (Damas-Milner) の型推論アルゴリズム ML 言語の中核部分に対する完全に自動的な型推論を行う 多くのプログラム言語の型推論の基礎 31 32 プログラム言語と型システム 型の整合性を静的に ( プログラム実行前に ) チェックする エラーを 早い段階で 発見することができる ( ある種の信頼性の保証 ) 33 ML の型推論 let rec f x = f (f (f (f (x+1))))) f : int -> int このページは ML の型推論がすごい! と言いたいための例です 詳細は今理解する必要はありません (* n 回適用した f(f(f( f(x) ))) を計算する *) Let rec iter f n x = if n = 0 then x else f (iter f (n-1) x) iter : (α -> α) -> int -> α -> α (* f と g を関数合成する *) let compose f g x = g (f x) compose : (α->β) -> (β->γ) -> (α->γ) 34 色付きの型システム (1) power : int int int x n 返り値 色付きの型システム (2) e1 : int e2 : int e1 - e2 : int e1 : int e2 : int e1 - e2 : int 35 36 6
色付きの型システム (3) f : a b e : a f @ e : b f : a b e : a f @ e : b 色付きの型システム (4) power : int (int int) x : int power @ x : int int n : int (power @ x) @ n : int a,b は赤でも青でもよいが 色が一貫していなければならない 37 38 プログラム特化の技法 型に色を付ける あとは 通常の 型システム上の型推論を行う ( 赤い int と青い int は別の型とみなす ) 3. メタプログラミング言語 それだけでよい 関数型言語と型システムを基礎として プログラム特化 ( および 一般のメタプログラミング ) は発展してきた Lisp/Scheme, MetaOCaml, template Haskell 39 40 メタプログラミングのための言語 マルチステージプログラミング言語 MetaOCaml else.<.~x *.~(power x (n 1)) >. power : int code int int code int int int 41 MetaOCaml プログラミング power.<5>. 12.<5 * 5 * 5 * * 5>. power.<x>. 12 エラー ( 変数や型整合性のチェック ).<fun x ->.~(power.<x>. 12)>..<fun x -> x * x * * x>. let f = run.<fun x ->.~(power.<x>. 12)>. In f 2 4096 42 7
メタプログラミング言語 プログラム言語と型システム else.<.~x *.~(power x (n 1))>..<1 + 2>..< 1 + 2>. ( コード生成 ) let x =.<1+2>. in.<.~x * 3 >..< (1+2) * 3 >. ( コード合成 ) run.< 1 + 2> 3 ( コード実行 ) 43 型の整合性を静的にチェックする let rec power_gen x n = else if even(n) then.<square.~(power_gen x (n/2))>. else.<.~x *.~(power_gen x (n-1))>. power_gen.<2>. 5 =.<2*(square (square 2)>. MetaOCamlにおいては プログラム生成器の信頼性だけでなく 生成されるプログラムのある種の信頼性を プログラム生成前に保証する 44 メタプログラミング言語の応用例 メタプログラミング言語の応用例 領域特化言語 (DSL) の処理系 ( インタプリタ ) の高速化 [Taha et al. 2004] Taha らの例 : DSL= 小さな関数型言語 MetaOCaml で記述したインタプリタを ステージ化 たとえば 階乗計算プログラムで約 7 倍の高速化 インタプリタ を 階乗計算プログラム に特化した 45 数値計算ライブラリの保守性の向上 [Carette et al. 2005] Maple( 数値計算パッケージ ) における ガウスの消去法アルゴリズム の実装 なんと 30 種類以上も ほとんど同じアルゴリズムの実装が はいっていた 同じアルゴリズムだが 行列要素が実数か複素数か など様々なパラメータによって ほんの少し違う実装たち プログラム特化の形で書き直した 人間が保守するのは 1 つのアルゴリズム実際にユーザが使うのは特化された 30 通りのプログラム 46 メタプログラミングの研究 亀山らの研究 MetaOCaml の型システムで安全性が保証されているのは 純粋な関数型言語の部分 ( コア ) のみ実際には副作用がたくさんある ref 型 ( 書き換え可能な変数 状態 ) 制御 (exception, 継続操作 ) 入出力 副作用を持つメタプログラミング言語に対する安全性 信頼性の確保 ( 型システムの設計 実装 ) 47 メタプログラミングの研究 理論的な安全性の保証 プログラムを実際に生成する前に おかしなプログラムが生成されないことを保証したい プログラミング技法プログラム生成における効率化技法の取り込み 現実への応用 高性能計算 ( 行列計算 隠れマルコフモデルのアルゴリズム レイトレーシングなど ) における プログラム生成を系統化 48 8
まとめ 今日の話題 プログラム特化 ( 部分計算 ) メタプログラム ( プログラムを作るプログラム ) プログラム言語の研究 保守性や拡張性と 実行効率の両立 安全性や信頼性の保証 型システムと関数型言語 49 9