Refinement Type Inference via Horn Constraint
Optimization?
Kodai Hashimoto and Hiroshi Unno
University of Tsukuba{kodai, uhiro}@logic.cs.tsukuba.ac.jp

Abstract. We propose a novel method for inferring refinement types ofhigher-order functional programs. The main advantage of the proposed
method is that it can infer maximally preferred (i.e., Pareto optimal)
refinement types with respect to a user-specified preference order. The
flexible optimization of refinement types enabled by the proposed method
paves the way for interesting applications, such as inferring most-generalcharacterization of inputs for which a given program satisfies (or violates) a given safety (or termination) property. Our method reducessuch a type optimization problem to a Horn constraint optimization
problem by using a new refinement type system that can flexibly reason about non-determinism in programs. Our method then solves theconstraint optimization problem by repeatedly improving a current solution until convergence via template-based invariant generation. We have
implemented a prototype inference system based on our method, andobtained promising results in preliminary experiments.

1

Introduction

Refinement types [5, 20] have been applied to safety verification of higher-orderfunctional programs. Some existing tools [9, 10, 16–19] enable fully automatedverification by refinement type inference based on invariant generation techniques such as abstract interpretation, predicate abstraction, and CEGAR. The
goal of these tools is to infer refinement types precise enough to verify a given
safety specification. Therefore, types inferred by these tools are often too specificto the particular specification, and hence have limited applications.
To remedy the limitation, we propose a novel refinement type inference
method that can infer maximally preferred (i.e., Pareto optimal) refinement
types with respect to a user-specified preference order. For example, let us consider the following summation function (in OCaml syntax)
let rec sum x = if x = 0 then 0 else x + sum (x - 1)
A refinement type of sum is of the form (x : {x : int | P (x)}) → {y : int | Q(x, y)}.
Here, P (x) and Q(x, y) respectively represent pre and post conditions of sum.
Note that the postcondition Q(x, y) can refer to the argument x as well as thereturn value y. Suppose that we want to infer a maximally-weak predicate for?

This work was supported by Kakenhi 25730035, 23220001, 15H05706, and 25280020.

P and maximally-strong predicate for Q within a given underlying theory. Our
method allows us to specify such preferences as type optimization constraints:
maximize(P ),minimize(Q).

Here, maximize(P ) (resp. minimize(Q)) means that the set of the models of P (x)(resp. Q(x, y)) should be maximized (resp. minimized). Our method then infersa Pareto optimal refinement type with respect to the given preferences.
In general, however, this kind of multi-objective optimization involves a
trade-off among the optimization constraints. In the above example, P may
not be weakened without also weakening Q. Hence, there often exist multiple
optima. Actually, all the following are Pareto optimal refinement types of sum.1(x : {x : int | x = 0}) → {y : int | y = x}(1)(x : {x : int | true}) → {y : int | y ≥ 0}(2)

(x : {x : int | x < 0}) → {y : int | false}(3)

Our method further allows us to specify a priority order on the predicate
variables P and Q. If P is given a higher priority over Q (we write P @ Q),
our method infers the type (2), whereas we obtain the type (3) if Q @ P .
Interestingly, (3) expresses that sum is non-terminating for any input x < 0.
The flexible optimization of refinement types enabled by our method paves
the way for interesting applications, such as inferring most-general characterization of inputs for which a given program satisfies (or violates) a given safety(or termination) property. Furthermore, our method can infer an upper boundof the number of recursive calls if the program is terminating, and can find aminimal-length counterexample path if the program violates a safety property.
Internally, our method reduces such a refinement type optimization problem to a constraint optimization problem where the constraints are expressed
as existentially quantified Horn clauses over predicate variables [1, 11, 19]. The
constraint generation here is based on a new refinement type system that canreason about (angelic and demonic) non-determinism in programs. Our method
then solves the constraint optimization problem by repeatedly improving a current solution until convergence. The constraint optimization here is based on an
extension of template-based invariant generation [3,7] to existentially quantified
Horn clause constraints and prioritized multi-objective optimization.
The rest of the paper is organized as follows. Sections 2 and 3 respectively
formalize our target language and its refinement type system. The applicationsof refinement type optimization are explained in Section 4. Section 5 formalizes
Horn constraint optimization problems and the reduction from type optimization problems. Section 6 proposes our Horn constraint optimization method.
Section 7 reports on a prototype implementation of our method and the resultsof preliminary experiments. We compare our method with related work in Section 8 and conclude the paper in Section 9. An extended version of the paperwith proofs is available online [8].
1Here, we use quantifier-free linear arithmetic as the underlying theory and consider
only atomic predicates for P and Q.

E[op(en)] −→D E[JopK(en)] (E-Op)
D(f ) = λex.e|ex| = |ev|

E[f ve] −→D E[[e
v /e
x]e]

E[let x = v in e] −→D E[[v/x]e](E-Let)(E-App)E[let x = ∗∀ in e] −→D E[[n/x]e](E-Rand∃)(E-If)

E[let x = ∗∃ in e] −→D E[[n/x]e](E-Rand∀)

if n = 0 then i = 1 else i = 2
E[ifz n then e1 else e2 ] −→D E[ei ]Fig. 1. The operational semantics of our language L

2

Target Language L

This section introduces a higher-order call-by-value functional language L, whichis the target of our refinement type optimization. The syntax is defined as follows.
m(programs) D ::= {fi 7→ λe
xi .ei }i=1(expressions) e ::= x | e1 e2 | n | op(e1 , . . . , ear (op) ) | ifz e1 then e2 else e3| let x = e1 in e2 | let x = ∗∀ in e | let x = ∗∃ in e(values) v ::= n | f ve(eval. contexts) E ::= [ ] | E e | v E | ifz E then e1 else e2 | let x = E in e
Here, x and f are meta-variables ranging over variables. n and op respectively
represent integer constants and operations such as + and ≥. ar (op) expresses
the arity of op. We write xe (resp. ve) for a sequence of variables xi (resp. valuesvi ) and |ex| for the length of xe. For simplicity of the presentation, the language L
has integers as the only data type. We encode Boolean values true and falsemrespectively as non-zero integers and 0. A program D = {fi 7→ λe
xi .ei }i=1 is amapping from variables fi to expressions λe
xi .ei , where λe
x.e is an abbreviationof λx1 . . . . λx|ex| .e. We define dom(D) = {f1 , . . . , fm } and ar (fi ) = |exi |. A value
f ve is required to satisfy 1 ≤ |ev | < ar (f ).
The call-by-value operational semantics of L is given in Figure 1. Here, JopK
represents the integer function denoted by op. Both expressions let x = ∗∀ in e
and let x = ∗∃ in e generate a random integer n, bind x to it, and evaluatee. They are, however, interpreted differently in our refinement type system (seeSection 3). We support these expressions to model various non-deterministic
behaviors caused by, for example, user inputs, inputs from communication channels, interrupts, and thread schedulers. We write −→∗D to denote the reflexive
and transitive closure of −→D .

