GUBS Upper Bound Solver (Extended Abstract)

TL;DR

The paper introduces GUBS, a constraint solver for inequalities over naturals, which is integrated into HoSA to analyze the complexity of higher-order functional programs, supported by implementation insights and case studies.

Contribution

It presents GUBS, a novel upper bound solver for natural number inequalities, and demonstrates its application within HoSA for automatic complexity analysis of higher-order programs.

Findings

GUBS effectively solves inequalities involving uninterpreted functions and arithmetic.

Integration of GUBS into HoSA enables automatic complexity analysis.

Case studies validate GUBS's practical utility.

Abstract

In this extended abstract we present the GUBS Upper Bound Solver. GUBS is a dedicated constraint solver over the naturals for inequalities formed over uninterpreted function symbols and standard arithmetic operations. GUBS now forms the backbone of HoSA, a tool for analysing space and time complexity of higher-order functional programs automatically. We give insights about the implemen- tation and report different case studies.

Tables

Table 1. Table 1 : Experimental evaluation conducted with GUBS .

	inc	inc+simp	inc+simp+scc
SAT(1)	17	17	18
SAT(2)	2	4	3
SAT(3)	0	0	1
Timeout	3	1	0

Equations

$$a,b\mathrel{::=}x\mid n\mid a\oplus b\mid\mathtt{f}(a_{\_}1,\dots,a_{\_}{\mathsf{ar}(\mathtt{f})})\hbox to0.0pt{$\;$.\hss}$$

$$\mathtt{r}(\mathtt{n},y)$$

$$\mathtt{r}_{\mathcal{M}}(\mathtt{n}_{\mathcal{M}},y)=1\geqslant 1\quad\text{and}\quad\mathtt{r}_{\mathcal{M}}(\mathtt{c}_{\mathcal{M}}(x,y),z)=y+1\geqslant 1+y=1+\mathtt{r}(y,\mathtt{c}(x,z))\hbox to0.0pt{$\;$.\hss}$$

$$\llbracket a\rrbracket_{\mathcal{M}}^{\alpha}=\begin{cases}\alpha(a)&\text{ if }a\in\mathcal{V}\hbox to0.0pt{$\;$,\hss}\\ a&\text{ if }a\in\mathbb{N}\hbox to0.0pt{$\;$,\hss}\\ \llbracket a_{\_}1\rrbracket_{\mathcal{M}}^{\alpha}\oplus_{\_}\mathbb{N}\llbracket a_{\_}2\rrbracket_{\mathcal{M}}^{\alpha}&\text{ if }a=a_{\_}1\oplus a_{\_}2\text{ and }{\oplus}\in\{+,*,\max\}\hbox to0.0pt{$\;$,\hss}\\ \mathtt{f}_{\mathcal{M}}(\llbracket a_{\_}1\rrbracket_{\mathcal{M}}^{\alpha},\ldots,\llbracket a_{\_}n\rrbracket_{\mathcal{M}}^{\alpha}),&\text{ if }a=\mathtt{f}(a_{\_}1,\ldots,a_{\_}n)\text{ and }\mathtt{f}\in\mathcal{F}\hbox to0.0pt{$\;$.\hss}\end{cases}$$

$$\mathtt{f}_{\mathcal{A}}(x,y)=\max(\mathsf{c_{\_}1}\cdot x+\mathsf{c_{\_}2}\cdot y+\mathsf{c}_{\_}3,\mathsf{d_{\_}1}\cdot x+\mathsf{d_{\_}2}\cdot y+\mathsf{c}_{\_}3)\hbox to0.0pt{$\;$.\hss}$$

$$e\ge C[\max (f_{\_}1,f_{\_}2)]$$

$$C[\max (e_{\_}1,e_{\_}2)]\ge f$$

Full text

1 Introduction

Synthesizing functions that obey certain constraints in the form of (in)equalities is a fundamental task in program analysis. For instance, in the context of termination and complexity analysis. To this end, the program verification community predominantly adopts techniques either based on LP solvers [11], or dedicated tools like PUBS [2]. The former approach is usually restricted to the synthesis of linear functions. The latter approach is based on solving recurrence relations and particularly useful for the synthesis of ranking functions in the context of imperative programs. Recurrence relations are limited in scope however, for instance, function composition cannot be directly expressed.

