日本ソフトウェア科学会第 34 回大会 (2017 年度) 講演論文集

関係的仕様からの関数型プログラム合成
中尾 收

佐竹 佑規

海野 広志

本研究では, 複数の再帰関数の入出力に関する関係的仕様と一部の関数の定義が与えられたときに, 残りの関数の定義を関係的仕様を満たすように自動的に合成する手法を提案する. 関係的仕様の具体例として, 等価性, 非干渉性, 単調性, 冪等性, 逆関数の存在性が挙げられる. したがって提案手法を用いると, 融合, 組化, 逆変換といった異なるプログ
ラム変換を同じ枠組みで行うことができ, 変換が成功した場合にその正しさの証明も出力できる. 本研究では, [13] で提案された帰納的定理証明とホーン節制約解消に基づく関係的検証法を, 定義が不完全な関数を扱えるように拡張することで関係的合成を実現する. 具体的には, 定義が不完全な関数の入出力関係を表した述語変数が満たすべきホーン節制約を生成し, アブダクションによって解を求め, そこから関数定義を抽出する. 本研究ではさらに, 提案手法に基づいた合成器の実装および予備実験を行った.

ことである. 関係的仕様の具体例として, 等価性, 非干

1 はじめに渉性, 単調性, 冪等性, 逆関数の存在性などが挙げられプログラム合成とは, 入出力例や自然言語による仕る. 関係的仕様からのプログラム合成の特に有用な応様, 形式的な仕様が与えられたときに, それらを満た用例として, 融合 [5] [15] や, 組化 [2] [3], 逆変換 [4] とすプログラムを自動的に生成する技術である [7]. 特

いったプログラム変換が考えられる. 一般にプログラに, 形式仕様からのプログラム合成が成功した場合は,

ム変換は, 変換前のプログラムと変換前後のプログラ出力されたプログラムが仕様を満たすことが保証さムが満たすべき関係的仕様から, 変換後のプログラム

れるため, プログラム合成は, プログラム検証を不完を合成する問題として捉えることができる. つまり,全な定義を許すように一般化したものと捉えること関係的仕様からのプログラム合成を実現すれば, 様々ができる. 特に形式仕様から関数型プログラムを合成

なプログラム変換を統一的に扱うことができ, さらにする手法には, 合成問題を小さく単純なものに分解し変換が正しいことの証明を出力することができるよて効率的に解く Leon [8] や, 仕様を表現するためにリうになる. そのようなプログラム合成の具体例として,ファインメント型を用いる Synquid [9], SMT ソルバ

リストの偶数番目の要素を取り出す関数 even とリス

CVC4 のモデル生成機能を利用する合成手法 [10] がトの各要素の総和を計算する関数 sum から, リストの存在する.

偶数番目の要素の総和を計算する関数 sum even を合本研究の目標は, 形式的な関係的仕様からの関数型成する問題を図 1 に示す. ここで, リストの要素の順プログラムの自動合成である. 関係的仕様とは, 複数

番は先頭から 0 番目, 1 番目と数える. sum と even をのプログラムの間に成り立つ関係を表現した仕様の用いてリストの偶数番目の要素の合計を計算するにFunctional Program Synthesis from Relational Specifications.
This is an unrefereed paper. Copyrights belong to the Authors.
Shu Nakao, Yuki Satake, Hiroshi Unno, 筑波大学システム情報工学研究科, Graduate School of Systems and Information
Engneering, University of Tsukuba.

はリストの走査をそれぞれ 1 回ずつの合計 2 回行う必要があるが, 合成される sum even は同等の計算を 1度の走査によってまとめて行うように効率化される.
このようなプログラム変換を融合変換という [2] [3].
図 1 で, ”??” は合成によって自動的に生成したい部

type list = Nil | Cons of int * list
let rec even x =match x with
| Nil -> Nil| Cons(u, Nil) -> Cons(u, Nil)
| Cons(u, Cons(_, us))-> Cons(u, even us)
let rec sum x =match x with
| Nil -> 0
| Cons(u, us) -> u + sum us
let rec sum_even = ??
let main x =assert (sum (even x) = sum_even x)

ラーに行われることを利用し, 型主導のプログラム探索を行うことで, 効率的なプログラム合成を実現している. 関係的仕様からの合成のためにはリファインメ
ント型に出現する関数の定義を展開する必要があるが, Leon と同様に, 関数の定義を展開できない場合があるため関係的仕様からのプログラム合成は難しい.

CVC4 は, 合成問題の形式に応じてそれに合った合成手法の適用を行うが, 関係的仕様からの合成のような,複数の関数が出現するような形式の問題に有効な手法は我々の知る限り提案されていない.
そこで我々は, 関係的仕様からの関数型プログラム

図1

sum even の合成問題

合成が可能な新しい手法を提案する. 提案手法は, 帰納的定理証明およびホーン節制約解消に基づいた関係的仕様検証法 [13] を, 不完全な定義の関数を許すよ

let rec sum_even x =match x with
| Nil -> 0
| Cons (u, Nil) -> u
| Cons (u, Cons(_, us))-> u + sum_even us

うに一般化することによってプログラム合成を可能にしたものであり, 重要な点は, (1) ホーン節制約を扱う
ことと, (2) 帰納法を用いることの 2 つである. それぞれについて説明する.

(1) ホーン節制約とは, (制約付き) ホーン節によって
図2

sum even の合成問題の解表された述語変数上の制約であり, 命令型, 関数型, 並行型といった様々なパラダイムのプログラム検証問題

分を表す. この例では, main 関数中の assert 式が失敗

が, ホーン節制約の解消問題に帰着できることが知らしないこと, つまり sum (even x) = sum even x が false

れている [11] [12] [14] [6]. ホーン節制約に出現する述語とならないこととして even, sum, sum even の間の関変数は, 各プログラムポイントにおける帰納的不変条

係的仕様を与えている. このプログラム合成問題の解件を表しており, 制約を満たす述語変数の解の存在をの 1 つを図 2 に示す.

示すことができれば, プログラムが仕様を満たすこと

しかし, 既存の関数型プログラム合成手法 Leon [8],が保証される. また, ホーン節制約は例外や代数デー

Synquid [9], CVC4 [10] では, このような関係的仕様か

タ型, 高階関数のような高度な言語機能や, 非決定性,

らのプログラム合成を十分に行うことはできなかっ

非停止性といった副作用を自然に扱うことができる.