3

Refinement Type System for L

In this section, we introduce a refinement type system for L that can reason about
non-determinism in programs. We then formalize refinement type optimization
problems (in Section 3.1), which generalize ordinary type inference problems.

The syntax of our refinement type system is defined as follows.
(refinement types) τ ::= {x | φ} | (x : τ1 ) → τ2
(type environments) Γ ::= ∅ | Γ, x : τ | Γ, φ(formulas) φ ::= t1 ≤ t2 | > | ⊥ | ¬φ | φ1 ∧ φ2 | φ1 ∨ φ2 | φ1 ⇒ φ2(terms) t ::= n | x | t1 + t2 | n · t(predicates) p ::= λex.φ
An integer refinement type {x | φ} equipped with a formula φ for type refinement
represents the type of integers x that satisfy φ. The scope of x is within φ.
We often abbreviate {x | >} as int. A function refinement type (x : τ1 ) → τ2represents the type of functions that take an argument x of the type τ1 andreturn a value of the type τ2 . Here, τ2 may depend on the argument x andthe scope of x is within τ2 . For example, (x : int) → {y | y > x} is the typeof functions whose return value y is always greater than the argument x. We
often write fvs(τ ) to denote the set of free variables occurring in τ . We definedom(Γ ) = {x | x : τ ∈ Γ } and write Γ (x) = τ if x : τ ∈ Γ .
In this paper, we adopt formulas φ of the quantifier-free theory of linear
integer arithmetic (QFLIA) for type refinement. We write |= φ if a formula φ isvalid in QFLIA. Formulas > and ⊥ respectively represent the tautology and thecontradiction. Note that atomic formulas t1 < t2 (resp. t1 = t2 ) can be encoded
as t1 + 1 ≤ t2 (resp. t1 ≤ t2 ∧ t2 ≤ t1 ) in QFLIA.
The inference rules of our refinement type system are shown in Figure 2.
Here, a type judgment ` D : Γ means that a program D is well-typed under arefinement type environment Γ . A type judgment Γ ` e : τ indicates that an
expression e has a refinement type τ under Γ . A subtype judgment Γ ` τ1 <: τ2states that τ1 is a subtype of τ2 under Γ . JΓ K occurring in the rules ISub andRand∃ is defined by J∅K = >, JΓ, x : {ν | φ}K = JΓ K ∧ [x/ν]φ, JΓ, x : (ν : τ1 ) →τ2 K = JΓ K, and JΓ, φK = JΓ K ∧ φ. In the rule Op, JopKTy represents a refinement
type of op that soundly abstracts the behavior of the function JopK. For example,
J+KTy = (x : int) → (y : int) → {z | z = x + y}.
All the rules except Rand∀ and Rand∃ for random integer generation are
essentially the same as the previous ones [18]. The rule Rand∀ requires e to have
τ for any randomly generated integer x. Therefore, e is type-checked against τunder a type environment that assigns int to x. By contrast, the rule Rand∃
requires e to have τ for some randomly generated integer x. Hence, e is typechecked against τ under a type environment that assigns a type {x | φ} to x
for some φ such that fvs(φ) ⊆ dom(Γ ) ∪ {x} and |= JΓ K ⇒ ∃x.φ. For example,
x : int ` let y = ∗∃ in x + y : {r | r = 0} is derivable because we can derivex : int, y : {y | y = −x} ` x + y : {r | r = 0}. Thus, our new type systemallows us to reason about both angelic ∗∃ and demonic ∗∀ non-determinism inhigher-order functional programs.
We now discuss properties of our new refinement type system. We can prove
the following progress theorem in a standard manner.
Theorem 1 (Progress). Suppose that we have ` D : Γ , dom(Γ ) = dom(D),and Γ ` e : τ . Then, either e is a value or e −→D e0 for some e0 .

Γ ` D(f ) : Γ (f )(for each f ∈ dom(D))`D:ΓΓ (x) = {ν | φ}
Γ ` x : {ν | ν = x}
Γ (x) = (ν : τ1 ) → τ2
Γ ` x : (ν : τ1 ) → τ2
Γ, x : τ1 ` e : τ2
Γ ` λx.e : (x : τ1 ) → τ2Γ ` e1 : (x : τ1 ) → τ2Γ ` e 2 : τ1Γ ` e1 e2 : τ2
Γ ` n : {ν | ν = n}Γ ` e : τ0

Γ ` τ 0 <: τΓ `e:τ
|= JΓ K ∧ φ1 ⇒ φ2

Γ ` {ν | φ1 } <: {ν | φ2 }(Prog)(IVar)(FVar)

(Abs)

(App)

Γ ` e1 : τ1
Γ, x : τ1 ` e2 : τ2
x 6∈ fvs(τ2 )(Let)Γ ` let x = e1 in e2 : τ2
Γ, x : int ` e : τ

x 6∈ fvs(τ )Γ ` let x = ∗∀ in e : τ
fvs(φ) ⊆ dom(Γ ) ∪ {x}|= JΓ K ⇒ ∃x.φ
Γ, x : {x | φ} ` e : τ
x 6∈ fvs(τ )Γ ` let x = ∗∃ in e : τ(Rand∀)(Rand∃)Γ ` e1 : {ν | φ}Γ, φ ∧ ν = 0 ` e2 : τΓ, φ ∧ ν 6= 0 ` e3 : τ(If)Γ ` ifz e1 then e2 else e3 : τ(Int) Γ ` JopKTy <: (x1 : τ1 ) → . . . → (xm : τm ) → τΓ ` ei : τi (for each i ∈ {1, . . . , m})(Sub)Γ ` op(e1 , . . . , em ) : τ(ISub)Γ ` τ10 <: τ1
Γ, ν : τ10 ` τ2 <: τ20
Γ ` (ν : τ1 ) → τ2 <: (ν : τ10 ) → τ20(Op)(FSub)