To overcome these restrictions, we have developed the GUBS Upper Bound Solver (GUBS for short). Given a set of inequalities over arithmetical expressions and uninterpreted function symbols, GUBS tries to find a model in $\mathbb{N}$, i.e., an interpretation of all the function symbols that make the given inequalities hold. This tool is currently used in our inference machinery for sized-types111See http://cl-informatik.uibk.ac.at/users/zini/software/hosa. and, experimentally, in our complexity tool TCT222See http://cl-informatik.uibk.ac.at/software/tct. for the synthesis of specific ranking function. GUBS itself is heavily inspired by methods developed for synthesising linear and non-linear interpretations in the context of rewriting. The main novel aspect of GUBS is the modular approach it rests upon, inspired by the framework underlying TCT. To date, it incorporates an adaption of the synthesis technique from [6] which reduces polynomial inequalities to SMT (with respect to the theory of quantifier free non-linear integer arithmetic), various syntactic simplification techniques and a per-SCC analysis. GUBS is open source and available from

https://github.com/ComputationWithBoundedResources/gubs .

Although developed foremost for the complexity analysis of (higher-order) rewrite systems, we are convinced that GUBS has potential applications outside rewriting. E.g., for the synthesis of ranking functions, the inference of certain dependent type systems such as the one of Dal Lago and Petit [5], the complexity analysis of concurrent programs as in [8], or various systems developed by the implicit computational complexity community (we name just [4]).

In the following we briefly outline our tool GUBS. More specific, we introduce the problem tackled by GUBS formally, we outline the central synthesis techniques and report on the experience that we have collected so far.

2 Constraint System over the Naturals

Let $\mathcal{V}$ denote a countably infinite set of variables, and let $\mathcal{F}$ denote a signature, i.e., a set of function symbols, disjoint from $\mathcal{V}$. Each function symbol $\mathtt{f}\in\mathcal{F}$ is equipped with a natural number $\mathsf{ar}(\mathtt{f})$, its arity. We use $x,y,\dots$ to denote variables, whereas $\mathtt{f},\mathtt{g},\dots$ denote function symbols. The set of arithmetical terms $\mathcal{T}(\mathcal{F},\mathcal{V})$ over function symbols $\mathcal{F}$ and variables $\mathcal{V}$ is generated inductively from $x\in\mathcal{V}$, $\mathtt{f}\in\mathcal{F}$, $n\in\mathbb{N}$ and pre-defined arithmetical operations ${\oplus}\in\{+,*,\max\}$ according to the following grammar:

[TABLE]

A constraint system $\mathcal{C}$ (over $\mathbb{N}$) is a finite set of constraints $a\geqslant b$.

Informally, a constraint system $\mathcal{C}$ is satisfiable if we can interpret each symbol $\mathtt{f}\in\mathcal{F}$ with a function $\mathtt{f}_{\mathcal{M}}\mathrel{\colon}\mathbb{N}^{\mathsf{ar}(\mathtt{f})}\to\mathbb{N}$ such that all constraints in $\mathcal{C}$ hold. Here, constraints and arithmetical operations are interpreted in the natural way. Consider for instance the constraint system $\mathcal{C}_{\_}1$ consisting of the following two constraints:

[TABLE]

This system is satisfiable, for instance, by taking $\mathtt{n}_{\mathcal{M}}=1$, $\mathtt{r}_{\mathcal{M}}(x,y)=x$ and $\mathtt{c}_{\mathcal{M}}(x,y)=y+1$, as we have

[TABLE]

More formally, an interpretation $\mathcal{M}$ over symbols $\mathcal{F}$ (into the naturals) is a mapping that assigns to each symbol $\mathtt{f}\in\mathcal{F}$ a function $\mathtt{f}_{\mathcal{M}}\mathrel{\colon}\mathbb{N}^{\mathsf{ar}(\mathtt{f})}\to\mathbb{N}$. Let ${\oplus_{\_}\mathbb{N}}\mathrel{\colon}\mathbb{N}^{2}\to\mathbb{N}$ for ${\oplus}\in\{{+},{*},{\max}\}$ denote addition, multiplication and the maximum function on natural numbers, respectively. The interpretation $\llbracket t\rrbracket_{\mathcal{M}}^{\alpha}$ of a term $t\in\mathcal{M}$ with respect to $\mathcal{M}$ and variable assignment $\alpha\colon\mathcal{V}\to\mathbb{N}$ is then defined in the expected way:

