スライド 1

Formative System Engineering
書き換え型プログラムの生成・検証
「左辺を右辺に書き換える」規則の集まりで構成される、抽象的なプログラム
プログラムの安全性の検証、効率の良いプログラムの自動生成等の研究の土台
書き換え型プログラム
x, xs は
変数
[] = 空リスト
x:xs = 先頭がx、残りがxs
であるリスト
例：
[1] = 1:[]
[1,2,3] = 1:(2:(3:[]))
dbl(0)
dbl(x+1)
sum([x])
sum(x:xs)
dup([])
dup(x:xs)
→
→
→
→
→
→
0
dbl(x) + 2
x
x + sum(xs)
[]
x:x:dup(xs)
プログラムの生成
sum([x])
dbl(2) →
→
sum([3,5]) →
dup([3,5]) →
→
dbl(1) + 2
dbl(0) + 2 + 2 → 0 + 2 + 2 → 4
3 + sum([5]) → 3 + 5 → 8
3:3:dup([5])
3:3:5:5:dup([]) → [3,3,5,5]
プログラムの検証
x + sum([])
規則の追加
sum([]) → 0
x
プログラムの実行例
x + 0
実行結果が一通りに定まるよう、
適切な規則を自動的に追加（完備化手続き）
生成・検証の両方において、既存の手法では
適切な戦略を指定する必要があり、使いにくい
プログラムがどのような入力に対しても満たすべき性質（帰納的定理）を検証
例：
dbl(x+y) = dbl(x) + dbl(y)
sum(dup(xs)) = dbl(sum(xs))
sum(dup([3,5]))
dbl(sum([3,5])) =
= sum([3,3,5,5]) = 16 = dbl(8)
x,y や xs が
どのような値であって
も、
両辺の実行結果が
等しくなる
「どのような入力に対してもプログラムが停止する」性質を利用した
数学的帰納法（書き換え帰納法）に基づき、上記定理を自動証明
研究課題：適切な実行戦略を効率よく探索する、
より自動化された手続きの実現

Download Report