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