た. Leon は合成問題を, 関数の入出力の間の関係を表したがって, ホーン節制約は様々なパラダイムのプロす論理式の制約によって表現する. Leon はこの問題をグラム検証問題を統一的に扱うための中間言語と捉えより小さい部分問題に分解することで効率的なプロることができる. 同様に, 本研究では様々なパラダイ

グラム合成を実現している. しかし, 関係的仕様を分ムのプログラム合成問題を, ホーン節制約解消問題を解するためには制約に出現する関数の定義を展開し一般化して定義が不完全な述語変数を許すようにしなければならないが, 複雑な仕様では, 制約に出現すたホーン節制約アブダクション問題 (Horn Constriant

る関数の定義を展開することができない場合がある.

Abduction Problem, HCAP) に帰着することによって,したがって, Leon の手法では関係的仕様からのプログ

様々なパラダイムのプログラム合成問題を統一的に扱

ラム合成は難しい. Synquid は, 合成する関数の仕様をえるようにする. 本論文では特に, 一階の決定的関数

リファインメント型によって与え, プログラムの型付型プログラムを合成する手法を具体的に与える.

けがその部分プログラムの型付け結果を用いてモジュ(2) 帰納法を用いる利点は, 関係的仕様を扱うことがHCAP を形式化し, プログラム合成問題から HCAP へ!"#$%&'()*+,
34の帰着法を示す. 4 節では HCAP の求解法を示す. 5
節では, HCAP の解からプログラムを抽出する手法を示す. 6 節では実験の結果を示し, 考察を行う. 最後に,HACP

7 節では結論を述べる.

56

2 提案手法の概要-./"01278!"#$%&'(

ここでは, 合成問題の具体例として図 1 で示した

sum even の合成問題を用いて提案手法によるプログ
ラム合成の流れを簡単に説明する.

2. 1 合成問題の HCAP への帰着
図 3 における, 関数型プログラム合成問題から HCAP

図3

提案手法による合成の流れへの帰着を行う部分を説明する. [12] で提案されたプログラム検証問題からホーン節制約を生成する手

できることである. 帰納法を用いると, 複数の関数の法を, 不完全な定義を持つ関数を許すように拡張して間の相互不変条件を帰納法の仮定として表現し, 証明用いることで, 合成問題からホーン節制約を生成すに用いることができるため, 複数の再帰関数の定義をる. sum even の合成問題からは以下のホーン節制約

同時に解析することが要求されるような関係的仕様Hsum even が生成される.
P (Nil, Nil), P (Cons(u, Nil), Nil),












P
(Cons(u,Cons(u,us)),
Cons(v,
vs))
⇐
1
2




P (us, vs) ∧ v = u1 ,






′
′


Q(Nil,
0),
Q(Cons(u,
us),
r
+
u)
⇐
Q(us,
r
),









 ⊥ ⇐ P (x, y) ∧ Q(y, r ) ∧ R(x, r ) ∧ r ̸= r
1
2
12
述語変数 P, Q, R はそれぞれ関数 even, sum, sum evenの検証が可能となる [13]. 提案手法は, [13] で提案された, 帰納的定理証明とホーン節制約解消に基づくプログラム検証法を拡張してプログラム合成に用いることにより, 関係的仕様からのプログラム合成を実現する.
提案手法によるプログラム合成の流れを図 3 に示す. 提案手法はまず, プログラム合成問題を HCAP に帰着する. ここで, HCAP の解とは, 不完全な定義を持つ関数に対応する述語を定義するホーン節の集合で関係的仕様を満たすもののことである. そのような解を求めるため, 次に, 定義が不完全な述語の帰納的定
義のテンプレートを生成し, テンプレートのパラメー
タが満たすべき制約を生成・解消する. 最後に, HCAPの解から一階の決定的関数型プログラムを抽出し, プ
ログラム合成問題の解として出力する.
本研究ではさらに, 提案手法に基づいた, 関数型言語

OCaml のためのプログラム合成器の実装を行い, 新たに作成した関係的仕様からのプログラム合成問題のベンチマークセットを用いて評価実験を行なった.
本 論 文 は 以 下 の よ う に 構 成 さ れ る . 2 節 で は,

sum even の合成問 題 を例にと り, 提案 手法 の処 理の流れを説明する. 3 節ではプログラム合成問題との引数と返り値の間の帰納的不変条件を表す. R は不完全な定義の関数 sum even に対応する述語変数であるため, R を定義するホーン節制約は生成されていな
い. それぞれの述語の引数のうち, 最後のものは関数の返り値に対応しており, 他の引数は関数の引数に対応している. ホーン節 P (Nil, Nil) は関数 even の定義中のmatch 式の最初のケースから生成され, even の引数がNil であるときに Nil が返されることを意味する.
対 し て P (Cons(u1 , Cons(u2 , Nil)), Cons(v, vs)) ⇐P (us, vs) ∧ v = u1 は match 式の 3 番目のケースから生成され, even の引数が Cons(u1 , Cons(u2 , us))の形をしているときは再帰呼び出し even us を行
い, そ の 結 果 を vs と し た と き に Cons(u1 , vs) を返 す こ と を 意 味 す る. 最 下 行 の ホ ー ン 節 ⊥ ⇐P (x, y) ∧ Q(y, r1 ) ∧ R(x, t2 ) ∧ r1 ̸= r2 は assert 式

から生成されており, 条件式 sum (even x) = sum evenx が false とならないための制約を表す.
このように生成されたホーン節制約と, 不完全な定義の関数に対応する述語変数の集合を入力として, それらの述語変数の定義をホーン節の集合の形で求める問
題が HCAP である. この例では, HCAP は Hsum even
を満たすように R を定義するホーン節の集合を求める問題となる.
ただし合成の目的においては, 解が制約を満たすだ
けでなく, 合成されるプログラムが望ましい性質をもつように解を求める必要がある. 本研究で合成するプ
ログラムに望まれる性質は, 停止性が保証される入力の領域が広いことと決定的であることである. 例えば,

Hsum even を満たす R を定義するホーン節の集合として自明な解 ∅ を即座に求めることができるが, ∅ は無限ループによって停止しない無意味なプログラム
を表しており, 合成の目的においては望ましくない.
そこで, 解の優劣を表す半順序関係を与え, 極大解を求めることによって望ましい性質を持った解を得る.

sum even に関する HCAP の極大解を以下に示す.  R(Nil, 0), R(Cons(u, Nil), u), R(Cons(u1 , Cons(u2 , x′ )), r′ + u1 ) ⇐ R(x′ , r′ ) に示す.
 R(x, r) ⇐ νbase (x, r), R(x, r) ⇐ R(x′ , r′ ) ∧ νind (x, r, x′ , r′ ) テンプレート中の ν は未知論理式を表す. テンプレー
