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