[TABLE]

We say that $\mathcal{M}$ is a model of a constraint system $\mathcal{C}$, in notation $\mathcal{M}\models\mathcal{C}$, if $\llbracket a\rrbracket_{\mathcal{M}}^{\alpha}\geqslant_{\_}\mathbb{N}\llbracket b\rrbracket_{\mathcal{M}}^{\alpha}$ holds for all assignments $\alpha$ and constraints $a\geqslant b\in\mathcal{C}$. For instance, we have $\mathcal{M}\models\mathcal{C}_{\_}1$ for the constraint system $\mathcal{C}_{\_}1$ and interpretation $\mathcal{M}$ depicted above. With our tool GUBS, we give a sound, but necessarily incomplete procedure to the following undecidable problem.

Definition 1** (Model Synthesis).**

Given a constraint system $\mathcal{C}$, the model synthesis problem asks for an interpretation $\mathcal{M}$ with $\mathcal{M}\models\mathcal{C}$.

3 Implementation

GUBS is written in the functional programming language Haskell. The source contains approximately 2000 lines of code, spread over 25 modules. GUBS comes along as a stand-alone executable as well as a Haskell library. For usage information and installation instructions, we kindly refer the reader to the homepage of GUBS. Here, we just provide a short outline of the central methods implemented in GUBS.

Synthesis of Models via SMT.

Conceptually, we follow the method presented in [6]. In this approach, each $k$-ary symbol $\mathtt{f}\in\mathcal{F}$ is associated with a template max-polynomial, i.e., an expression over $k$ variables and connectives $\{{+},{*},{\max}\}$, and undetermined coefficient variables $\vec{\mathsf{c}}$. For instance, a linear template for a binary symbol $\mathtt{f}$ employed by GUBS is

[TABLE]

To find a concrete model based on these templates, we search for a solution to $\exists\vec{\mathsf{c}}.\ \bigwedge_{\_}{a\geqslant b\in\mathcal{C}}\forall\vec{x}\in\mathcal{V}.\ \llbracket a\rrbracket_{\mathcal{M}}^{\mathcal{A}}\geq\llbracket b\rrbracket_{\mathcal{M}}^{\mathcal{A}}$, in two steps. First, we eliminate $\max$ according to the following rules.

[TABLE]

Notice that this elimination procedure is sound as our max-polynomial algebra allows the formation of weakly monotone expressions only. Once all occurrences of $\max$ are eliminated, we reduce the resulting formula to diophantine constraints over the coefficient variables $\vec{\mathsf{c}}$, via the so called absolute positiveness check, see also [6]. The diophantine constraints are then given to an SMT-solver that supports quantifier-free non-linear integer arithmetic, from its assignment and the initially fixed templates GUBS then computes concrete interpretations. To get more precise bounds, GUBS minimises the obtained model by making use of the incremental features of current SMT-solvers, essentially by putting additional constraints on coefficients.

Limitations: The main limitation of this approach is that the shape of interpretations is fixed to that of the templates, noteworthy, the degree of the interpretation is fixed in advance. As the complexity of the absolute positiveness check depends not only on the size of the given constraint system but to a significant extend also on the degree of interpretation functions, our implementation searches iteratively for interpretations of increasing degree.

Also notice that our max-elimination procedure is incomplete, for instance, it cannot deal with the constraint $\max(2x,2y)\geqslant x+y$, which is reduced to $2x\geqslant x+y\lor 2y\geqslant x+y$. In contrast, in [7] a complete procedure is proposed. However, our experimental assessment concluded that this encoding introduces too many auxiliary variables, which turned out as a significant bottleneck of the overall procedure.

Separate SCC Analysis.

