けっこう有名だけど、ちゃんと読んだことなかった論文。手法 $\lambda^{2}$ というプログラム合成の手法。

タイトル

Synthesizing Data Structure Transformations from Input-Output Examples

PLDI2015

Synthesizing data structure transformations from input-output examples | Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation

概要

リストや木構造のような再帰的なデータ構造に対して、高階関数の map や fold を含むプログラムを合成する手法を提案。

手法の入出力

手法の入力

入出力例 $a_i \mapsto b_i$ の集合 $\mathcal{E}_\text{in}$

手法の出力

プログラム
- $\forall i. (e\ a_i ) \rightsquigarrow b_i$
- コストモデル $\mathcal{C}$ において最小なもの

DSL の定義

DSL は代数型と再帰をもつラムダ式に基づいたものである。具体的な定義は以下。

f:id:t-keita:20200920015838p:plain

$\bigoplus$ は演算子であり、任意のものを追加することができるが、predefined なものとして map, mapt, filter, foldl, foldr, foldt, recl が定義されている。各命令のセマンティクスは以下の通りである。

f:id:t-keita:20200926013503p:plain

map, filter, fold はお馴染みの関数だが、recl ってなにもの？

Hypothesis によるプログラムの抽象化

欠けている（具体的されていない）構造をプレースホルダとしてもつ可能性のあるプログラムを hypothesis と呼ぶ。プレースホルダは自由変数として表現され hole と呼ばれる。hole をもつ hypothesis は open hypothesis と呼ばれる。なお open でない、closed hypothesis は program のはず。

たとえば、 $x$ や $\lambda x.f^{\ast} x$ は、それぞれ自由変数 $x$ と $f^{\ast}$ をもつので open hypothesis である。なお $x$ や $f^{\ast}$ が hypothesis に対する hole である。一方で、 $\lambda x. \texttt{map} (\lambda y. y + 1)\ x$ は、束縛変数しか持たないので closed hypothesis である。

合成アルゴリズムでは、hypothesis に含まれる hole を、具体的なプログラムや別の hypothesis に置換してゆくことで入出力の制約を満たすプログラムを見つける。

Synthesis Algorithm

まずは合成アルゴリズムの全体像から見てゆく。

f:id:t-keita:20200926010500p:plain:w400

$Q$ は subtask のキューである。 $e$ を hypothesis, $f$ を ( $e$ に含まれる) hole, $\mathcal{E}$ を入出力例とするとき、subtask は $(e, f, \mathcal{E})$ の3つ組から構成される。 hypothesis $e$ として最も簡単な形のプログラム $\lambda x.f$ から開始し、hole を DSL の命令に置換ししてゆく。なお、１行目は $\mathcal{E}$ でなく $\mathcal{E_\text{in}}$ が正しそう。

subtask の $e$ が closed hypothesis であれば、プログラムとして不足のない形であるため、入出力の制約を満たすか調べるのみである。(lines 4-7)

subtask の $e$ が open hypothesis であれば、hole $f$ をより複雑な構造 $h$ で置換してゆく。hole $f$ の型を出力例 $\mathcal{E}$ から推論し、その型に合う hypothesis $h$ を求める。このとき新たな hypothesis を作る処理は InductiveGen 内で行われる。詳細は後述。(lines 8, 9)

hypothesis $e$ に含まれる hole $f$ を hypothesis $h$ で置換し、その結果を $e'$ とする。得られる hypothesis が close である場合はキューに追加するのみである。得られる hypothesis $e'$ が open である場合、 $e'$ に含まれる hole $f^{\ast}$ に対し、 $f^{\ast}$ が満たすべき入出力例 $\mathcal{E}^{\ast}$ を求める。この処理は Deduce 内で行われる。(lines 10-15)

合成が成功する場合の具体例として、たとえば以下のように hypothesis の形が具体化されてゆく。

