λ² 
λ² is a tool for synthesizing functional programs from input-output examples.
There are two versions of λ²:
- PLDI: This is a slightly improved version of the code that we benchmarked for the PLDI 2015 paper. Use this if you want to reproduce our benchmarks.
- Development: This version has significantly diverged and no longer performs similarly. However, it has many more features and the code is cleaner. Use this if you want to extend λ².
Building
- Clone the repository:
git clone [email protected]:jfeser/L2.git; cd L2- Install dependencies.
opam install --deps-only ./l2.opam.lockedPLDI version
- Check out the
pldi-modernizebranch.
git checkout pldi-modernize- Try λ² on a benchmark problem by running:
dune exec src/l2.exe -- benchmarks/concat.jsonYou should see output like:
Solved concat in 39ms. Solutions:
(let concat (let a (lambda (c b) (foldr c (lambda (e d) (cons d e)) b)) _) _)
Development version
- Try λ² on a benchmark problem by running:
dune exec src/l2-cli/l2_cli.exe -- synth -l components/stdlib.ml -dd higher_order,input_ctx specs/largest_n.jsonYou should see output like:
.lkO0K0xc.
'kk;. .;kWXc Synthesizing..
.NN, kMMo
'WMWx kMMk Hypotheses verified: 48458
;dkc lWMX, Hypotheses saved: 0
.:loc. .OMWx.
.okcdWMN, .oXOc. Memoization table hit rate: 98.16
.0o kMM0 .xNk' ';
.' lMMN. .cOl. .KO Hashcons table equals calls: 1139934 (718173 t, 421761 f)
;MMM, lXWOddddddx0Md Hashcons table hash calls: 891626, hashcons calls: 891626
oMMM: ;kkkkkkkkkkkkk, Hashcons table len: 73738, num entries: 69923
.ONWMMl Hashcons bucket sum: 160341, min: 0, med: 3, max: 21
'XO.0MMo
,Ko OMMx Signatures: 2785 none, 25306 checked, 18420 dups, 0 fails
.xNc xMMO
;NK, dMM0
.dNd. lMMX. ..
;XMo :MMM' ,O.
dWNl .NMMOlxd.
lKO: ;KMNx.
Runtime: 5.4s
Found solution:
fun b a -> take (reverse (sort (concat a))) b
Running benchmarks
Benchmark problems are in the bench/ directory.
Questions?
Send email to [email protected].
Publications
Feser, J. K., Chaudhuri, S., & Dillig, I. (2015, June). Synthesizing data structure transformations from input-output examples. In Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation (pp. 229-239). ACM.