トの 1 行目は合成する関数 sum even のベースケースに対応し, 2 行目は再帰呼び出しを行うインダクショ
ンケースに対応する.
テンプレートを追加した制約は関係的仕様を満たさなければならないので, 未知論理式を許すように [13]を拡張したホーン節制約解消法を用いて制約を解きながら未知論理式が満たすべき制約を集める. [13] は
ホーン節制約の解が存在することの証拠として帰納的定理証明システムの証明木を構築するので, 未知論
理式を含むホーン節制約のための証明木を構築させ,その証明木が実際に解の存在性を含意するために未知論理式が満たすべき制約を証明木から抽出する. 上のテンプレートを利用して集めた未知論理式の制約を以下に示す.

⊥ ⇐ νbase (x, r2 ) ∧ r2 ̸= 0 ∧ x = Nil,⊥ ⇐ νind (x, r2 , x′ , r2′ ) ∧ r2 ̸= 0 ∧ x = Nil,⊥ ⇐ νbase (x, r2 ) ∧ r2 ̸= u ∧ x = Cons(u, Nil),⊥ ⇐ νind (x, r2 , x′ , r2′ ) ∧ r2 ̸= u ∧ x = Cons(u, Nil),

この解は, 図 2 で示した, 任意の入力に対して停止す⊥ ⇐ νbase (x, r2 ) ∧ x = Cons(u1 , Cons(u2 , us)),

る決定的なプログラムを表す. HCAP の詳細な定義は⊥ ⇐ νind (x, r2 , x′ , r2′ ) ∧ r2 ̸= r2′ + u ∧3 節にて述べる.

x = Cons(u1 , Cons(u2 , us)),⊥ ⇐ νind (x, r2 , x′ , r2′ ) ∧ x′ ̸= us ∧2. 2 HCAP の求解

x = Cons(u1 , Cons(u2 , us))

図 3 における, HCAP の求解法について説明する.

抽出された未知論理式の制約は, [1] で研究されたマHCAP の解空間は膨大であるため, 提案手法は解のルチアブダクション問題と捉えることができるため,

テンプレートを用いることによって探索空間を限定

同文献で提案されている求解法を, 合成の目的で望まし, テンプレートのパラメータである未知論理式を決しい解を求めるように拡張して用いる. 上の未知論理

定することによって解を求める. つまり, テンプレー

式の制約の解を以下に示す.

トによって解の形を制限することで, 合成される関数

νbase (x, r)≡

x = Cons(u1 , Nil) ∧ r = u1 ,定義に出現する補助関数の呼び出しや再帰呼び出しのパターンを制限している. したがって, テンプレー

x = Nil ∧ r = 0 ∨′′νind (x, r, x , r )≡x = Nil ∧ r = 0 ∨トを適切に設定することで目的のプログラム変換が,x = Cons(u1 , Nil) ∧ r = u1 ∨関係的仕様からのプログラム合成として実現される.

x = Cons(u1 , Cons(u2 , x′ )) ∧sum even の合成問題から帰着された HCAP の解を求

r = 1 + u1 + r ′めるために使用する解のテンプレートの一例を以下

この解をテンプレートに代入すると, 前節で示した

HCAP の解が得られる.

2. 3 HCAP の解からの関数型プログラム抽出{hc 1 , . . . , hc m } で あ る. ホ ー ン 節 と は 肯 定 形 の 述

図 3 における, HCAP の解からの関数型プログラ

語変数リテラルの数が 1 つ以下の節である. ホーン節

ムの抽出法について説明する. 本手法は, HCAP の解

hc に出現する述語変数の集合を pvs(hc) と表す. ホーから決定的な一階の関数型プログラムを抽出する.

HCAP の解に現れるホーン節の一つ一つは, 関数のン節制約系 H に関しては, 出現する述語変数の集合を∪pvs(H) = hc∈H pvs(hc) と定義する. H 中の任意の入力に応じた分岐に対応する. そのため, ホーン節

異なるホーン節 hc 1 , hc 2 は共通の自由変数を持たなごとに対応する分岐とその分岐の条件を抽出する.

いとする. ホーン節のうち Head が P (et) のものを確定

sum even の例では, ホーン節 R(Nil, 0) は sum even

節と呼び, H に含まれる確定節の集合を def (H) と記の引数が Nil のときに 0 を返すことを意味し, ホー述する. 同様に, Head が ⊥ のものをゴール節と呼び,

′

′

′

′

