arXiv subjects

Georg Moser

Publications and source records attributed to Georg Moser.

At least 37 records · Page 2Linked to original sources

arXiv2019

The Epsilon Calculus with Equality and Herbrand Complexity

Hilbert's epsilon calculus is an extension of elementary or predicate calculus by a term-forming operator $\varepsilon$ and initial formulas involving such terms. The fundamental results about the epsilon calculus are so-called epsilon theorems, which have been proven by means of the epsilon elimination method. It is a procedure of transforming a proof in epsilon calculus into a proof in elementary or predicate calculus through getting rid of those initial formulas. One remarkable consequence is a proof of Herbrand's theorem due to Bernays and Hilbert which comes as a corollary of extended first epsilon theorem. The contribution of this paper is the upper and lower bounds analysis of the length of Herbrand disjunctions in extended first epsilon theorem for epsilon calculus with equality. We also show that the complexity analysis for Herbrand's theorem with equality is a straightforward consequence of the one for extended first epsilon theorem without equality due to Moser and Zach.

math.LO↗

arXiv2018

Automated Amortised Resource Analysis for Term Rewrite Systems

In this paper we establish an automated amortised resource analysis for term rewrite systems. The method is presented in an annotated type system and gives rise to polynomial bounds on the innermost runtime complexity of the analysed term rewrite system. Our analysis does not restrict the input rewrite system in any way so that rewrite systems may serve as abstractions of first-order, eagerly evaluated functional programs over user-defined inductive data-types. This facilitates integration in a general framework for resource analysis of programs. In particular, we have implemented the method and integrated it into our analysis tool TcT. Furthermore, we have coupled the established analysis with a complexity reflecting transformation from pure OCaml programs. This extends the provided analysis to a fully automated resource analysis of higher-order functional programs.

cs.LO↗

arXiv2018

Analysis of Logarithmic Amortised Complexity

We introduce a novel amortised resource analysis based on a potential-based type system. This type system gives rise to logarithmic and polynomial bounds on the runtime complexity and is the first such system to exhibit logarithmic amortised complexity. We relate the thus obtained automatable amortised resource analysis to manual amortised analyses of self-adjusting data structures, like splay trees, that can be found in the literature.

cs.PL↗

arXiv2017

Proceedings 8th Workshop on Developments in Implicit Computational Complexity and 5th Workshop on Foundational and Practical Aspects of Resource Analysis

The DICE workshop explores the area of Implicit Computational Complexity (ICC), which grew out from several proposals to use logic and formal methods to provide languages for complexity-bounded computation (e.g. Ptime, Logspace computation). It aims at studying the computational complexity of programs without referring to external measuring conditions or a particular machine model, but only by considering language restrictions or logical/computational principles entailing complexity properties. The FOPARA workshop serves as a forum for presenting original research results that are relevant to the analysis of resource (e.g. time, space, energy) consumption by computer programs. The workshop aims to bring together the researchers that work on foundational issues with the researchers that focus more on practical results. Therefore, both theoretical and practical contributions are encouraged. We also encourage papers that combine theory and practice. Given the complementarity and the synergy between these two communities, and following the successful experience of co-location of DICE-FOPARA 2015 in London at ETAPS 2015, we hold these two workshops together at ETAPS 2017, which takes place in Uppsala, Sweden. The provided proceedings collect the papers accepted at the workshop.

cs.LO↗

arXiv2016

Kruskal's Tree Theorem for Acyclic Term Graphs

In this paper we study termination of term graph rewriting, where we restrict our attention to acyclic term graphs. Motivated by earlier work by Plump we aim at a definition of the notion of simplification order for acyclic term graphs. For this we adapt the homeomorphic embedding relation to term graphs. In contrast to earlier extensions, our notion is inspired by morphisms. Based on this, we establish a variant of Kruskal's Tree Theorem formulated for acyclic term graphs. In proof, we rely on the new notion of embedding and follow Nash-Williams' minimal bad sequence argument. Finally, we propose a variant of the lexicographic path order for acyclic term graphs.

cs.LO↗