Synthesis of models via SMT gets impractical on large constraint systems. To overcome this, GUBS divides the given constraint system $\mathcal{C}$ into its strongly connected components (SCCs for short) $\mathcal{C}_{\_}1,\dots,\mathcal{C}_{\_}n$, topologically sorted, and finds a model for each SCC $\mathcal{C}_{\_}i$ iteratively. Here, the underlying call graph is formed as follows. The nodes are given by the constraints in $\mathcal{C}$. Let $a_{\_}1\geqslant b_{\_}1$ to $a_{\_}2\geqslant b_{\_}2$ be two constraints in $\mathcal{C}$, where wlog. $a_{\_}1=C[\mathtt{f_{\_}1}(\vec{a_{\_}1}),\dots,\mathtt{f_{\_}n}(\vec{a_{\_}n})]$ for a context $C$ without function symbols. Then there is an edge from $a_{\_}1\geqslant b_{\_}1$ to $a_{\_}2\geqslant b_{\_}2$ if any of the symbols occurring in $\vec{a_{\_}1},\dots,\vec{a_{\_}n},b_{\_}1$ occurs in $a_{\_}2$. The intuition is that once we have found a model for all the successors of $a_{\_}1\geqslant b_{\_}1$, we can interpret the terms $\vec{a_{\_}i}$ and $b_{\_}1$ within this model. We can then extend this model by finding a suitable interpretation for $\mathtt{f_{\_}1},\dots,\mathtt{f_{\_}n}$, thereby obtaining a model that satisfies $a_{\_}1\geqslant b_{\_}1$.

Syntactical Simplifications.

We apply a series of syntactical complete simplifications that are fast and may reduce the search domain for the SMT solver. For example, instantiation substitutes all variables that occur only on the left-hand side of a constraint with [math]. This reduces the size of the generated abstract polynomials. Elimination fixes the interpretation of function symbols that occur only on the right-hand side of the constraint system to [math]. This reduces the domain of the interpretation. Propagation performs a restricted form of inlining to simplify the constraint system. For instance, given a constraint $\mathtt{f}(x,y)\geqslant x+y$, if $\mathtt{f}$ does not occur on the left-hand side of a different constraint we can fix the model of $\mathtt{f}$ and substitute all $\mathtt{f}$ occurring on the right-hand side of the constraint system.

4 Case Studies

In this section we briefly outline our experience collected so far, in the two contexts where GUBS is currently employed.

Synthesis of Sized-Types.

Various successful approaches to automatic verification of termination properties of higher-order functional programs are based on sized-types [10]. Here, a type carries not only some information about the kind of each object, but also about its size, hence the name. This information is then exploited when requiring that recursive calls are done on arguments of strictly smaller size.

In recent work [3] we have taken a fresh look at sized-types, with particular emphasis towards application in runtime analysis and automation. A result of this work is the tool HoSA, which given a program written in a simple typed higher-order language, annotates all types with size information. GUBS is a central ingredient of HoSA.

Consider the function, prependAll xs ys $=$ map (append xs) ys, which prepends a given list $xs$ to all elements of it second argument $ys$, itself a list of lists. Sized-type inference with HoSA works by first decorating datatypes occurring in the types of functions with size indices, resulting in so called template types, see Figure 1(a). Size indices are annotated here in square brackets. These template types make reference to so far undetermined functions. Inference then amounts simply to type-checking, where however, type-checking emits constraints relating the different size indices. The emitted constraint system is depicted in Figure 1(b) in S-expression notation, the notation expected by GUBS. A model found by GUBS on the resulting constraint system, such as the one depicted in Figure 1(c), is then used to construct concrete sized-types from the initial template types, see Figure 1(d).

It is worthy of note that in this example, the inferred types are precise and thus informative, not least, because of the minimisation techniques incorporated in GUBS, as outlined in Section 3. Also worthy of note, including the time spend by GUBS, the depicted sized-types were found in a quarter of a second, on one of the authors’ laptops.

HoSA is also capable of instrumenting a given program, by threading through the computation a program counter. This way, the runtime of a program is reflected in its sized-type and thus HoSA can give quantitative information on the runtime of programs. HoSA is able to analyse the runtime of a series of examples, fully automatically, which cannot be handled by most competitor methodologies (see e.g., [9]). Noteworthy, HoSA can deal with a variety of examples whose runtime is not linear, e.g., sorting algorithms and non-trivial list functions. GUBS is capable of dealing with reasonably sized constraint systems in this context. For instance, the runtime analysis of the function which computes the cross-product of two lists in quadratic time, itself defined in terms of two folds, relies on 87 functions related by 85 constraints. To this end, GUBS analyses $10$ SCCs individually. The computed bounds are tight, the overall procedure takes just three quarters of a second on this example.

Synthesis of Polynomial Interpretation.