Fig. 2. The inference rules of our refinement type system

We can also show the type preservation theorem in a similar manner to [18].
Theorem 2 (Preservation). Suppose that we have ` D : Γ and Γ ` e : τ . If
e is of the form let x = ∗∃ in e0 , then we get Γ ` e0 : τ for some e0 such thate −→D e0 . Otherwise, we get Γ ` e0 : τ for any e0 such that e −→D e0 .
3.1

Refinement Type Optimization Problems

We now define refinement type optimization problems, which generalize refinement type inference problems addressed by previous work [9, 10, 15–19].
We first introduce the notion of refinement type templates. A refinement type
template of a function f is the refinement type obtained from the ordinary MLstyle type of f by replacing each base type int with an integer refinement type{ν | P (ex, ν)} for some fresh predicate variable P that represents an unknown
predicate to be inferred, and each function type T1 → T2 with a (dependent)
function refinement type (x : τ1 ) → τ2 . For example, from an ML-style type(int → int) → int → int, we obtain the following template.
(f : (x1 : {x1 | P1 (x1 )}) → {x2 | P2 (x1 , x2 )}) →(x3 : {x3 | P3 (x3 )}) → {x4 | P4 (x3 , x4 )}Note here that the first argument f is not passed as an argument to P3 andP4 because f is of a function type and never occurs in QFLIA formulas for
type refinement. A refinement type template of a program D with dom(D) ={f1 , . . . , fm } is the refinement type environment ΓD = f1 : τ1 , . . . , fm : τm ,where each τi is the refinement type template of fi . We write pvs(ΓD ) for theset of predicate variables that occur in ΓD . A predicate substitution θ for ΓD
is a map from each P ∈ pvs(ΓD ) to a closed predicate λx1 , . . . , xar (P ) .φ, wherear (P ) represents the arity of P . We write θΓD to denote the application of a
substitution θ to ΓD . We also write dom(θ) to represent the domain of θ.
We can define ordinary refinement type inference problems as follows.
Definition 1 (Refinement Type Inference). A refinement type inference
problem of a program D is a problem to find a predicate substitution θ such that
` D : θΓD .
We now generalize refinement type inference problems to optimization problems.
Definition 2 (Refinement Type Optimization). Let D be a program, ≺ bea strict partial order on predicate substitutions, and Θ = {θ | ` D : θΓD }. A
predicate substitution θ ∈ Θ is called Pareto optimal with respect to ≺ if there
is no θ0 ∈ Θ such that θ0 ≺ θ. A refinement type optimization problem (D, ≺)is a problem to find a Pareto optimal substitution θ ∈ Θ with respect to ≺.
In the remainder of the paper, we will often consider type optimization problems
extended with user-specified constraints and/or templates for some predicate
variables (see Section 4 for examples and Section 5 for formal definitions).
The above definition of type optimization problems is abstract in the sensethat ≺ is only required to be a strict partial order on predicate substitutions. We
below introduce an example concrete order, which is already explained informallyin Section 1 and adopted in our prototype implementation described in Section 7.
The order is defined by two kinds of optimization constraints: the optimization
direction (i.e. minimize/maximize) and the priority order on predicate variables.
Definition 3. Suppose that– P = {P1 , . . . , Pm } is a subset of pvs(ΓD ),– ρ is a map from each predicate variable in P to an optimization direction dthat is either ↑ (for maximization) or ↓ (for minimization), and– @ is a strict total order on P that expresses the priority.2 We below assume
that P1 @ · · · @ Pm .
We define a strict partial order ≺(ρ,@) on predicate substitutions that respects ρand @ as the following lexicographic order:
θ1 ≺(ρ,@) θ2 ⇐⇒ ∃i ∈ {1, . . . , m} . θ1 (Pi ) ≺ρ(Pi ) θ2 (Pi )∧∀j < i. θ1 (Pj ) ≡ρ(Pj ) θ2 (Pj )Here, a strict partial order ≺d and an equivalence relation ≡d on predicates aredefined as follows.
2

If @ were partial, the relation ≺(ρ,@) defined shortly would not be a strict partial
order. Our implementation described in Section 7 uses topological sort to obtain astrict total order @ from a user-specified partial one.

– p1 ≺d p2 ⇐⇒ p1 d p2 ∧ p2 6d p1 ,– p1 ≡d p2 ⇐⇒ p1 d p2 ∧ p2 d p1 ,– λex.φ1 ↑ λe
x.φ2 ⇐⇒|= φ2 ⇒ φ1 , and λe
x.φ1 ↓ λe
x.φ2 ⇐⇒|= φ1 ⇒ φ2 .
Example 1. Recall the function sum and its type template with the predicate
variables P, Q in Section 1. Let us consider optimization constraints ρ(P ) =↑,ρ(Q) =↓, and P @ Q, and predicate substitutions– θ1 = {P 7→ λx. x = 0, Q 7→ λx, y. y = x},– θ2 = {P 7→ λx. >, Q 7→ λx, y. y ≥ 0}, and– θ3 = {P 7→ λx. x < 0, Q 7→ λx, y. ⊥}.
We then have θ2 ≺(ρ,@) θ1 and θ2 ≺(ρ,@) θ3 , because (λx. >) ≺↑ (λx. x = 0) and(λx. >) ≺↑ (λx. x < 0).
tu

4

Applications of Refinement Type Optimization

In this section, we present applications of refinement type optimization to the
problems of proving safety (in Section 4.1) and termination (in Section 4.3), anddisproving safety (in Section 4.4) and termination (in Section 4.2) of programsin the language L. In particular, we discuss precondition inference, namely, inference of most-general characterization of inputs for which a given programsatisfies (or violates) a given safety (or termination) property.
4.1

Proving Safety