arXiv2015

The Complexity of Interaction (Long Version)

In this paper, we analyze the complexity of functional programs written in the interaction-net computation model, an asynchronous, parallel and confluent model that generalizes linear-logic proof nets. Employing user-defined sized and scheduled types, we certify concrete time, space and space-time complexity bounds for both sequential and parallel reductions of interaction-net programs by suitably assigning complexity potentials to typed nodes. The relevance of this approach is illustrated on archetypal programming examples. The provided analysis is precise, compositional and is, in theory, not restricted to particular complexity classes.

cs.PL↗

arXiv2015

Analysing the Complexity of Functional Programs: Higher-Order Meets First-Order (Long Version)

We show how the complexity of higher-order functional programs can be analysed automatically by applying program transformations to a defunctionalized versions of them, and feeding the result to existing tools for the complexity analysis of first-order term rewrite systems. This is done while carefully analysing complexity preservation and reflection of the employed transformations such that the complexity of the obtained term rewrite system reflects on the complexity of the initial program. Further, we describe suitable strategies for the application of the studied transformations and provide ample experimental data for assessing the viability of our method.

cs.LO↗

arXiv2014

A Complexity Preserving Transformation from Jinja Bytecode to Rewrite Systems

We revisit known transformations from Jinja bytecode to rewrite systems from the viewpoint of runtime complexity. Suitably generalising the constructions proposed in the literature, we define an alternative representation of Jinja bytecode (JBC) executions as "computation graphs" from which we obtain a novel representation of JBC executions as "constrained rewrite systems". We prove non-termination and complexity preservation of the transformation. We restrict to well-formed JBC programs that only make use of non-recursive methods and expect tree-shaped objects as input. Our approach allows for simplified correctness proofs and provides a framework for the combination of the computation graph method with standard techniques from static program analysis like for example "reachability analysis".

cs.PL↗

arXiv2014

Amortised Resource Analysis and Typed Polynomial Interpretations (extended version)

We introduce a novel resource analysis for typed term rewrite systems based on a potential-based type system. This type system gives rise to polynomial bounds on the innermost runtime complexity. We relate the thus obtained amortised resource analysis to polynomial interpretations and obtain the perhaps surprising result that whenever a rewrite system R can be well-typed, then there exists a polynomial interpretation that orients R. For this we adequately adapt the standard notion of polynomial interpretations to the typed setting.

cs.LO↗

arXiv2013

Polynomial Path Orders

This paper is concerned with the complexity analysis of constructor term rewrite systems and its ramification in implicit computational complexity. We introduce a path order with multiset status, the polynomial path order POP*, that is applicable in two related, but distinct contexts. On the one hand POP* induces polynomial innermost runtime complexity and hence may serve as a syntactic, and fully automatable, method to analyse the innermost runtime complexity of term rewrite systems. On the other hand POP* provides an order-theoretic characterisation of the polytime computable functions: the polytime computable functions are exactly the functions computable by an orthogonal constructor TRS compatible with POP*.

cs.LO↗

arXiv2013

A Combination Framework for Complexity

In this paper we present a combination framework for polynomial complexity analysis of term rewrite systems. The framework covers both derivational and runtime complexity analysis. We present generalisations of powerful complexity techniques, notably a generalisation of complexity pairs and (weak) dependency pairs. Finally, we also present a novel technique, called dependency graph decomposition, that in the dependency pair setting greatly increases modularity. We employ the framework in the automated complexity tool TCT. TCT implements a majority of the techniques found in the literature, witnessing that our framework is general enough to capture a very brought setting.

cs.CC↗

arXiv2012

Polynomial Path Orders: A Maximal Model

This paper is concerned with the automated complexity analysis of term rewrite systems (TRSs for short) and the ramification of these in implicit computational complexity theory (ICC for short). We introduce a novel path order with multiset status, the polynomial path order POP*. Essentially relying on the principle of predicative recursion as proposed by Bellantoni and Cook, its distinct feature is the tight control of resources on compatible TRSs: The (innermost) runtime complexity of compatible TRSs is polynomially bounded. We have implemented the technique, as underpinned by our experimental evidence our approach to the automated runtime complexity analysis is not only feasible, but compared to existing methods incredibly fast. As an application in the context of ICC we provide an order-theoretic characterisation of the polytime computable functions. To be precise, the polytime computable functions are exactly the functions computable by an orthogonal constructor TRS compatible with POP*.