ン節 R(Cons(u1 , Cons(u2 , x )), r + u1 ) ⇐ R(x , r )′は引数が Cons(u1 , Cons(u2 , x ) のとき再帰呼び出し′′′H 中のゴール節の集合を goal (H) と記述する.
ホーン節制約系 H の述語解釈 ρ とは, H に出現すsum even x を行い, その返り値を r としたとき r +u1

る述語変数集合 pvs(H) から Var(P ) への写像である.

を返すことを意味する. したがって, 2. 2 節で示した

ここで, V は整数と代数データ型の値すべてを含む意

HCAP の解からは図 2 で示した OCaml プログラムが味領域を表す. ホーン節制約系 H の解とは, H に含ま抽出される.

れる全てのホーン節 hc ∈ H について ρ |= hc である
ような述語解釈 ρ のことであり, このとき ρ |= H と3 プログラム合成から HCAP への帰着

書く.

3. 1 ホーン節制約系
本研究で使用するホーン節制約系 (Horn Clause Con-straint Sets, HCCSs) の構文を以下で定義する.

3. 2 ホーン節制約アブダクション問題
定義 3.1 (ホーン節制約アブダクション問題) ホ ー ン(HCCS)

H: := {hc 1 , . . . , hc m }節制約アブダクション問題 (Horn Clause Abduction(Horn Clause)hc: := h ⇐ bProblem, HCAP) とは, ホーン節制約系 H と H に出現
する述語変数の部分集合 P ⊆ pvs(H), 確定節の集合(Head)h: := P (et) | ⊥(Body)b: := P1 (et1 ) ∧ ... ∧ Pm (etm ) ∧ ϕ上の半順序 ⪯ の組 (H, P, ⪯) として表される問題で(Formula)ϕ: := t1 ≤ t2 | t1 = t2

あり, その解とは, P 内の述語変数を定義する確定節(Term)

t| isC (t) | ⊤ | ⊥ | ¬ϕ

集合 D のうち, ホーン節制約系 H ∪ D の解が存在し,| ϕ1 ∧ ϕ2 | ϕ1 ∨ ϕ2

⪯ - 極大なものである. ⪯ - 極大な D とは, D ⪯ D′ を

: := n | x | t1 + t2 | t1 − t2

満たす D でない D′ が存在しないものである.

| C(et) | sC,i (t)
簡単のため, ここでは量化子のない整数上の線形算術

3. 3 HCAP への帰着

および代数データ型上の等式理論に限定して話を進めプログラム合成問題からのホーン節制約生成は, プる. P は述語変数, n は整数, x は変数, C は代数データ

ログラム検証問題からのホーン節制約生成法 [12] を,型のコンストラクタをそれぞれ表すメタ変数である. et

不完全な定義の関数を扱えるように拡張して行う. 合は項列 t1 , . . . , tm を, sC,i はコンストラクタ C の i 番

成問題中に出現する ”??” それぞれについてフレッシュ

目の引数を取得するアクセッサを, isC は引数がコンな述語変数を生成する.

ストラクタ C で構成された代数データ型の値である

本研究の目標は, 広い領域で停止する決定的な一階か判定する述語をそれぞれ表す. 述語変数 P およびコの関数型プログラムを合成することである. そのため,ンストラクタ C のアリティをそれぞれ ar(P ), ar(C)

解を制約論理プログラムとしてとらえ, 入力を定めたと表す.

ときにその導出が決定的である方が大きく, また導出

ホーン節制約系 H はホーン節の有限集合が停止するような入力の領域が広い方が大きいような半順序 ⪯det を持つ HCAP へ帰着させる. ただし, 半

未知論理式を作成すればよい.

順序 ⪯det が定義されるのは, 出現する述語変数が等

4. 2 未知論理式に関する制約の抽出

しいものに限る.

本手法は, 未知論理式に関する制約を集めるため,

4 HCAP の求解[13] の手法を拡張して用いる. 集められる制約は, Body

⪯det - 極大である HCAP の解を求めることは困難に未知論理式が出現するゴール節の形をとる.

である. そこで, ⪯det - 極大な解を求める保証はない

帰納的定理証明とホーン節制約に基づいたプログが, 多くの場合 ⪯det - 極大な解を求めることを目指

ラム検証法 [13] は, 関係的仕様を表現するホーン節

したヒューリスティクスを用いた HCAP の求解法を

制約の解の存在を, 帰納的定理証明に基づいて判定

この節で提案する. ⪯det - 極大な解を厳密に求めるよする. 帰納的定理証明は, 判断を D; Γ; A; ϕ ⊢ h のうな求解法や, 任意の半順序の極大解を求めるような形で記述し, 判断に対して推論規則を適用していき

HCAP の求解法は, 今後の課題である.

証明木を構築することで行う. D は述語変数を解

HCAP の求解は, 以下に示す手順で行う.

釈するための確定節の集合, Γ は帰納法の仮定を表

1. 未知論理式を含む HCAP の解のテンプレートをす論理式の集合, A は述語変数適用の集合, ϕ は述作成する

語変数適用を含まない論理式の集合, h はホーン節

2. 帰納的定理証明に基づくホーン節制約解消法[13] によって証明木を構築し, 未知論理式に関する制約を集める

3. 集めた制約をマルチアブダクション問題としての Head である. 判断 D; Γ; A; ϕ ⊢ h は, D による∧述語の解釈と Γ の補題の元で, A ∧ ϕ ⊢ h が妥当であることを表す. ホーン節制約 H 中のゴール∧
節の集合 goal (H) = { Ai ∧ ϕi ⇒ ⊥}m
i=1 から判断

def (H); ∅; Ai ; ϕi ⊢ ⊥ を生成することで, ホーン節制

解くことで HCAP の解を得る

4. 3 で得た HCAP の解から, ヒューリスティックス
を用いて ⪯det でより大きい解を得る

約解消問題を, 全ての判断について証明木を構築する
定理証明問題に帰着させる.

以降の節で, それぞれの手順について詳述する.

本手法は, 未知論理式を含むホーン節制約を元に生成される判断に対して証明規則を適用していくことで

4. 1 テンプレートの生成

証明木を構築し, 構築した証明木が解の存在性を含意

未知論理式をパラメータにもつ HCAP の解のテンするために必要な未知論理式の制約条件を抽出する.

プレートを生成する. 未知論理式は, ホーン節に出現する述語変数適用の各引数の間の関係を表す. 2. 2 節

ただし, 判断内の Head h は ⊥ に限られる.

sum even の合成問題の例から生成される判断 J1 をで示したテンプレート中の未知論理式 νbase (x, r) は,以下に示す.

Head の述語変数適用 R(x, r) の引数 x, r の間の関係

J1 ≡ D; ∅; {P (x, y), Q(y, r1 ), R(x, r2 )} ; r1 ̸= r2 ⊢ ⊥′′を表している. 同様に, 未知論理式 νind (x, r, x , r ) は,4. 2. 1 推論規則

Head の述語変数適用 R(x, r) と, Body の述語変数適本手法で判断を導出するために用いる推論規則は,

′

′

′

′

用 R(x , r ) のそれぞれの引数 x, r, x , r の間の関係[13] の推論規則のうち, INDUCT 規則, UNFOLD 規則,を表している.

APPLY⊥ 規則, VALID⊥ 規則の 4 つである. それぞれ

2 節では Body に出現する述語が Head と同じ述語について説明する. INDUCT 規則は判断中の A 内の変数を持つものに限ったテンプレートを説明したが,述語変数適用の一つを選び, その述語変数適用の導出

他の述語の出現を許すこともできる. 複数の関数呼びに関する帰納法を適用することで帰納法の仮定を作成

出しを許す場合は, 対応する述語の組み合わせの数だ

し, Γ に追加する. UNFOLD 規則は判断中の A 内の述

けテンプレートを生成し, それぞれのホーン節に出現

語変数適用 P (et) を一つ選び, その述語変数適用の導出∧木を得るために最後に使われた規則 P (et) ⇐ ϕi ∧ Ai

するすべての述語変数適用の引数の間の関係を表す

を D から取り出し, 場合分けを行う. このとき場合分けの数だけ証明木は分岐する. 判断中の ϕ は ϕ ∧ ϕi に,

J13

A は A ∪ Ai に更新される. APPLY⊥ 規則は Γ に含ま

J15
J14

VALID⊥

J8

れる帰納法の仮定を一つ選び, 対応する述語変数適用

VALID⊥APPLY⊥UNFOLD R..
.

に適用する. VALID⊥ 規則は, 判断中の ϕ が ϕ |= ⊥であるときに証明木の枝を閉じる.

J9

VALID⊥

J11

J12
J10

J5

4. 2. 2 証明木の推定戦略用している証明戦略をそのまま使用することはできない. そこで本手法では合成のために, HCAP の述語
変数の集合 P に注目した以下の戦略を採用する.

..
.

J7

J2
J1

1. 最初の判断 D; ∅; A1 ; ϕ1 ⊢ ⊥ の A1 に含まれる述語変数適用のうち, その述語変数が P に含まれな

図4

VALID⊥J6
J4

INDUCT Q

UNFOLD Q

UNFOLD Q

未知論理式が含まれるホーン節制約には, [13] が採

..
.
J5
J3

VALID⊥..
.
J8

UNFOLD Q

INDUCT Q
UNFOLD P

INDUCT P

sum even の合成問題で構築される証明木

いもの全てについて, それぞれ 1 度ずつ UNFOLD
規則と INDUCT 規則を適用する.

加した判断 J2 を生成している. この仮定は, 以降の証

2. UNFOLD 規則によって新たに A に追加された

明規則の適用により新たに追加された述語変数適用

述語変数適用の, 入力に対応する代数データ型のP (x′ , y ′ ) について, y ′ が等しい述語変数適用 Q(y ′ , r1′ )引数について, ϕ からどのコンストラクタで構成と, x′ が等しい述語変数適用 R(x′ , r2′ ) が存在する場

されているかという情報が得られる場合, その述合に APPLY⊥ 規則によって適用することができる. こ

語変数適用に対してもう一度 UNFOLD 規則を適の仮定を適用すると, 判断中の論理式 ϕ を ϕ ∧ r1′ = r2′

用する. これを繰り返す.

に更新することができる. J2 からは, 述語変数適用

3. 判断 D; Γ; A; ϕ ⊢ ⊥ の A に含まれる述語変数適P (x, y) に注目して UNFOLD 規則を適用する. D 中に用のうち, その述語変数が P に含まれるもの全て

P を定義する確定節は 3 つ存在するため, UNFOLDについて, それぞれ 1 度だけ UNFOLD 規則を適規則を適用すると証明木が 3 つに分岐する. 分岐の先用する.

でも Q について同様に, INDUCT 規則を適用して帰4. UNFOLD 規則によって展開された確定節がすべて述語変数適用を含むような場合の枝に, APPLY⊥
規則を適用する.

納法の仮定を追加したのち, UNFOLD 規則により証明木を分岐させる.

UNFOLD する確定節の組み合わせによっては, 判

5. VALID⊥ 規則を適用し枝を閉じる.

断中の論理式 ϕ が充足不可能となる場合が存在す

6. 以上全ての手順において, 判断 D; Γ; A; ϕ ⊢ ⊥る. 判 断 J9 中 の 論 理 式 ϕ9 に つ い て 注 目 す る と,中の論理式 ϕ が更新された際, ϕ |= ⊥ であるな

ϕ9 ⇒ x = Cons(u1 , Nil) ∧ x = Nil である. しから即座に VALID⊥ 規則を適用し枝を閉じる.

し, そのような x は存在しないため, ϕ9 ⊢ ⊥ である

この戦略を, sum even の合成問題から生成されたことから VALID⊥ 規則によって枝を閉じることがで

判断 J1 に適用して得られる証明木を図 4 に示す.

きる.

戦略に沿って順に説明する. 最初の判断 J1 に次 に 手 順 2 を 適 用 す る.UNFOLD 規 則 に よって対し, 手順 1 に従い, 述語変数適用 P (x, y), Q(y, r1 )P (Cons(u, Nil), Cons(u, Nil)), Q(Cons(u, us), r′ +について, INDUCT 規則と UNFOLD 規則をそれぞu) ⇐ Q(us, r′ ) の確定節に関する分岐を行なった

れ 適 用 す る. 述 語 変 数 適 用 P (x, y) に 関 し て IN-

判断 J5 について注目して説明する. 新しく追加された

DUCT 規則を適用することによって, 帰納法の仮定

述語変数適用は Q(us, r ′ ) である. この判断中の論理

P (x, y) ∧ Q(y, r1 ) ∧ R(x, r2 ) ⇒ r1 = r2 を J1 に追式 ϕ5 について, ϕ5 ⇒ us = Nil であるため, Q(us, r ′ )に注目して UNFOLD 規則を適用する.
手順 2 が完了したならば, 手順 3 に従い不完全な定義の関数に対応する述語変数適用 R(x, r2 ) につ述語変数適用が存在する場合, その述語変数適用のために A から選出された述語変数適用の対応する引数とその引数が等しいという制約が抽出される.

関する UNFOLD 規則の適用を行う. 判断 J8 に注

図 4 で示した証明木の J14 に APPLY⊥ 規則を適用

目 し て 説 明 す る. R(x, r2 ) を UNFOLD す る こ としている部分では, 帰納法の仮定を適用するために必に よ り, 解 の テ ン プ レ ー ト R(x, r) ⇐ νbase (x, r),

要な条件が x′ = us であるため, 制約 ϕ14 ⇒ x′ = us

R(x, r) ⇐ R(x′ , r′ ) ∧ νind (x, r, x′ , r′ ) 中のそれぞれが抽出される. また, 未知論理式を含む判断に対しての未知論理式 ν が判断中の ϕ に追加される.

VALID⊥ 規則を適用している部分から, それぞれ未知

手順 3 が完了したならば, UNFOLD 規則による分岐が全て述語変数適用を判断に追加するような枝につい論理式が満たすべき制約が抽出される. それらを全て集めると, 2. 2 節で示した制約となる.

て, APPLY⊥ 規則を適用する. 判断 J14 がその条件に当てはまる枝であるため, それに注目して説明する. 判断

4. 3 マルチアブダクションによる求解J14 内の述語変数適用は, P (x, y), Q(y, r1 ), R(x, r2 ),証明木から集めたそれぞれの制約について未知論

P (us, vs), Q(vs, r1′ ), R(x′ , r2′ ) である. このとき, 帰納

理式の解を求め, 最後に全ての解の論理積を取ったも法の仮定 P (x, y) ∧ Q(y, r1 ) ∧ R(x, r2 ) ⇒ r1 = r2 をのを解のテンプレートに代入したものを HCAP の解

述語変数適用の組 P (us, vs), Q(vs, r1′ ), R(x′ , r2′ ) に適とする. 未知論理式の解を求めるために, [1] にて紹介

用して, 判断中の論理式 ϕ14 を r1′ = r2′ ∧ ϕ14 に更新されているマルチアブダクション問題の最弱解を求めする.

る手法を, 証明木から集めた制約の最弱解を求めるよ以上の手順を全て終えて, 判断中の論理式 ϕ に未知

うに拡張して適用する. マルチアブダクション問題と論理式 ν を含むものは VALID 規則を適用し証明木のは, 複数種類の述語変数適用が複数回出現する制約を枝を閉じる.

満足する述語変数の解を求める問題である. ここで最この戦略により, 定義済みの関数と似た再帰呼び出しを行う関数を合成することができる. 複雑な再帰呼弱解とは, その解より論理的に弱い解が存在しないものをいう.

び出しを行う関数の合成はこの戦略だけでは不十分[1] の手法は, 与えられた制約を満足する述語の最弱であるため, より洗練された戦略を発見することが将解をモデル生成と量化子除去 (Quantifier Elimination,

来の課題である.

以下 QE) を用いて求める. その手法は以下に示す 3 つ

4. 2. 3 証明木からの未知論理式の制約抽出
証明木の構築において, VALID⊥, APPLY⊥ 規則を適用する際に制約を抽出する.
判断 D; Γ; A; ϕ ⊢ ⊥ に対し VALID⊥ 規則を適用する条件に ϕ |= ⊥ という制約が含まれる. したがって

ϕ 中に未知論理式が含まれていてかつ ϕ |= ⊥ が自明でない場合, ϕ ⇒ ⊥ が制約として抽出される.
判断 D; Γ; A; ϕ ⊢ ⊥ に対し APPLY⊥ 規則を適用す∧る際, A′ ∧ ϕ′ ⊢ h という形の帰納法の仮定が参照さ′のステップに分かれている.

1. モデルによって生成した述語変数の初期解を用いて, 制約を述語変数の種類ごとに分解する

2. 分解した制約を, さらに述語変数適用の出現ごとに分解する

3. 述語変数の初期解を生成し, QE によってその解を弱める
この手法には制約の分解によっては, 解を無限に弱め続けるケースに陥ることや, 各々の述語は最弱だが全れる. A は仮定あるいは補題に必要な述語変数適用

体では最弱でないような局所解を出力することがあるの集合であり, 述語変数適用に対応するものを A からという問題があった. この問題を解決するために, 分適切に選出する. その際 A から選出される述語変数適解を行う際にまず論理式の形による分解を試みるこ

用の中に不完全な定義の関数に対応する述語 P が含とで, 問題が起きるような分解をなるべく防ぐようなまれており, かつ A′ 中で P の引数と共通の変数を持

拡張を行った.

4. 2. 3 節にて抽出された sum even の問題の制約をAlgorithm 1: extractdef extract(P ; D)

解くと, 未知論理式の解は以下のようになる.

νbase (x, r)≡

x = Nil ∧ r = 0 ∨(where D = {P (ex, y) ⇐ bi | 1 ≤ i ≤ m} ,∧ nixij , yij ) ∧ ϕi )bi = j Pij (ex = Cons(u, Nil) ∧ r = u,νind (x, r, x′ , r′ )≡x = Nil ∧ r = 0 ∨=x = Cons(u1 , Nil) ∧ r = u ∨x = Cons(u1 , Cons(u2 , x′ )) ∧r = u1 + r ′if QE(∃ex.ϕ1 ) thenextract branch(λy.b1 ; xe)else if . . .
else if QE(∃ex.ϕn ) then

4. 4 より大きい解へのアプローチ
マルチアブダクション問題を解くことによって未知論理式の解を求めることで得た HCAP の解は, 制約論

extract branch(λy.bn ; xe)else inf loop()// 無限ループ

理プログラムとして捉えたときに, 入力を定めたときの導出が複数存在するという意味で決定的ではない.
そのため, 入力を定めたときの導出が一意に定まるよ
うに解の決定化を行うヒューリスティックスを述べる.

HCAP の解の中の, 不完全な定義の関数に対応する述語変数を定義する各々の確定節について, 述語の入力
変数の領域で重なるものが存在するとき, その 2 つの差集合をとって片方の入力変数の領域を狭めることで, 重なる領域が存在しないようにする. このとき, 再節の集合となる.
 R(Nil, 0), R(Cons(u, Nil), u),′′′′ R(Cons(u1 , Cons(u2 , x )), r + u1 ) ⇐ R(x , r ) 

5 HCAP の解からのプログラム抽出
HCAP の解は確定節の有限集合であるため, 制約論
理プログラムと捉えることができる. ここでは, 制約論理プログラムから 1 階の決定的な関数の定義の抽出を試みる手法を述べる. 他のパラダイムのプログラ

帰的な定義の確定節の領域を狭めるようにする.
このヒューリスティックスを適用することで, 制約論理プログラムの意味で, 入力を定めたときにその導出が一意に定まるように決定化している. しかし, 出

ムを抽出したい場合は, それに特化した抽出の手法を与える必要がある. 抽出法のバリエーションを増やす
ことは今後の課題である.

力のモデルが複数存在するような場合に出力を一意

述語変数 P と, P を Head にもつ確定節の有限に定めることや, 停止しないような導出を避けるよう

集合 D から, P に対応する関数を定義を抽出するに決定化することはできない.

手続き extract を Algorithm 1 に示す. D 中の確定節∧ i
P (ex, y) ⇐ nxij , yij ) ∧ ϕi は, P に対応する関j Pij (e4. 3 節で求めた sum even の問題の解は以下のホーン節の集合である.


R(Nil,
R(Cons(u,0),Nil), u),
 R(Nil, 0) ⇐ R(x′ , r′ ),









数の入力に応じた分岐のうちの一つを表す. xe は関数の入力に対応する変数, y は返り値に対応する変数である. QE(∃ex.ϕi ) は, ϕi に出現する変数のうち x
e に含



R(Cons(u, Nil), u) ⇐ R(x′ , r′ ),







 R(Cons(u , Cons(u , x′ )), r′ + u ) ⇐ R(x′ , r′ ) 121
この解が表すプログラムは, 入力が Nil である場合と,の領域に射影したものが if 式の分岐条件となる. 分岐

Cons(u, Nil) の形をしている場合に当てはまる確定節の本体の式は, 手続き extract branch によって抽出さが複数存在するため, 非決定的である. この解に対しれる. どの分岐条件にも当てはまらない入力が存在すて決定化を行うと, 以下に示すような決定的なホーンる場合は, 無限ループを起こす分岐に到達する.

まれないものを存在量化した論理式の量化子除去を行った論理式を表す. QE によって, ϕi を入力変数 xeif 式の各分岐を抽出する手続き extract branch の定Algorithm 3: decide

Algorithm 2: extract branch∧
def extract branch(λy.( ∅ ∧ ϕ); ue)=

def decide(eu; ϕ)=// 空列

ϵdecide(eu; λy.ϕ)def extract branch∧(λy.( nxi , yi ) ∧ ϕ); ue)=
i=1 Pi (edef decide(eu; λx1 , . . . , xn .ϕ)=let ϕ′ = QE(∃x1 , ue.ϕ) inlet et = decide(eu; λex1 .ϕ) inlet ψ = ∀eu.((∃x1 .ϕ′ ) ⇒ ϕ′ [x1 7→ f (eu)]) inlet ϕ = ϕ[ex1 7→ et ] in′let Mf = model(ψ) in

let y1 = fun of(P1 )(e
t) in

Mf (e
u),

extract branch∧( nxi , yi ) ∧ λy.ϕ′ ; y1 , ue)
i=2 Pi (edecide(eu; λx2 , . . . , xn .ϕ[x1 7→ Mf (eu)])

由変数が出現するため, QE によって x1 , ue 以外の変義を Algorithm 2 に示す. extract branch の入力は, 合成数を除去した論理式 ϕ′ を得る. x1 に対応する式は,される式が満たすべき述語 λy.b と式に出現してよい∀eu.((∃x1 .ϕ′ ) ⇒ ϕ′ [x1 7→ f (eu)]) を満たす関数 f のモ

自由変数の列 ue である. b 中の述語変数適用 Pi (exi , yi )デル Mf を SMT ソルバによって生成することによりは, Pi に対応する関数の呼び出しの入力に対応する

合成する.

変数が x
ei ,

返り値に対応する変数が yi であることを表す. ただし, b 中の述語変数適用の各引数として

6 実装と実験

渡される変数は互いに異なるものとする. λy.b に述提案手法に基づいた関数型プログラム合成器のプ

語変数適用が現れない場合, つまり関数呼び出しを行

ロトタイプを, 関数型プログラム検証器 RCaml [12] をわない式を抽出する場合は, 後述の手続き decide を用拡張することによって実装した. RCaml には帰納法にいる.1 つ以上の述語変数適用が現れる場合, 先頭の 1

基づいたホーン節制約ソルバ [13] がすでに組み込まつ P1 (ex1 , y1 ) に対応する関数呼び出しを作成し, 関数

れていたので, それを拡張した.

呼び出しの返り値に y1 を let 束縛して残りの述語変本研究では, 独自に作成したベンチマークセットを数適用を再帰的に処理する. ここで, y1 を束縛する let

用いて実装した合成器の評価実験を行なった. ベンチ

式はプログラムの構文上の let 式であるのに対し, そマークセットは本論文の付録に添付する. 表 6 に実験

れ以外の let 式はアルゴリズムレベルの let 式なので,結果を示す. kind 列は合成問題としてどのような関係

extract branch が返す式に出現しないということに注的仕様を与えたのかを示す. eq は等価性, inv は逆関数意されたい. 関数呼び出しのために, 引数の列 xe1 に対の存在性, incr は増加性を表す. 特に, sum even は融合応する式の列 et も手続き decide によって決定する. そ変換の問題である. result 列には合成に成功したもの

して, 論理式 ϕ 中の x
e1 を et で置き換えた論理式 ϕ をについては得られたプログラムを示し, 失敗したもの

得る. fun of(P1 ) は, 述語変数 P1 に対応する関数をについてはその原因を示す. wrong proof tree は証明木表す.

の探索に失敗していることを表す. stack overflow は,′手 続 き decide の 定 義 を Algorithm 3 に 示 す. de-cide の引数は, 合成される n 個の式に出現してよ

合成の際にスタックオーバーフローが起きてしまったことを表す.

い自由変数の列 u
e と, n 個の式が満たすべき述語

また, 関数型プログラム合成器 Leon [8] について,

λx1 , . . . , xn .ϕ である. n = 0 の場合, decide は空列を今回作成したベンチマークセットと同等のものを入力

返す. n > 0 の場合, まず x1 に対応する式を合成し,として与え実験した. 表 6 に実験結果を示す. 実験で残りの x2 , . . . , xn についても再帰的に合成する. 与えは time out を 1 分に設定した. Leon は再帰的な定義られた述語の論理式 ϕ には, x1 , . . . , xn , ue の他にも自を持つ関数の逆関数の合成問題 sub acc を解けていな表1

提案手法の実験結果

problemkindresultmult acceqmult acc x y a = if y = 0 then a else mult acc x (y-1) (a+x)

mult

eq

mult x y = if y = 0 then 0 else x + mult x (y-1)

mult int

mult x y = x * ymult disteqwrong proof tree

sum acceq

wrong proof tree

sub

inv

sub x y = x - y

sub recinv

sub x y = if y = 0 then x else sub (x-1) (y-1)

pred

inv

pred x = x - 1

double1eq

wrong proof tree

double2eq

double x = if x = 0 then 0 else 2 + double (x - 1)

incr

incr

incr x = x + 1
max x y = if x > y then x else ymax
sum eveneq

sum even l = match l with Nil → 0 | Cons(u,Nil) → u | Cons(u, Cons ( , us)) → u + sum even us

sum scseq

sum scs l = match l with Nil → 0 | Cons(u, us) → 1 + u + sum scs ustup sum eveneq

wrong proof tree

pred dup

inv

stack overflow

い. また, sum even の合成結果は, sum と even の 2 つの関数呼び出しを行なっているため, 融合変換になっ
ていない.

7 まとめ
本論文では, 関係的仕様から関数型プログラムを合成するための帰納的定理証明およびホーン節制約に基づいた手法を提案した. また提案手法の実装とベンチマークを用いた評価実験を行い, 既存手法との比較を行った. 既存手法では難しかった, プログラム合成によるプログラム変換において有望な結果を得た.
参考文献[ 1 ] Albarghouthi, A., Dillig, I., and Gurfinkel, A.: Maximal Specification Synthesis, Proc. POPL ’16, ACM, 2016,
pp. 789–801.
[ 2 ] Bird, R. S.: Using circular programs to eliminate
multiple traversals of data, Acta Informatica, Vol. 21,
No. 3(1984), pp. 239–250.
[ 3 ] Chin, W.-N.: Towards an Automated Tupling Strategy,
Proc. PEPM’93, ACM, 1993, pp. 119–132.
[ 4 ] Dijkstra, E. W.: Program Inversion, Springer New York,
1982, pp. 351–354.

[ 5 ] Gill, A., Launchbury, J., and Peyton Jones, S. L.: A short
cut to deforestation, Proc. FPCA’93, ACM, 1993, pp. 223–
232.
[ 6 ] Grebenshchikov, S., Lopes, N. P., Popeea, C., and Rybalchenko, A.: Synthesizing Software Verifiers from Proof
Rules, Proc. PLDI’12, ACM, 2012, pp. 405–416.
[ 7 ] Gulwani, S.: Dimensions in Program Synthesis, Proc.
PPDP ’10, ACM, 2010, pp. 13–24.
[ 8 ] Kneuss, E., Kuraj, I., Kuncak, V., and Suter, P.: Synthesis Modulo Recursive Functions, Proc. OOPSLA ’13, ACM,
2013, pp. 407–426.
[ 9 ] Polikarpova, N., Kuraj, I., and Solar-Lezama, A.: Program Synthesis from Polymorphic Refinement Types, Proc.
PLDI ’16, ACM, 2016, pp. 522–538.
[10] Reynolds, A., Deters, M., Kuncak, V., Tinelli, C., andBarrett, C.: Counterexample-Guided Quantifier Instantiation for Synthesis in SMT, Proc. CAV’15, 2015, pp. 198–
216.
[11] Rondon, P., Kawaguchi, M., and Jhala, R.: Liquid
Types, Proc. PLDI’08, ACM, 2008, pp. 159–169.
[12] Unno, H. and Kobayashi, N.: Dependent Type Inferencewith Interpolants, Proc. PPDP’09, ACM, 2009, pp. 277–
288.
[13] Unno, H., Torii, S., and Sakamoto, H.: Automating
Induction for Solving Horn Clauses, Proc. CAV’17, 2017,
pp. 571–591.
[14] Vazou, N., Seidel, E. L., Jhala, R., Vytiniotis, D., andPeyton Jones, S. L.: Refinement Types for Haskell, Proc.
ICFP’14, ACM, 2014, pp. 269–282.
[15] Wadler, P.: Deforestation: transforming programs to表2Leon の実験結果

problemresultmult acc

mult acc(x,y,a) = mult(x, y) + a

mult

mult(x,y) = mult acc(x, y, 0)mult intmult(x, y) = x * ymult dist

mult dist(x, y, z) = mult(x, z) + mult(y, z)

sum accsum acc(x, a)= a + sum(x)sub

sub(x,y) = x - y

sub rectime outpred

pred(x) = x - 1

double1

double(x) = mult(x, 2)

double2

double(x) = mult(2, x)

incr

failedmax

max(x, y) = if (x ≥ y) x else ysum evensum even(l) = sum (even(l))

tup sum eventup sum even(l) = (sum(l), even(l))

pred dup

time out

eliminate trees, Proc. ESOP’88, LNCS, Vol. 300, 1988,
pp. 344–358.

A ベンチマーク
本研究で作成した合成器の実験に使用したベンチ
マークプログラムを以下に示す.

mult acc
let rec mult x y =if y = 0 then 0 else y + mult x (y-1)
let rec mult_acc x y a = ??
let main x y a =assert(a + mult x y = mult_acc x y a)mult
let rec mult x y = ??
let rec mult_acc x y a =if y = 0 then aelse mult_acc x (y-1) (a+x)
let main x y a =assert(a + mult x y = mult_acc x y a)mult int
let rec mult x y = mult x y
let main x y =assert(x * y = mult x y)mult dist
let rec mult x y =if y = 0 then 0 else x + mult x (y-1)
let rec mult_dist x y z = ??
let main x y z =assert (mult x z + mult y z= mult_dist x y z)

sum acc
let rec sum n =if n < 0 then n + sum (n + 1)
else if n = 0 then 0
else n + sum (n - 1)
let rec sum_acc n a = ??
let main n a =assert(a + sum n = sum_acc n a)sub
let rec add x y = x + y
let rec sub x y = ??
let main x y =assert (add y (sub x y) = x)

sub rec
let rec add x y =if x = 0 then y else 1 + add (x-1) y
let rec sub x y = ??

let main x y =assert (add y (sub x y) = x)

pred
let succ x = x + 1
let rec pred x = ??
let main x =assert (pred (succ x) = x)

double1
let rec mult x y =if y = 0 then 0 else x + mult x (y-1)
let rec double x = ??
let main x =assert (mult x 2 = double x)

double2
let rec mult x y =if y = 0 then 0 else x + mult x (y-1)
let rec double x = ??
let main x =assert (mult 2 x = double x)

mono
let rec mono x = ??
let main x y =if x > y then assert (mono x > mono y)else ()

incr
let rec incr x = ??
let main x =assert (incr x > x)

comm
let rec comm x y = ??
let main x y =assert(comm x y = comm y x)

max
let rec max x y = ??
let main x y =if x > y thenassert (max x y = x)
else
assert (max x y = y)sum eventype list = Nil | Cons of int * list
let rec sum l =match l with
| Nil -> 0
| Cons(u, us) -> u + sum us
let rec even l =match l with
| Nil -> Nil| Cons(u, us) -> Cons(u, us)| Cons(u1, Cons(u2, us))-> Cons(u1, even us)
let rec sum_even l = ??
let main l =assert (sum (even l) = sum_even l)sum scs
type list = Nil | Cons of int * list
let rec scs l =match l with
| Nil -> Nil| Cons(u, us) -> Cons(1 + u, scc us)
let rec sum l =match l with
| Nil -> 0
| Cons(u, us) -> u + sum us
let rec sum_scs l = ??
let main l =assert (sum (scs l) = sum_scs l)tup sum eventype list = Nil | Cons of int * list
let rec sum l =match l with
| Nil -> 0
| Cons(u, us) -> u + sum us
let rec even l =match l with
| Nil -> Nil| Cons(u, us) -> Cons(u, us)| Cons(u1, Cons(u2, us))-> Cons(u1, even us)
let rec tup_sum_even l = ??
let main l =assert ((sum l, even l) = tup_sum_even l)pred dup

type list = Nil | Cons of int * list
let rec succ l =match l with
| Nil -> Nil| Cons(u, us) -> Cons(u + 1, succ us)
let rec dup l =match l with
| Nil -> Nil| Cons(u, us) -> Cons(u, Cons(u, dup us))let rec pred_dup l = ??
let main l =assert (succ (pred_dup l) = dup l)