34 (2017 ),,.,,,,,.,,,,., [13],.,,,.,. 1,,, [7].,,,,., Leon [8], Synquid [9], SMT CVC4 [10].,., Functional Program Synthesis from Relational Specifica

Size: px

Start display at page:

Download "34 (2017 ),,.,,,,,.,,,,., [13],.,,,.,. 1,,, [7].,,,,., Leon [8], Synquid [9], SMT CVC4 [10].,., Functional Program Synthesis from Relational Specifica"

けんじつつの
5 years ago
Views:

1 34 (2017 ),,.,,,,,.,,,,., [13],.,,,.,. 1,,, [7].,,,,., Leon [8], Synquid [9], SMT CVC4 [10].,., 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..,,,,,., [5] [15], [2][3], [4].,,.,,,., even sum, sum even 1., 0, 1. sum even 1 2, sum even 1. [2][3]. 1,??

2 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) 1 sum even let rec sum_even x = match x with Nil -> 0 Cons (u, Nil) -> u Cons (u, Cons(_, us)) -> u + sum_even us 2 sum even., main assert, sum (even x) = sum even x false even, sum, sum even. 1 2., Leon [8], Synquid [9], CVC4 [10],. Leon,. Leon.,,,., Leon. Synquid,,,,., Leon,. CVC4,,,.,., [13],,, (1), (2) 2.. (1), ( ),,,, [11] [12] [14] [6].,,,.,,,,.,.,, (Horn Constriant Abduction Problem, HCAP),.,. (2),

3 !"#$%&'()*+, 34 HACP 56 -./"012 78!"#$%&'( 3.,,, [13]., [13],,. 3., HCAP., HCAP,.,,,., HCAP,.,, OCaml,.. 2, sum even,. 3 HCAP, HCAP. 4 HCAP. 5, HCAP. 6,., 7. 2, 1 sum even HCAP 3, HCAP. [12],,. sum even H sum even. P (Nil, Nil), P (Cons(u, Nil), Nil), P (Cons(u 1, Cons(u 2, us)), Cons(v, vs)) P (us, vs) v = u 1, Q(Nil, 0), Q(Cons(u, us), r + u) Q(us, r ), P (x, y) Q(y, r 1) R(x, r 2) r 1 r 2 P, Q, R even, sum, sum even. R sum even, R.,,. P (Nil, Nil) even match, even Nil Nil. P (Cons(u 1, Cons(u 2, Nil)), Cons(v, vs)) P (us, vs) v = u 1 match 3, even Cons(u 1, Cons(u 2, us)) even us, vs Cons(u 1, vs). P (x, y) Q(y, r 1) R(x, t 2) r 1 r 2 assert

4 , sum (even x) = sum even x false.,, HCAP., HCAP H sum even R.,,.,., H sum even R,,.,,. sum even HCAP. R(Nil, 0), R(Cons(u, Nil), u), R(Cons(u 1, Cons(u 2, x )), r + u 1) R(x, r ), 2,. HCAP HCAP 3, HCAP. HCAP,,.,,.,,. sum even HCAP. 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, r 2) r 2 0 x = Nil, ν ind (x, r 2, x, r 2) r 2 0 x = Nil, ν base (x, r 2) r 2 u x = Cons(u, Nil), ν ind (x, r 2, x, r 2) r 2 u x = Cons(u, Nil), ν base (x, r 2) x = Cons(u 1, Cons(u 2, us)), ν ind (x, r 2, x, r 2) r 2 r 2 + u x = Cons(u 1, Cons(u 2, us)), ν ind (x, r 2, x, r 2) x us x = Cons(u 1, Cons(u 2, us)), [1],,.. ν base (x, r) x = Nil r = 0 x = Cons(u 1, Nil) r = u 1, ν ind (x, r, x, r ) x = Nil r = 0 x = Cons(u 1, Nil) r = u 1 x = Cons(u 1, Cons(u 2, x )) r = 1 + u 1 + r, HCAP.