Term rewriting systems (TRSs for short) provide an abstract model of computation that is at the heart of functional and declarative programming. In the last decade termination and resource behaviour of TRSs have been investigated actively. Polynomial interpretation is an elementary method in this context. In its most simple setting, a polynomial interpretation $\mathcal{M}$, i.e. interpretation over polynomials as above, orients a TRS $\mathcal{R}$ if $\llbracket l\rrbracket_{\mathcal{M}}^{\alpha}>_{\_}\mathbb{N}\llbracket r\rrbracket_{\mathcal{M}}^{\alpha}$ holds for all rules $l\to r\in\mathcal{R}$. Together with certain monotonicity constraints on the interpretation, orientability implies termination. When the interpretation of constructors are additionally sufficiently constrained, quantitative information on the runtime of $\mathcal{R}$ can be obtained. Notably, orientation constraints and monotonicity constraints are straight forward translated into a constraint system. Consider for instance the TRS consisting of the two rules depicted in Figure 2(a), corresponding constraints are given in Figure 2(b).

The two constraints on the left enforce the orientation. The first constraint on the right enforces sufficient monotonicity constraints on the interpretation, viz, cons should be monotone in its second argument. The final rule enforces that cons is interpreted by a strongly linear interpretation $cons_{\mathcal{M}}(x,xs)\leqslant x+xs+\texttt{k}$ for some constant $\texttt{k}\in\mathbb{N}$, thereby relating the interpretation of lists linearly to its size. The so computed interpretation is depicted in Figure 2(c) and witnesses that the runtime complexity, i.e., the number of reduction steps as measured in the size of the input list, is linear.

So far, we did not conduct a thorough investigation of the strength of GUBS in this context. We expect however an increase in strength and execution time due to the incorporation of GUBS in TCT.

5 Experimental Evaluation

We conducted preliminary experiments to show the viability of GUBS and the implemented methods. The considered examples are the constraints generated from HoSA for the time and size complexity analysis of a set of functional programs. We performed the experiment with three different strategies: $(i)$ inc repeatedly tries to synthesize a model using abstract templates of an increasing degree up to degree four; $(ii)$ inc+simp additionally applies simplification and minimisation; $(iii)$ inc+simp+scc additionally performs the SCC decomposition.

Table 1 illustrates the summary of the conducted experiment. The details of the experiment are available online333See http://cbr.uibk.ac.at/tools/gubs/experiments. SAT($n$) indicates that a model could be successfully inferred where the maximal degree of the model is $n$, which corresponds in this case to the asymptotic worst-case bounds of the original problem and Timeout indicates that the computation timed-out after $90$ seconds. The strategy inc conceptually corresponds to the current strategy applied in TCT to synthesize polynomial interpretations. We see that the experiments improve with syntactical Simplifications turned on. Furthermore, the full strategy is the only one that finds a model for the insertionsort example.

In particular in the context of rewriting several tools have been established that support constraint solving of diophantine constraints and the synthesis of models of constraint systems. Consider for example, TTT, CiME, Satchmo and AProVE444See http://cl-informatik.uibk.ac.at/software/ttt2, http://cime.lri.fr, https://github.com/jwaldmann/satchmo and http://aprove.informatik.rwth-aachen.de respectively. However, without further consideration a direct comparison is difficult. None of the aforementioned tools can handle the given example systems directly, as the tools are usually tuned for a more specific setting.

6 Conclusion and Future Work

We have described GUBS, an open source tool for synthesising functions over the naturals that satisfy a given set of inequalities. The development of GUBS was motivated by the lack of dedicated constraint solvers for polynomial inequalities.

In future work, we would like to extend GUBS in various directions. In the short term, we would like to improve the methods that are currently implemented. This includes dedicated synthesis techniques for certain subclasses of constraint systems or models, e.g., via reductions to linear programming. It also includes the search for suitable divide-and-conquer methods. Model synthesis is in general not modular, however for certain classes, e.g. disjoint systems, synthesis is modular. The aforementioned SCC analysis is a first step into this direction. Another direction for future work is to extend upon the set of models that can be found in GUBS. Currently, GUBS is only able to synthesise weakly monotone functions over the naturals. It would be interesting, for instance, to include support of integers and rationals, together with non-monotone functions such as subtraction and division. This is clearly feasible with the current toolset underlying GUBS. Finally, and maybe most importantly, we would like to see further applications of our tool.