cs.CC↗

arXiv2012

A New Order-theoretic Characterisation of the Polytime Computable Functions

We propose a new order, the small polynomial path order (sPOP* for short). The order sPOP* provides a characterisation of the class of polynomial time computable function via term rewrite systems. Any polynomial time computable function gives rise to a rewrite system that is compatible with sPOP*. On the other hand any function defined by a rewrite system compatible with sPOP* is polynomial time computable. Technically sPOP* is a tamed recursive path order with product status. Its distinctive feature is the precise control provided. For any rewrite system that is compatible with sPOP* that makes use of recursion up to depth d, the (innermost) runtime complexity is bounded from above by a polynomial of degree d.

cs.CC↗

arXiv2011

The Derivational Complexity Induced by the Dependency Pair Method

We study the derivational complexity induced by the dependency pair method, enhanced with standard refinements. We obtain upper bounds on the derivational complexity induced by the dependency pair method in terms of the derivational complexity of the base techniques employed. In particular we show that the derivational complexity induced by the dependency pair method based on some direct technique, possibly refined by argument filtering, the usable rules criterion, or dependency graphs, is primitive recursive in the derivational complexity induced by the direct method. This implies that the derivational complexity induced by a standard application of the dependency pair method based on traditional termination orders like KBO, LPO, and MPO is exactly the same as if those orders were applied as the only termination technique.

cs.LO↗

arXiv2011

A Path Order for Rewrite Systems that Compute Exponential Time Functions (Technical Report)

In this paper we present a new path order for rewrite systems, the exponential path order EPOSTAR. Suppose a term rewrite system is compatible with EPOSTAR, then the runtime complexity of this rewrite system is bounded from above by an exponential function. Furthermore, the class of function computed by a rewrite system compatible with EPOSTAR equals the class of functions computable in exponential time on a Turing maschine.

cs.CC↗

arXiv2011

Dependency Pairs and Polynomial Path Orders

We show how polynomial path orders can be employed efficiently in conjunction with weak innermost dependency pairs to automatically certify polynomial runtime complexity of term rewrite systems and the polytime computability of the functions computed. The established techniques have been implemented and we provide ample experimental data to assess the new method.

cs.LO↗

arXiv2011

Efficient Implementation of Rewriting Revisited Technical Report

Recently, many techniques have been introduced that allow the (automated) classification of the runtime complexity of term rewrite systems (TRSs for short). In earlier work, the authors have shown that for confluent TRSs, innermost polynomial runtime complexity induces polytime computability of the functions defined. In this paper, we generalise the above result to full rewriting. Following our previous work, we exploit graph rewriting. We give a new proof of the adequacy of graph rewriting for full rewriting that allows for a precise control of the resources copied. In sum we completely describe an implementation of rewriting on a Turing machine (TM for short). We show that the runtime complexity of the TRS and the runtime complexity of the TM is polynomially related. Our result strengthens the evidence that the complexity of a rewrite system is truthfully represented through the length of derivations. Moreover our result allows the classification of non-deterministic polytime-computation based on runtime complexity analysis of rewrite systems.

cs.CC↗

arXiv2011

Automated Complexity Analysis Based on the Dependency Pair Method

This article is concerned with automated complexity analysis of term rewrite systems. Since these systems underlie much of declarative programming, time complexity of functions defined by rewrite systems is of particular interest. Among other results, we present a variant of the dependency pair method for analysing runtime complexities of term rewrite systems automatically. The established results significantly extent previously known techniques: we give examples of rewrite systems subject to our methods that could previously not been analysed automatically. Furthermore, the techniques have been implemented in the Tyrolean Complexity Tool. We provide ample numerical data for assessing the viability of the method.

cs.LO↗