5 2. 3 HCAP 3, HCAP., HCAP. HCAP,.,. sum even, R(Nil, 0) sum even Nil 0, R(Cons(u 1, Cons(u 2, x )), r + u 1) R(x, r ) Cons(u 1, Cons(u 2, x ) sum even x, r r +u 1., 2. 2 HCAP 2 OCaml. 3 HCAP 3. 1 (Horn Clause Constraint Sets, HCCSs). (HCCS) H ::= {hc 1,..., hc m} (Horn Clause) hc ::= h b (Head) h ::= P ( t) (Body) b ::= P 1( t 1)... P m( t m) ϕ (Formula) ϕ ::= t 1 t 2 t 1 = t 2 is C(t) ϕ ϕ 1 ϕ 2 ϕ 1 ϕ 2 (Term) t ::= n x t 1 + t 2 t 1 t 2 C( t) s C,i(t),. P, n, x, C. t t 1,..., t m, s C,i C i, is C C. P C ar(p ), ar(c). H {hc 1,..., hc m}. 1. hc pvs(hc). H, pvs(h) = hc H pvs(hc). H hc 1, hc 2. Head P ( t), H def (H)., Head, H goal(h). H ρ, H pvs(h) V ar(p )., V. H, H hc H ρ = hc ρ, ρ = H ( ) (Horn Clause Abduction Problem, HCAP), H H P pvs(h), (H, P, ),, P D, H D, -. - D, D D D D HCAP, [12],.??.,.,,,

6 det HCAP., det,. 4 HCAP det - HCAP., det -, det - HCAP. det -, HCAP,. HCAP,. 1. HCAP 2. [13], 3. HCAP 4. 3 HCAP, det, HCAP., ν base (x, r), Head R(x, r) x, r., ν ind (x, r, x, r ), Head R(x, r), Body R(x, r ) x, r, x, r. 2 Body Head,.,,. 4. 2,, [13]., Body. [13],,., D; Γ; A; ϕ h,. D, Γ, A, ϕ, h Head. D; Γ; A; ϕ h, D Γ, A ϕ h. H goal(h) = { A i ϕ i } m i=1 def (H); ; A i; ϕ i,,.,,., Head h. sum even J 1. J 1 D; ; {P (x, y), Q(y, r 1), R(x, r 2)} ; r 1 r , [13], INDUCT, UNFOLD, APPLY, VALID 4.. INDUCT A,, Γ. UNFOLD A P ( t), P ( t) ϕ i A i

7 D,.. ϕ ϕ ϕ i, A A A i. APPLY Γ,. VALID, ϕ ϕ = , [13]., HCAP P. 1. D; ; A 1; ϕ 1 A 1, P, 1 UNFOLD INDUCT. 2. UNFOLD A,, ϕ, UNFOLD.. 3. D; Γ; A; ϕ A, P, 1 UNFOLD. 4. UNFOLD, APPLY. 5. VALID. 6., D; Γ; A; ϕ ϕ, ϕ = VALID., sum even J J 1, 1, P (x, y), Q(y, r 1), INDUCT UNFOLD. P (x, y) IN- DUCT, P (x, y) Q(y, r 1) R(x, r 2) r 1 = r 2 J 1. 4 J 9. J 5 J 3 J 13 VALID VALID J 5 INDUCT Q J 2 J 1 J 8. J 11 J 7 INDUCT P J 15 J 14 J 10 VALID APPLY UNFOLD R J 12 VALID VALID UNFOLD Q J 6 J 4 UNFOLD Q. J 8 INDUCT Q UNFOLD P sum even UNFOLD Q J 2., P (x, y ), y Q(y, r 1), x R(x, r 2) APPLY., ϕ ϕ r 1 = r 2. J 2, P (x, y) UNFOLD. D P 3, UNFOLD 3. Q, INDUCT, UNFOLD. UNFOLD, ϕ. ϕ 9 J 9 ϕ 9, x = Cons(u 1, Nil) x = Nil., x, ϕ 9 VALID. 2.UNFOLD P (Cons(u, Nil), Cons(u, Nil)), Q(Cons(u, us), r + u) Q(us, r ) J 5. Q(us, r ). ϕ 5, ϕ 5 us = Nil, Q(us, r )

8 UNFOLD. 2, 3 R(x, r 2) UNFOLD. J 8. R(x, r 2) UNFOLD, R(x, r) ν base (x, r), R(x, r) R(x, r ) ν ind (x, r, x, r ) ν ϕ. 3, UNFOLD, APPLY. J 14,. J 14, P (x, y), Q(y, r 1), R(x, r 2), P (us, vs), Q(vs, r 1), R(x, r 2)., P (x, y) Q(y, r 1) R(x, r 2) r 1 = r 2 P (us, vs), Q(vs, r 1), R(x, r 2), ϕ 14 r 1 = r 2 ϕ 14., ϕ ν VALID.,., , VALID, APPLY. D; Γ; A; ϕ VALID ϕ =. ϕ ϕ =, ϕ. D; Γ; A; ϕ APPLY, A ϕ h. A, A. A P, A P, A. 4 J 14 APPLY, x = us, ϕ 14 x = us., VALID,., , HCAP., [1],.,.,. [1], (Quantifier Elimination, QE) , 2., 3., QE,,.,,.

9 sum even,. ν base (x, r) x = Nil r = 0 x = Cons(u, Nil) r = u, ν ind (x, r, x, r ) x = Nil r = 0 x = Cons(u 1, Nil) r = u x = Cons(u 1, Cons(u 2, x )) r = u 1 + r 4. 4 HCAP,,.,. HCAP,,, 2,.,.,,.,, sum even. R(Nil, 0), R(Cons(u, Nil), u), R(Nil, 0) R(x, r ), R(Cons(u, Nil), u) R(x, r ), R(Cons(u 1, Cons(u 2, x )), r + u 1) R(x, r ), Nil, Cons(u, Nil),., Algorithm 1: extract def extract(p ; D) (where D = {P ( x, y) b i 1 i m}, b i = n i j P ij( x ij, y ij) ϕ i) = if QE( x.ϕ 1) then extract branch(λy.b 1; x) else if... else if QE( x.ϕ n) then extract branch(λy.b n; x) else inf loop() //. R(Nil, 0), R(Cons(u, Nil), u), R(Cons(u 1, Cons(u 2, x )), r + u 1) R(x, r ) 5 HCAP HCAP,., 1.,.. P, P Head D, P extract Algorithm 1. D P ( x, y) n i j P ij( x ij, y ij) ϕ i, P. x, y. QE( x.ϕ i), ϕ i x. QE, ϕ i x if., extract branch.,. if extract branch

10 Algorithm 2: extract branch def extract branch(λy.( ϕ); ũ)= decide(ũ; λy.ϕ) def extract branch (λy.( n i=1 Pi( xi, yi) ϕ); ũ)= let t = decide(ũ; λ x 1.ϕ) in let ϕ = ϕ[ x 1 t ] in let y 1 = fun of(p 1)( t) in extract branch ( n i=2 Pi( xi, yi) λy.ϕ ; y 1, ũ) Algorithm 3: decide def decide(ũ; ϕ)= ϵ // def decide(ũ; λx 1,..., x n.ϕ)= let ϕ = QE( x 1, ũ.ϕ) in let ψ = ũ.(( x 1.ϕ ) ϕ [x 1 f(ũ)]) in let M f = model(ψ) in M f (ũ), decide(ũ; λx 2,..., x n.ϕ[x 1 M f (ũ)]), QE x 1, ũ Algorithm 2. extract branch, λy.b ũ. b P i( x i, y i), P i x i, y i., b. λy.b,, decide.1, 1 P 1( x 1, y 1), y 1 let., y 1 let let, let let, extract branch., x 1 t decide., ϕ x 1 t ϕ. fun of(p 1), P 1. decide Algorithm 3. decide, n ũ, n λx 1,..., x n.ϕ. n = 0, decide. n > 0, x 1, x 2,..., x n. ϕ, x 1,..., x n, ũ ϕ. x 1, ũ.(( x 1.ϕ ) ϕ [x 1 f(ũ)]) f M f SMT. 6, RCaml [12]. RCaml [13],.,.. 6. kind. eq, inv, incr., sum even. result,. wrong proof tree. stack overflow,., Leon [8],. 6. time out 1. Leon sub acc

11 1 problem kind result mult acc eq mult 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 * y mult dist eq wrong proof tree sum acc eq wrong proof tree sub inv sub x y = x - y sub rec inv sub x y = if y = 0 then x else sub (x-1) (y-1) pred inv pred x = x - 1 double1 eq wrong proof tree double2 eq double x = if x = 0 then 0 else 2 + double (x - 1) incr incr incr x = x + 1 max max x y = if x > y then x else y sum even eq sum even l = Nil 0 Cons(u,Nil) u Cons(u, Cons (, us)) u + sum even us sum scs eq sum scs l = Nil 0 Cons(u, us) 1 + u + sum scs us tup sum even eq 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 [ 2 ] Bird, R. S.: Using circular programs to eliminate multiple traversals of data, Acta Informatica, Vol. 21, No. 3(1984), pp [ 3 ] Chin, W.-N.: Towards an Automated Tupling Strategy, Proc. PEPM 93, ACM, 1993, pp [ 4 ] Dijkstra, E. W.: Program Inversion, Springer New York, 1982, pp [ 5 ] Gill, A., Launchbury, J., and Peyton Jones, S. L.: A short cut to deforestation, Proc. FPCA 93, ACM, 1993, pp [ 6 ] Grebenshchikov, S., Lopes, N. P., Popeea, C., and Rybalchenko, A.: Synthesizing Software Verifiers from Proof Rules, Proc. PLDI 12, ACM, 2012, pp [ 7 ] Gulwani, S.: Dimensions in Program Synthesis, Proc. PPDP 10, ACM, 2010, pp [ 8 ] Kneuss, E., Kuraj, I., Kuncak, V., and Suter, P.: Synthesis Modulo Recursive Functions, Proc. OOPSLA 13, ACM, 2013, pp [ 9 ] Polikarpova, N., Kuraj, I., and Solar-Lezama, A.: Program Synthesis from Polymorphic Refinement Types, Proc. PLDI 16, ACM, 2016, pp [10] Reynolds, A., Deters, M., Kuncak, V., Tinelli, C., and Barrett, C.: Counterexample-Guided Quantifier Instantiation for Synthesis in SMT, Proc. CAV 15, 2015, pp [11] Rondon, P., Kawaguchi, M., and Jhala, R.: Liquid Types, Proc. PLDI 08, ACM, 2008, pp [12] Unno, H. and Kobayashi, N.: Dependent Type Inference with Interpolants, Proc. PPDP 09, ACM, 2009, pp [13] Unno, H., Torii, S., and Sakamoto, H.: Automating Induction for Solving Horn Clauses, Proc. CAV 17, 2017, pp [14] Vazou, N., Seidel, E. L., Jhala, R., Vytiniotis, D., and Peyton Jones, S. L.: Refinement Types for Haskell, Proc. ICFP 14, ACM, 2014, pp [15] Wadler, P.: Deforestation: transforming programs to

12 2 Leon problem result mult acc mult acc(x,y,a) = mult(x, y) + a mult mult(x,y) = mult acc(x, y, 0) mult int mult(x, y) = x * y mult dist mult dist(x, y, z) = mult(x, z) + mult(y, z) sum acc sum acc(x, a)= a + sum(x) sub sub(x,y) = x - y sub rec time out pred pred(x) = x - 1 double1 double(x) = mult(x, 2) double2 double(x) = mult(2, x) incr failed max max(x, y) = if (x y) x else y sum even sum even(l) = sum (even(l)) tup sum even tup sum even(l) = (sum(l), even(l)) pred dup time out A eliminate trees, Proc. ESOP 88, LNCS, Vol. 300, 1988, pp 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 a else 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 =??

13 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) Nil -> 0 Cons(u, us) -> u + sum us let rec even l = 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 = Nil -> Nil Cons(u, us) -> Cons(1 + u, scc us) let rec sum l = 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 even type list = Nil Cons of int * list let rec sum l = Nil -> 0 Cons(u, us) -> u + sum us let rec even l = 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) max let rec max x y =?? let main x y = if x > y then assert (max x y = x) else assert (max x y = y) sum even type list = Nil Cons of int * list let rec sum l =

14 pred dup type list = Nil Cons of int * list let rec succ l = Nil -> Nil Cons(u, us) -> Cons(u + 1, succ us) let rec dup l = 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)

Parametric Polymorphism

ML 2 2011/04/19 Parametric Polymorphism Type Polymorphism ? : val hd_int : int list - > int val hd_bool : bool list - > bool val hd_i_x_b : (int * bool) list - > int * bool etc. let hd_int = function (x