We explain how to formalize, as a type optimization problem, a problem ofinferring maximally-weak precondition under which a given program satisfies
a given postcondition. For example, let us consider the following terminating
version of sum.
let rec sum’ x = if x <= 0 then 0 else x + sum’ (x-1)
In our framework, a problem to infer a maximally-weak precondition on the argument x for a postcondition x = sum0 x is expressed as a type optimization problem to infer sum0 ’s refinement type of the form (x : {x | P (x)}) → {y | x = y}under an optimization constraint maximize(P ). Our type optimization method
described in Sections 5.2 and 6 infers the following type.
(x : {x | 0 ≤ x ≤ 1}) → {y | x = y}This type says that the postcondition holds if the actual argument x is 0 or 1.
Example 2 (Higher-Order Function). For an example of a higher-order function,
consider the following.
let rec repeat f n e = if n<=0 then e else repeat f (n-1) (f e)By inferring repeat’s refinement type of the form
(f : (x : {x | P1 (x)}) → {y | P2 (x, y)}) → (n : int) → (e : {e | P3 (n, e)}) → {r | r ≥ 0}
under optimization constraints ρ(P1 ) =↓, ρ(P2 ) = ρ(P3 ) =↑, and P3 @ P2 @ P1 ,our type optimization method obtains(f : (x : {x | x ≥ 0}) → {y | y ≥ 0}) → (n : int) → (e : {e | e ≥ 0}) → {r | r ≥ 0}
Thus, our type optimization method can infer maximally-weak refinement types
for the function arguments of a given higher-order function that are sufficientfor it to satisfy a given postcondition.
tu
4.2

Disproving Termination

In a similar manner to Section 4.1, we can apply type optimization to the problems of inferring maximally-weak precondition for a given program to violate
the termination property. For example, consider the function sum in Section 1.
For disproving termination of sum, we infer sum’s refinement type of the form
(x : {x | P (x)}) → {y | ⊥} under an optimization constraint maximize(P ). Our
type optimization method infers the following type.
(x : {x | x < 0}) → {y | ⊥}The type expresses that sum returns no value (i.e., sum is non-terminating) if
called with an argument x that satisfies x < 0.
Example 3 (Non-Deterministic Function). For an example of non-deterministic
function, let us consider a problem of disproving termination of the following.
let rec f x = let n = read_int () in if n<0 then x else f x
Here, read_int () is a function to get an integer value from the user and ismodeled as ∗∃ in our language L. Note that the termination of f does not dependon the argument x but user inputs n. Our type optimization method successfully
disproves termination of f by inferring a refinement type (x : int) → {y | ⊥}for f and {n | n ≥ 0} for the user inputs n. These types mean that f neverterminates if the user always inputs some non-negative integer.
tu
4.3

Proving Termination

Refinement type optimization can also be applied to bounds analysis for inferring
upper bounds of the number of recursive calls. Our bounds analysis for functional
programs is inspired by a program transformation approach to bounds analysis
for imperative programs [6, 7]. Let us consider sum in Section 1. By inserting
additional parameters i and c to the definition of sum, we obtainlet rec sum_t x i c = if x=0 then 0 else x + sum_t (x-1) i (c+1)

