List of accepted papers
Conrad Rau, David Sabel and Manfred Schmidt-Schauss
Encoding Induction in Correctness Proofs of Program Transformations as a Termination Problem
Abstract:
The diagram-based method to prove correctness of program
transformations consists of computing complete set of (forking and
commuting) diagrams, acting on sequences of standard reductions and
program transformations. In many cases, the only missing step for
proving correctness of a program transformation is to show the
termination of the rearrangement of the sequences. Therefore we
encode complete sets of diagrams as term rewriting systems and use an
automated tool to show termination, which provides a further step in
the automation of the inductive step in correctness proofs.
Bernhard Gramlich and Klaus Györgyfalvay
On Modularity of Termination Properties of Rewriting under Strategies
Abstract:
The modularity of termination and confluence properties of term
rewriting systems has been extensively studied, for disjoint unions
and other more types of combinations. However, for rewriting under
strategies the theory is less well explored. Here we extend the
modularity analysis of termination properties systematically to
(variants of) innermost and outermost rewriting. It turns out — as
expected — that in essence innermost rewriting behaves
nicely w.r.t. modularity of termination properties, whereas this is not
all the case for outermost rewriting, at least not without further
assumptions.
Christian Sternagel and René Thiemann
A Relative Dependency Pair Framework
Abstract:
We present a relative DP framework which generalizes the existing DP framework by allowing weak pairs and strict rules and forms the basis of our proof checker CeTA. The new framework can be used to characterize relative termination using dependency pairs. One of its main features is the possibility to split a DP problem into two DP problems which can be treated independently. By such a split we can easily solve problems that arise when using incomplete termination techniques or techniques like unlabeling which revert the effect of earlier techniques.
Marc Brockschmidt, Thomas Ströder, Carsten Otto and Jürgen Giesl
Proving Non-Termination for Java Bytecode
Abstract:
Recently, we developed an approach for automated termination proofs of Java Bytecode (JBC), which is based on constructing and analyzing termination graphs. These graphs represent all possible program executions in a finite way. In this paper, we show that this approach can also be used to detect non-termination. We implemented our results in the termination prover AProVE and provide experimental evidence for the power of our approach.
Harald Zankl, Sarah Winkler, Aart Middeldorpt
Automating Ordinal Interpretations
Abstract:
In this note we study weakly monotone interpretations for direct proofs
of termination which is sound if the interpretation functions are
``simple''. This is e.g. the case for standard addition and multiplication
of ordinal numbers. We compare the power of such interpretations to
polynomial interpretations over the natural numbers and report on
preliminary experimental results.
Fabian Emmes, Tim Enger and Jürgen Giesl
Detecting Non-Looping Non-Termination
Abstract:
We introduce a technique to prove non-termination of term rewrite systems automatically. In contrast to most previous approaches, our technique is also able to detect non-looping nontermination.
René Thiemann
A Report on the Certification Problem Format
Abstract:
We show how the certification problem format is beneficial for certification of termination proofs. We further highlight some of its design decisions and mention problems that are open for discussion.
Alexander Bau, Tobias Kalbitz, Maria Voigtländer and Johannes Waldmann
Recent Developments in the Matchbox Termination Prover
Abstract:
We report on recent and ongoing work on the Matchbox termination prover: a constraint compiler that transforms
a Boolean-valued Haskell function
into a Boolean satisfiability problem (SAT),a constraint solver for real and arctic
matrix constraints that is using evolutionary
optimization, and is running on massively parallel
(graphics) hardware.
Martin Avanzini, Naohi Eguchi and Georg Moser
On a Correspondence between Predicative Recursion and Register Machines
Abstract:
We present the small polynomial path order sPOP*.
Based on sPOP*, we study a class of rewrite systems, dubbed
systems of predicative recursion of degree d, such that for
rewrite systems in this class we obtain that the runtime complexity
lies in O(n^d). We show that predicative recursive rewrite systems of degree
d define functions computable on a register machine in time O(n^d).
Cristina Borralleras, Miquel Bofill, Enric Rodríguez Carbonell and Albert Rubio
The recursive path and polynomial ordering
Abstract:
In most termination tools two ingredients, namely recursive path
orderings (RPO) and polynomial interpretation orderings (POLO), are
used in a consecutive disjoint way to solve the final constraints
generated from the termination problem.
We present a simple ordering that combines both RPO and
POLO and defines a family of orderings that includes both, and extends
them with the possibility of having, at the same time, an RPO-like
treatment for some symbols and a POLO-like treatment for the others.
The ordering is extended to higher-order terms, providing an
automatable use of polynomial interpretations in combination with
beta-reduction.
Michael Codish, Igor Gonopolskiy, Amir Ben-Amram, Carsten Fuhs and Jürgen Giesl
Termination Analysis via Monotonicity Constraints over the Integers and SAT Solving
Abstract:
We describe an approach for proving termination of programs abstracted
to systems of monotonicity constraints in the integer
domain. Monotonicity constraints are a non-trivial extension of the
size-change termination method. In this setting, termination is PSPACE
complete, hence we focus on a significant subset in NP, which we call
MCNP, designed to be amenable to a SAT-based solution. We use ranking
functions in terms of bounded differences between multisets of
integers. Experiments with our approach as a back-end for termination
analysis of Java Bytecode with AProVE and COSTA as front-ends reveal a
good trade-off between precision and cost of analysis.
Marc Brockschmidt, Richard Musiol, Carsten Otto and Jürgen Giesl
Proving Termination of Java Bytecode with Cyclic Data
Abstract:
In earlier work, we developed a technique to prove termination of Java Bytecode (JBC) automatically: first, JBC programs are automatically transformed to term rewrite systems (TRSs) and then, existing methods and tools are used to prove termination of the resulting TRSs. In this paper, we extend our technique in order to prove termination of algorithms on cyclic data such as cyclic lists or graphs automatically. We implemented our technique in the tool AProVE and performed extensive experiments to evaluate its practical applicability.
Patrick Baillot and Ugo Dal Lago
Higher-Order Interpretations and Program Complexity
Abstract:
Polynomial interpretations and their generalizations like quasi-interpretations have been used in the setting of first-order functional languages to design criteria ensuring statically some complexity bounds on programs This fits in the area of implicit computational complexity, which aims at giving machine-free characterizations of complexity classes. Here we extend this approach to the higher-order setting. For that we consider the notion of simply typed term rewriting systems, we define higher-order polynomial interpretations (HOPI) for them and give a criterion based on HOPIs to ensure that a program can be executed in polynomial time. In order to obtain a criterion which is flexible enough to validate some interesting programs using higher-order primitives, we introduce a notion of polynomial quasi-interpretations,coupled with a simple termination criterion based on linear types and path-like orders.
Beniamino Accattoli and Ugo Dal Lago
On the Invariance of Derivational Complexity for Head Reduction
Abstract:
The lambda-calculus is a widely accepted computational model of higher-order functional programs, yet there is not any direct and universally accepted cost model for it. As a consequence, the computational difficulty of reducing lambda-terms to their normal form is typically studied by reasoning on concrete implementation algorithms. Here, we show that when head reduction is the underlying dynamics, derivational complexity is indeed a reasonable cost model. This improves on known results, which only deal with weak (call-by-value or call-by-name) reduction. Invariance is proved by way of a linear calculus of explicit substitutions, which allows to nicely decompose any head reduction step in the lambda-calculus into more elementary substitution steps, thus making the combinatorics of head-reduction easier to reason about. The technique is also a promising tool to attack what we see as the main open problem, namely understanding for which normalizing strategies derivation complexity is an invariant cost model, if any.
Bertram Felgenhauer
Binomial Interpretations
Abstract:
Polynomial interpretations can be used for proving termination of
term rewrite systems. In this note, we contemplate binomial
interpretations based on binomial coefficients, and show that they
form a suitable basis for obtaining (weakly) monotone algebras. The
main motivation is that this representation covers examples with
negative coefficients like f(x) = 2x² - x + 1, and even some
polynomials with rational coefficients like f(x) = x(x-1)/2 that
map natural numbers to natural numbers.
Thomas Ströder, Fabian Emmes, Peter Schneider-Kamp and Jürgen Giesl
Automated Runtime Complexity Analysis for Prolog by Term Rewriting
Abstract:
For term rewrite systems (TRSs), a huge number of automated termination
analysis techniques have been developed during the last decades, and by
automated transformations of Prolog programs to TRSs, these techniques can
also be used to prove termination of Prolog programs. Very recently,
techniques for automated termination analysis of TRSs have been adapted to
prove asymptotic upper bounds for the runtime complexity of TRSs automatically.
In this paper, we present ongoing work to transform Prolog programs
automatically into TRSs in such a way that the resulting TRSs have at least
the same asymptotic upper complexity bound. Thus, techniques for complexity
analysis of TRSs can be applied to prove upper complexity bounds for Prolog
programs.
Georg Moser and Michael Schaper
Termination Graphs Revisited
Abstract:
We revisit termination graphs from the viewpoint of runtime
complexity. Suitably generalising the construction proposed in the
literature, we define an alternative representation of JBC executions as computation
graphs. We show that the transformation from JBC programs to computation graphs
is sound, that is termination preserving. Moreover, we establish that
the transformation is complexity preserving.
Friedrich Neurauter and Aart Middeldorp
Matrix Interpretations for Polynomial Derivational Complexity
Abstract:
Matrix interpretations can be used to bound the derivational complexity
of term rewrite systems. In general, the obtained bounds are
exponential. In this paper we use joint spectral radius theory in order
to completely characterize matrix interpretations that
induce polynomial upper bounds on the derivational complexity of
(compatible) rewrite systems.