$\lambda x.f$
$\lambda x.(\texttt{foldl}\ h'\ [\ ]\ x)$ where $h' = \lambda a. \lambda e. f'$
$\lambda x.(\texttt{foldl}\ h'\ [\ ]\ x)$ where $h' = \lambda a. \lambda e. f'$ and $f' = \texttt{cons} (e, a)$

このとき $\lambda x.f$ の入出力の制約が以下であるとき、

$[\ ]\mapsto [\ ]$
$[0 ]\mapsto [0 ]$
$[0\ 1]\mapsto [1\ 0]$
$[0\ 1\ 2]\mapsto [2\ 1\ 0]$

$h' = \lambda a. \lambda e. f'$ の入出力の制約は以下となる。

$([\ ], 0) \mapsto [ 0 ]$
$([ 0 ], 1) \mapsto [1\ 0 ]$
$([1\ 0], 2) \mapsto [2\ 1\ 0 ]$

このように、hypothesis の構造を展開するのにあわせて、新たな hypothesis が満たすべき入出力の制約を演繹的に求めてゆくのがこの手法の特徴である。

Hypothesis Generation

Figure 2 のアルゴリズム中の InductiveGen( $\tau$ ) の詳細を見てゆく。ここでは、型 $\tau$ を満たす hypothesis を作る。

closed hypothesis を作るには、Figure 3 の命令のうち $\tau$ と型の整合性が取れるものを列挙するのみである。つまり、演算子として再帰的に hypothesis を持てるのは Figure 3 の命令のみという前提？DSL の演算子として独自に追加した命令が再帰的な構造を持つことは許されない？

closed hypothesis を作るため、Figure 3 以外の DSL の構文要素を列挙してゆく。このとき、型が $\tau$ と整合性が取れるもののみを再帰的に列挙する。型の整合性によって探索空間を削減しているものの、組み合わせ爆発が起きそうなところである。stream を採用しているのはこれを軽減するためっぽい。(とはいえ、解となる最小のプログラムのコストが n の場合は、やはりコストが (n-1) 以下のプログラムをすべて列挙する必要がある。)

Inference of New Examples Using Deduction

Figure 2 のアルゴリズム中の Deduce の詳細を見てゆく。ここでは、subtask $(e, f, \mathcal{E})$ から新たな $e'$ と $f^{\ast}$ が定まったとき、適切な入出力の制約 $\mathcal{E}^{\ast}$ を演繹的に求める。具体化には $e'$ の命令の種類に応じて Figure 4 の規則に従うように $\mathcal{E}^{\ast}$ を構成すればよい。

一部の具体例を見る。

①
f:id:t-keita:20200926024114p:plain:w400
新たに map を使う hypothesis を作ったとき、その時点での入出力 $\mathcal{E}$ のなかに入力と出力のリストの長さが異なるものがあったら、適切な $\mathcal{E}^{\ast}$ は存在しない ( $\bot$ )。たとえば、 $[1,2,3 ] \mapsto [1,2 ]$ を実現する map は存在しない。

②
f:id:t-keita:20200926024808p:plain:w400
新たに map を使う hypothesis を作ったとき、その時点での入出力 $\mathcal{E}$ のリストの要素のなかに、同じ入力値に対して異なる出力値が対応するようなものがあれば、適切な $\mathcal{E}^{\ast}$ は存在しない ( $\bot$ )。たとえば、 $[1,2,1 ] \mapsto [5, 6, 7 ]$ を実現する map は存在しない。なぜなら、1 に対応する値が 5 と 7 の2種類存在し、写像 (map) になっていないから。

上記2つの規則①,②は、整合性が取れないことを検出するためのものであったが、次の規則は整合性が取れた時に $\mathcal{E}^{\ast}$ が満たすべき要件について述べている。
f:id:t-keita:20200926025617p:plain:w400
たとえば、 $\mathcal{E} = \{ [1,2 ] \mapsto [5, 6 ] \}$ のとき、 $\mathcal{E}^{\ast} = \{ 1 \mapsto 5, 2 \mapsto 6 \}$ が得られる。

その他の規則に関しては論文参照。

Evaluation

論文参照。

所感

トップダウンで deductive な合成のアプローチ。わりと素直なやり方だと思う。入出力の制約を高階関数の引数に伝播させる仕組みが面白い。
演算子の引数のなかにリスト型のものが2つ以上存在するときは、入出力の制約を伝播するのは難しそう。たとえば、リストとリストを結合する演算子をサポートする場合など。このあたりは FlashMeta あたりが上手く扱っていた気がする。
ページ数は多いしフォーマルな記述がある一方で、例がたくさんあって理解しやすい。soundness や completeness についても議論がある。論文の書き方として参考になる。
具体化されていない構造をもつプログラムは、この論文では hypothesis と呼ばれているが、最近では sketch と呼ばれることが多い印象。ただ Morpheus の論文では、hypothesis と sketch という両方の用語を使っていた。