Here, i and c respectively represent the initial value of the argument x and thenumber of recursive calls so far. For proving termination of sum, we infer sum t’s
refinement type of the form
(x : {x | P (x}) → (i : int) → (c : {c | Inv (x, i, c)}) → int
under optimization constraints maximize(P ), minimize(Bnd ), P @ Bnd , andadditional constraints on the predicate variables P, Bnd , Inv∀x, i, c. (Inv (x, i, c) ⇐ c = 0 ∧ i = x)

(4)∀x, i, c. (Bnd (i, c) ⇐ P (x) ∧ Inv(x, i, c))(5)Here, Bnd (i, c) is intended to represent the bounds of the number c of recursive
calls of sum with respect to the initial value i of the argument x. We therefore
assume that Bnd (i, c) is of the form 0 ≤ c ≤ k0 + k1 · i, where k0 , k1 represent
unknown coefficients to be inferred. The constraint (4) is necessary to express themeaning of the inserted parameters i and c. The constraint (5) is also necessary
to ensure that the bounds Bnd (i, c) is implied by a precondition P (x) and aninvariant Inv(x, i, c) of sum. Our type optimization method then infers(x : {x | x ≥ 0}) → (i : int) → (c : {c | x ≤ i ∧ i = x + c}) → int
and Bnd (i, c) ≡ 0 ≤ c ≤ i. Thus, we can conclude that sum is terminating for
any input x ≥ 0 because the number c of recursive calls is bounded from aboveby the initial value i of the argument x.
Interestingly, we can infer a precondition for minimizing the number of recursive calls of sum by replacing the priority constraint P @ Bnd with Bnd @ P ,assuming that Bnd (i, c) is of the form 0 ≤ c ≤ k0 for some unknown constant k0 ,and adding an additional constraint ∃x.P (x) (to avoid a meaningless solution
P (x) ≡ ⊥). In fact, our type optimization method obtains(x : {x | x = 0}) → (i : int) → (c : {c | c = 0}) → int
and Bnd (i, c) ≡ c = 0. Therefore, we can conclude that the minimum number ofrecursive calls is 0 when the actual argument x is 0.
We expect that our bounds analysis for functional programs can further be
extended to infer non-linear upper bounds by adopting ideas from an elaboratetransformation for bounds analysis of imperative programs [6].
4.4

Disproving Safety

We can use the same technique in Section 4.3 to infer maximally-weak precondition for a given program to violate a given postcondition. For example, let us
consider again the function sum. A problem to infer a maximally-weak precondition on the argument x for violating a postcondition sum x ≥ 2 can be reduced
to a problem to infer sum t’s refinement type of the form
(x : {x | P (x)}) → (i : int) → (c : {c | Inv (x, i, c)}) → {y | ¬(y ≥ 2)}

under the same constraints for bounds analysis in Section 4.3. The refinement
type optimization method then obtains(x : {x | 0 ≤ x ≤ 1}) → (i : int) → (c : {c | 0 ≤ x ∧ i = x + c}) → {y | ¬(y ≥ 2)}
and Bnd (i, c) ≡ 0 ≤ c ≤ i. This result says that if the actual argument x is 0 or
1, then sum terminates and returns some integer y that violates y ≥ 2. In otherwords, x = 0, 1 are counterexamples to the postcondition sum x ≥ 2.
We can instead find a minimal-length counterexample path3 violating thepostcondition sum x ≥ 2 by replacing the priority constraint P @ Bnd with
Bnd @ P , assuming that Bnd (i, c) is of the form 0 ≤ c ≤ k0 for some unknown
constant k0 , and adding an additional constraint ∃x.P (x). Our type optimization
method then infers(x : {x | x = 0}) → (i : int) → (c : {c | 0 ≤ x ∧ i = x + c}) → {y | ¬(y ≥ 2)}
and Bnd (i, c) ≡ c = 0. From the result, we can conclude that a minimal-lengthcounterexample path is obtained when the actual argument x is 0.

5

Horn Constraint Optimization and Reduction from
Refinement Type Optimization

We reduce refinement type optimization problems into constraint optimization
problems subject to existentially-quantified Horn clauses [1, 11, 19]. We first formalize Horn constraint optimization problems (in Section 5.1) and then explain
the reduction (in Section 5.2).
5.1

Horn Constraint Optimization Problems

Existentially-Quantified Horn Clause Constraint Sets (∃HCCSs) over QFLIA are
defined as follows.
(∃HCCSs) H ::= {hc 1 , . . . , hc m }(Horn clauses) hc ::= h ⇐ b(heads) h ::= P (et) | φ | ∃ex.(P (et) ∧ φ)e(bodies) b ::= P1 (t1 ) ∧ . . . ∧ Pm (etm ) ∧ φ
We write pvs(H) for the set of predicate variables that occur in H.
A predicate substitution θ for an ∃HCCS H is a map from each P ∈ pvs(H)to a closed predicate λx1 , . . . , xar (P ) .φ. We write ΘH for the set of predicate
substitutions for H. We call a substitution θ is a solution of H if for each hc ∈ H,|= θhc. For a subset Θ ⊆ ΘH , we call a substitution θ ∈ Θ is a Θ-restricted
solution if θ is a solution of H. Our constraint optimization method describedin Section 6 is designed to find a Θ-restricted solution for some Θ consisting of
3Here, minimality is with respect to the number of recursive calls within the path.

substitutions that map each predicate variable to a predicate with a bounded
number of conjunctions and disjunctions. In particular, we often usenoar (P )
Θatom = P 7→ λx1 , . . . , xar (P ) .n0 + Σi=1 ni · xi ≥ 0 | P ∈ pvs(H)consisting of atomic predicate substitutions.
Example 4. Recall the function sum and the predicate substitutions θ1 , θ2 , θ3 in
Example 1. Our method reduces a type optimization problem for sum into a
constraint optimization problem for the following HCCS Hsum (the explanationof the reduction is deferred to Section 5.2).

Q(x, 0) ⇐ P (x) ∧ x = 0, P (x − 1) ⇐ P (x) ∧ x 6= 0,
Q(x, x + y) ⇐ P (x) ∧ Q(x − 1, y) ∧ x 6= 0
Here, θ1 is a solution of Hsum , and θ2 and θ3 are Θatom -restricted solutions of
Hsum . If we fix Q(x, y) ≡ ⊥ (i.e., infer sum’s type of the form (x : {x | P (x)}) →{y | ⊥}) for disproving termination of sum as in Section 4.2, we obtain the fol⊥lowing HCCS Hsum.
{⊥ ⇐ P (x) ∧ x = 0, P (x − 1) ⇐ P (x) ∧ x 6= 0}⊥
Hsum
has, for example, Θatom -restricted solutions {P 7→ λx.x < 0} and {P

λx.x < −100}.

7→tu

We now define Horn constraint optimization problems for ∃HCCSs.
Definition 4. Let H be an ∃HCCS and ≺ be a strict partial order on predicate
substitutions. A solution θ of H is called Pareto optimal with respect to ≺ ifthere is no solution θ0 of H such that θ0 ≺ θ. A Horn constraint optimization
problem (H, ≺) is a problem to find a Pareto optimal solution θ with respect to≺. A Θ-restricted Horn constraint optimization problem is a Horn constraint
optimization problem with the notion of solutions replaced by Θ-restricted solutions.
Example 5. Recall Hsum and its solutions θ1 ,θ2 ,θ3 in Example 1. Let us consider aHorn constraint optimization problem (Hsum , ≺(ρ,@) ) where ρ(P ) = ↑, ρ(Q) = ↓,and Q @ P . We have θ3 ≺(ρ,@) θ1 and θ3 ≺(ρ,@) θ2 . In fact, θ3 is a Pareto
optimal solution of Hsum with respect to ≺(ρ,@) .
tu
In general, an ∃HCCS H may not have a Pareto optimal solution with respect to ≺(ρ,@) even though H has a solution. For example, consider a Hornconstraint optimization problem (Hsum , ≺(ρ,@) ) where ρ(P ) =↑, ρ(Q) =↓, andis notP @ Q. Because the semantically optimal solution Q(x, y) ≡ y = x(x+1)
2expressible in QFLIA, it must be approximated, for example, as Q(x, y) ≡ y ≥0 ∧ y ≥ x ∧ y ≥ 2x − 1. The approximated solution, however, is not Pareto
optimal because we can always get a better approximation like Q(x, y) ≡ y ≥0 ∧ y ≥ x ∧ y ≥ 2x − 1 ∧ y ≥ 3x − 3 if we use more conjunctions.
We can, however, show that an ∃HCCS has a Θatom -restricted Pareto optimal
solution with respect to ≺(ρ,@) if it has any Θatom -restricted solution. Interested
readers are referred to the extended version [8]. For the above example, θ2 in
Example 1 is a Θatom -restricted Pareto optimal solution.

1: procedure Optimize(H, ≺)2:
match Solve(H) with
3:
Unknown → return Unknown
4:| NoSol → return NoSol
5:| Sol (θ0 ) →6:θ := θ0 ;7:
while true do
8:
let H0 = Improve≺ (θ, H) in
9:
match Solve(H0 ) with
10:
Unknown → return Sol (θ)
11:| NoSol → return OptSol (θ)
12:| Sol (θ0 ) → θ := θ0
13:
end
Fig. 3. Pseudo-code of the constraint optimization method for ∃HCCSs

5.2

Reduction from Refinement Type Optimization

Our method reduces a refinement type optimization problem into an Horn constraint optimization problem in a similar manner to the previous refinement
type inference method [18]. Given a program D, our method first prepares arefinement type template ΓD of D as well as, for each expression of the form
let x = ∗∃ in e, a refinement type template {x | P (ey , x)} of x, where P is a fresh
predicate variable and ye is the sequence of all the integer variables in the scope.
Our method then generates an ∃HCCS by type-checking D against ΓD and collecting the proof obligations of the forms JΓ K ∧ φ1 ⇒ φ2 and JΓ K ⇒ ∃ν.φ respectively from each application of the rules ISub and Rand∃. We write Gen(D, ΓD )to denote the ∃HCCS thus generated from D and ΓD .
We can show the soundness of our reduction in the same way as in [18].
Theorem 3 (Soundness of Reduction). Let (D, ≺) be a refinement type optimization problem and ΓD be a refinement type template of D. If θ is a Pareto
optimal solution of Gen(D, ΓD ), then θ is a solution of (D, ≺).

6

Horn Constraint Optimization Method

In this section, we describe our Horn constraint optimization method for ∃HCCSs.
The method repeatedly improves a current solution until convergence. The pseudocode of the method is shown in Figure 3. The procedure Optimize for Horn constraint optimization takes a (Θ-restricted) ∃HCCS optimization problem (H, ≺)and returns any of the following: Unknown (which means the existence of a solution is unknown), NoSol (which means no solution exists), Sol (θ) (which meansθ is a possibly non-Pareto optimal solution), or OptSol (θ) (which means θ is a
Pareto optimal solution). The sub-procedure Solve for Horn constraint solving
takes an ∃HCCS H and returns any of Unknown, NoSol, or Sol (θ). The detailed
description of Solve is deferred to Section 6.1.

Optimize first calls Solve to find an initial solution θ0 of H (line 2). Optimize returns Unknown if Solve returns Unknown (line 3) and NoSol if Solvereturns NoSol (line 4). Otherwise (line 5), Optimize repeatedly improves a current solution θ starting from θ0 until convergence (lines 6 – 13). To improve θ,
we call a sub-procedure Improve≺ (θ, H) that generates an ∃HCCS H0 from H
by adding constraints that require any solution θ0 of H0 satisfies θ0 ≺ θ (line 8).
Optimize then calls Solve to find a solution of H0 . If Solve returns Unknown,
Optimize returns Sol (θ) as a (possibly non-Pareto optimal) solution (line 10). If
Solve returns NoSol, it is the case that no improvement is possible, and hence
the current solution θ is Pareto optimal. Thus, Optimize returns OptSol (θ) (line11). Otherwise, we obtain an improved solution θ0 ≺ θ (line 12). Optimize thenupdates the current solution θ with θ0 and repeats the improvement process.
⊥
Example 6. Recall Hsumin Example 4 and consider an optimization problem
⊥⊥(Hsum , ≺(@,ρ) ) where ρ(P ) =↑. We below explain how Optimize Hsum, ≺(@,ρ)proceeds. First, Optimize calls Solve and obtains an initial solution, e.g., θ0 =⊥⊥. Optimize then calls Improve≺(@,ρ) (θ0 , Hsum
) and obtains{P 7→ λx.⊥} of Hsum0⊥an ∃HCCS H = Hsum ∪{P (x) ⇐ ⊥, ∃x.¬(P (x) ⇒ ⊥)} that requires any solution
θ of H0 satisfies θ(P ) ≺ρ(P ) θ0 (P ) = λx.⊥. Optimize then calls Solve(H0 ) andobtains an improved solution, e.g., θ1 = {P 7→ λx.x < 0}. In the next iteration,⊥
Optimize returns θ1 as a Pareto optimal solution because Improve≺ (θ1 , Hsum)
has no solution.
tu

We now discuss properties of the procedure Optimize under the assumptionof the correctness of the sub-procedure Solve (i.e., θ is a Θ-restricted solution of
H if Solve(H) returns Sol (θ), and H has no Θ-restricted solution if Solve(H)returns NoSol ). The following theorem states the correctness of Optimize.
Theorem 4 (Correctness of the Procedure Optimize). Let (H, ≺) be a
Θ-restricted Horn constraint optimization problem. If Optimize(H, ≺) returns
OptSol(θ) (resp. Sol(θ)), θ is a Pareto optimal (resp. possibly non-Pareto optimal) Θ-restricted solution of H with respect to ≺.
The following theorem states the termination of Optimize for Θatom -restricted
Horn constraint optimization problems.
Theorem 5 (Termination of the Procedure Optimize). Let (H, ≺(@,ρ) )be a Θatom -restricted Horn constraint optimization problem. Suppose that(a) for any P such that ρ(P ) =↓, P is not existentially quantified in H and(b) if Solve returns θ, for any P , θP defined as θ {P 7→ λex.φ} (where φ ≡ >if ρ(P ) =↑ and φ ≡ ⊥ if ρ(P ) =↓) is either not a solution or θP 6≺(@,ρ) θ.
It then follows that Optimize(H, ≺(@,ρ) ) always terminates.
6.1

Sub-Procedure Solve for Solving ∃HCCSs

The pseudo-code of the sub-procedure Solve for solving ∃HCCSs is presented
in Figure 4. Here, Solve uses existing template-based invariant generation techniques based on Farkas’ lemma [3, 7] and ∃HCCS solving techniques based on

1: procedurenSolve(H)
2:

3:
4:
5:
6:
7:
8:
9:
10:
11:
12:

o
ar (P )
P 7→ λex.c0 + Σi=1 ci · xi ≥ 0 | P ∈ pvs(H) inV
let ∃ec.∀ex.∃ey .φ = ∃ec. hc∈H ∀fvs(hc).θ(hc) inlet ∃ec, ze.∀ex.φ0 = apply Skolemization to ∃e
c.∀e
x.∃e
y .φ inlet ∃ec, ze, w.φe 00 = apply Farkas’ lemma to ∃ec, ze.∀ex.φ0 inmatch SMT(φ00 ) withSat(σ) → return Sol (σ(θ))| Unknown| Unsat → match SMT(∀ex.∃ey .φ) with
Unsat → return NoSol| Unknown → return Unknown| Sat(σ) → return Sol (σ(θ))
let θ =

Fig. 4. Pseudo-code of the constraint solving method for ∃HCCSs based on templatebased invariant generation

Skolemization [1, 11, 19]. Solve first generates a template substitution θ thatmaps each predicate variable in pvs(H) to a template atomic predicate with unknown coefficients c0 , . . . , car (P ) (line 2).4 Solve then applies θ to H and obtains
a verification condition of the form ∃e
c.∀e
x.∃e
y .φ without predicate variables (line3). Solve applies Skolemization [1, 11, 19] to the condition and obtains a simplified condition of the form ∃ec, ze.∀ex.φ0 (line 4). Solve further applies Farkas’lemma [3, 7] to eliminate the universal quantifiers and obtains a condition of
the form ∃ec, ze, w.φe 00 (line 5). Solve then uses an SMT solver that supports thequantifier-free theory of non-linear integer arithmetic (QFNIA) to find a satisfying assignment to φ00 (line 6). If such an assignment σ is found, Solve returns
σ(θ) as a solution (line 7). Otherwise (no assignment is found),5 Solve uses
an SMT solver that supports the quantified theory of non-linear integer arithmetic (NIA) to check the absence of a Θatom -restricted solution by checking theunsatisfiability of ∀ex.∃ey .φ (line 9). Solve returns NoSol if Unsat is returned(line 10) and Unknown if Unknown is returned (line 11). Otherwise (a satisfying
assignment σ is found), Solve returns σ(θ) as a solution (line 12).
Example 7. We explain how Solve proceeds for H0 in Example 6. Solve first
generates a template substitution θ = {P 7→ λx.c0 + c1 · x ≥ 0} with unknown
coefficients c0 , c1 and applies θ to H0 . As a result, we get a verification condition (⊥ ⇐ c0 + c1 · x ≥ 0 ∧ x = 0) ∧∀x.
∧(c0 + c1 · (x − 1) ≥ 0 ⇐ c0 + c1 · x ≥ 0 ∧ x 6= 0)∃c0 , c1 . ∃x. c0 + c1 · x ≥ 0
4

The presented code here is thus specialized to solve Θatom -restricted Horn constraint
optimization problems. To solve Θ-restricted optimization problems for other Θ, weneed here to generate templates that conform to the shape of substitutions in Θ
instead. Our implementation in Section 7 iteratively increases the template size.
5
Note here that even though no assignment is found, H may have a Θatom -restricted
solution because Farkas’ lemma is not complete for QFLIA formulas [3, 7] andSkolemization of ∃e
c.∀e
x.∃e
y .φ into ∃ec, ze.∀ex.φ0 here assumes that ye are expressed aslinear expressions over xe [1, 11, 19].

By applying Farkas’ lemma, we obtain∃w1 , w2 , w3 ≥ 0. 
(c0 · w1 ≤ −1 ∧ c1 · w1 + w2 − w3 = 0) ∧  ∃w4 , w5 , w6 ≥ 0. (−1 − c0 + c1 ) · w4 + c0 · w5 − w6 ≤ −1 ∧ ∧ 


c
·
(−w
+
w
)
+
w
=
0
4
5
6
 1
 
∃c0 , c1 . 


(−1
−
c
+
c
)
·
w
+
c
·
w
−
w
≤
−1
∧
0
1
7
0
8
9
 ∃w7 , w8 , w9 ≥ 0.
∧
c1 · (−w7 + w8 ) − w9 = 0∃x. c0 + c1 · x ≥ 0
By using an SMT solver, we obtain, for example, a satisfying assignment σsuch that σ(c0 ) = σ(c1 ) = −1, σ(w1 ) = σ(w2 ) = σ(w5 ) = σ(w6 ) = σ(w7 ) =σ(w9 ) = 1, and σ(w3 ) = σ(w4 ) = σ(w8 ) = 0. Thus, Solve returns σ(θ) ={P 7→ λx. − 1 − x ≥ 0} ≡ θ1 in Example 6.
tu
The following theorem states the correctness of the sub-procedure Solve.
Lemma 1 (Correctness of the Sub-Procedure Solve). Let H be an ∃HCCS.
θ is a Θatom -restricted solution of H if Solve(H) returns Sol(θ), and H has noΘatom -restricted solution if Solve(H) returns NoSol.

7

Implementation and Experiments

We have implemented a prototype refinement type optimization tool for OCaml
based on the method presented in this paper. Our tool uses Z3 (https://z3.
codeplex.com/) as its underlying SMT solver. We conducted preliminary experiments on a machine with Intel Core i7-3770 3.40GHz, 16GB of RAM.
The experimental results are sum- Table 1. The results of a non-termination
marized in Tables 1 and 2. Ta- verification benchmark set used in [2,11,13].
ble 1 shows the results of an existing
Verified TimeOut Other
first-order non-termination verificaOur tool
41
27
13
tion benchmark set used in [2,11,13].
CppInv [13]7065Because the original benchmark set T2-TACAS [2]51
030
was written in the input language of
MoCHi [11]4826
7
T2 (http://mmjb.github.io/T2/),
TNT [4]19
359
we used an OCaml translation of thebenchmark set provided by [11]. The results for CppInv, T2-TACAS, and TNT
are according to Larraz et al. [13]. The result for MoCHi is according to [11].
Our tool was able to successfully disprove termination of 41 programs (out of81) in the time limit of 100 seconds. Our prototype tool was not the best but
performed reasonably well compared to the state-of-the-art tools dedicated to
non-termination verification.
Table 2 shows the results of maximally-weak precondition inference for proving safety (P/S) and termination (P/T), and disproving safety (D/S) and termination (D/T). We used non-termination (resp. termination) verification benchmarks for higher-order functional programs from [11] (resp. [12]). The column“#I” shows the number of optimization iterations, and the column “Time” shows
the running time in seconds. The column “Op.” shows whether Pareto optimal

Table 2. The results of maximally-weak precondition inference.
Program App. #I Time Op.
ProgramApp.
#I Time Op.
fixpoint [11] D/T 1 0.300 3
append [12]P/T
10 10.664 3?
fib_CPS [11] D/T 1 7.083 3?
zip [12]P/T
3 12.236
indirect_e [11] D/T 1 0.344 3 repeat (Sec.4.1)
P/S
4 0.948 3?
0
indirectHO_e [11] D/T 1 0.312 3
sum (Sec.4.1)
P/S
2 0.036 3
loopHO [11] D/T 1 16.094 3?
sum (Sec.4.2)
D/T
1 0.174 3
foldr [11] D/T 3 8.048 3
sum t (Sec.4.3) P/T(P @ Bnd ) 5 12.028 3?
sum_geq3 P/S 4 2.654 3? sum t (Sec.4.3) P/T(Bnd @ P ) 2 15.504 3?
append P/S 5 3.608 3? sum t (Sec.4.4) D/S(P @ Bnd ) 4 12.020 3?
fib D/T 1 0.039 3
sum t (Sec.4.4) D/S(Bnd @ P ) 1 20.780 3?

refinement types are inferred: 3(resp. 3? ) indicates that the Pareto optimalityof inferred types is checked automatically by our tool (resp. manually by us).
The results show that our prototype tool is reasonably efficient for proving safety(P/S) and disproving termination (D/T) of higher-order functions. Further engineering work, however, is required to make the tool more efficient for proving
termination (P/T) and disproving safety (D/S).

8

Related Work

Type inference problems for refinement type systems [5, 20] have been intensively studied [9, 10, 15–19]. To our knowledge, this paper is the first to address
type optimization problems, which generalize ordinary type inference problems.
As we saw in Sections 4 and 7, this generalization enables significantly wider
applications in the verification of higher-order functional programs.
For imperative programs, Gulwani et al. have proposed a template-based
method to infer maximally-weak pre and maximally-strong post conditions [7].
Their method, however, cannot directly handle higher-order functional programs, (angelic and demonic) non-determinism in programs, and prioritized
multi-objective optimization, which are all handled by our new method.
Internally, our method reduces a type optimization problem to a constraint
optimization problem subject to an existentially quantified Horn clause constraint set (∃HCCS). Constraint solving problems for ∃HCCSs have been studied
by recent work [1, 11, 19]. They, however, do not address constraint optimization
problems. The goal of our constraint optimization is to maximize/minimize theset of the models for each predicate variable occurring in the given ∃HCCS. Thus,
our constraint optimization problems are different from Max-SMT [14] problems
whose goal is to minimize the sum of the penalty of unsatisfied clauses.

9

Conclusion

We have generalized refinement type inference problems to type optimization
problems, and presented interesting applications enabled by type optimization
to inferring most-general characterization of inputs for which a given functional
program satisfies (or violates) a given safety (or termination) property. We havealso proposed a refinement type optimization method based on template-based
invariant generation. We have implemented our method and confirmed by experiments that the proposed method is promising for the applications.

References
1. T. A. Beyene, C. Popeea, and A. Rybalchenko. Solving existentially quantified
horn clauses. In CAV ’13, volume 8044 of LNCS, pages 869–882. Springer, 2013.
2. H. Y. Chen, B. Cook, C. Fuhs, K. Nimkar, and P. W. O’Hearn. Proving nontermination via safety. In TACAS ’14, volume 8413 of LNCS, pages 156–171. Springer,
2014.
3. M. A. Colón, S. Sankaranarayanan, and H. B. Sipma. Linear invariant generation
using non-linear constraint solving. In CAV ’03, volume 2725 of LNCS, pages
420–432. Springer, 2003.
4. F. Emmes, T. Enger, and J. Giesl. Proving non-looping non-termination automatically. In IJCAR ’12, volume 7364 of LNCS, pages 225–240. Springer, 2012.
5. T. Freeman and F. Pfenning. Refinement types for ML. In PLDI ’91, pages
268–277. ACM, 1991.
6. S. Gulwani, K. K. Mehra, and T. Chilimbi. SPEED: Precise and efficient static
estimation of program computational complexity. In POPL ’09, pages 127–139.
ACM, 2009.
7. S. Gulwani, S. Srivastava, and R. Venkatesan. Program analysis as constraint
solving. In PLDI ’08, pages 281–292. ACM, 2008.
8. K. Hashimoto and H. Unno. Refinement type inference via horn constraint optimization. An extended version, available from http://www.cs.tsukuba.ac.jp/~uhiro/, 2015.
9. R. Jhala, R. Majumdar, and A. Rybalchenko. HMC: verifying functional programs
using abstract interpreters. In CAV ’11, volume 6806 of LNCS, pages 470–485.
Springer, 2011.
10. N. Kobayashi, R. Sato, and H. Unno. Predicate abstraction and CEGAR for
higher-order model checking. In PLDI ’11, pages 222–233. ACM, 2011.
11. T. Kuwahara, R. Sato, H. Unno, and N. Kobayashi. Predicate abstraction and CEGAR for disproving termination of higher-order functional programs. In CAV’15,
LNCS. Springer, 2015.
12. T. Kuwahara, T. Terauchi, H. Unno, and N. Kobayashi. Automatic termination
verification for higher-order functional programs. In ESOP ’14, volume 8410 of
LNCS, pages 392–411. Springer, 2014.
13. D. Larraz, K. Nimkar, A. Oliveras, E. Rodrı́guez-Carbonell, and A. Rubio. Proving
non-termination using max-SMT. In CAV ’14, volume 8559 of LNCS, pages 779–
796. Springer, 2014.
14. R. Nieuwenhuis and A. Oliveras. On SAT modulo theories and optimization problems. In SAT ’06, volume 4121 of LNCS, pages 156–169. Springer, 2006.
15. P. Rondon, M. Kawaguchi, and R. Jhala. Liquid types. In PLDI ’08, pages 159–169.
ACM, 2008.
16. T. Terauchi. Dependent types from counterexamples. In POPL ’10, pages 119–130.
ACM, 2010.
17. H. Unno and N. Kobayashi. On-demand refinement of dependent types. In FLOPS’08, volume 4989 of LNCS, pages 81–96. Springer, 2008.
18. H. Unno and N. Kobayashi. Dependent type inference with interpolants. In PPDP
’09, pages 277–288. ACM, 2009.
19. H. Unno, T. Terauchi, and N. Kobayashi. Automating relatively complete verification of higher-order functional programs. In POPL ’13, pages 75–86. ACM,
2013.
20. H. Xi and F. Pfenning. Dependent types in practical programming. In POPL ’99,
pages 214–227. ACM, 1999.