by Shachar Itzhaky, Hila Peleg, Nadia Polikarpova, Reuben N. S. Rowe and Ilya Sergey
帰納法を用いた証明において帰納法の仮定を適切に強める（＝補題発見）ことが本質的な課題であることは広く知られているが、同様にプログラムの自動合成では適切な補助関数の生成が本質的な課題である。「プログラムと証明は同じものである」というアイデアを使って、本論文では循環証明 (cyclic proof) の証明探索を通してヒープを扱うプログラムを自動合成する方法が提案されている。
概要
一言で言えば、本論文の手法は Synthetic Separation Logic (SSL) という先行研究の cyclic な拡張である。これだけだとあんまりなので、以下ではもう少し詳しく説明する。
難しい例として論文で挙げられているのが２分木をリストに変換するプログラム flatten の自動合成である。ノードが葉である場合は良いとして、問題はノードが葉でない場合である。それぞれの子供を引数に再帰的に flatten を呼ぶまではよいのだが、その結果として２つのリストが手に入ってしまう。最終的な出力は１つのリストなので、２つのリストを１つにまとめることが必要なのだが、既存研究ではこの手続きを自動で合成することができなかった*1。これは「２つのリストを１つのリストにする手続きが必要」ということを発見するのが難しいためで、このことをヒントとして与えれば（例えば append 関数を利用可能な関数一覧に加えておくとか、append 関数の仕様をヒントとして入力するとか）既存手法でも解くことができる。
本論文のアプローチは cyclic proof なので、再帰的なデータ構造を見つけたら取り敢えずパターンマッチをしてみて、「生成対象の仕様が（偶然）これまでに見たものと一致したら、１回目の部分にジャンプする」*2ようなプログラムを合成することになる。リストの例では
２つのリスト xs, ys から、１つのリスト zs を作る (*)
ということが仕様を満足するプログラムを探索するのに、xs にパターンマッチをして、xs が空のケースとそうでないケースの両方でプログラムを合成することを目指す。空のケースはいいとして、空でないケースを考えると、xs = (a :: xs') という形だと分かるので、
１つの要素 a と２つのリスト xs', ys から、１つのリスト zs を作る
というのが新たな仕様となる。(zs = (a :: zs')) とすることで、
２つのリスト xs' と ys から、１つのリスト zs' を作る
という仕様を満足するプログラムを見つければよい。しかしこれは、(*)の変数名を変えたものに過ぎないので、そこへのジャンプ（または関数呼び出し）に代えられる。こうして、提案手法は flatten の合成に成功することになる。
私見
本手法はそれなりに強力なようだが、一見して気になる制限として、補題発見を能動的に行わない点を挙げる。cyclic proof の文脈でいうなら、cut を行わずに証明探索を行っている。したがって、自然に推論していって上の例のように "たまたま" cycle が構成できる場合はいいが、一般にはそういうことは期待できないはずで、そうした場合には本手法でも上手く合成はできないだろう。どれくらい多くの仕様（に対する推論）が自然に cycle を生成するのか、というのは重要な問題である。ライブラリ関数などは、その普遍性・一般性ゆえに、こういう制約下でも合成しやすそうである。
一般の cyclic proof 探索に応用できるような新しいアイデアがあるわけではなく、cyclic proof の推論としてはむしろ非常に素朴（かつ限界が明らかなもの）である。「一定程度ちゃんと動く実装」のための様々な工夫が大変そうであった。
