RTA-TLCA 2014 LNCS PROCEEDINGS: PAPERS WITH ABSTRACTS

ABSTRACT. Inductive data such as finite lists and trees can elegantly be defined by constructors which allow programmers to analyze and manipulate finite data via pattern matching. Dually, coinductive data such as streams can be defined by observations such as head and tail and programmers can synthesize infinite data via copattern matching. This leads to a symmetric language where finite and infinite data can be nested. In this paper, we compile nested pattern and copattern matching into a core language which only supports simple non-nested (co)pattern matching. This core language may serve as an intermediate language of a compiler. We show that this translation is conservative, i.e., the multi-step reduction relation in both languages coincides for terms of the original language. Furthermore, we show that the translation preserves strong normalisation: a term of the original language is strongly normalising in one language if and only if it is so in the other.

ABSTRACT. Decreasing diagrams technique (van Oostrom, 1994) has been successfully used to prove confluence of rewrite systems in various ways; using rule-labelling (van Oostrom, 2008), it can be also applied directly to prove confluence of some linear term rewriting systems (TRSs) automatically. Some efforts for extending the rule-labelling are known, but non-left-linear TRSs are left beyond the scope. Two methods for automatically proving confluence of non-(left-)linear TRSs with the rule-labelling are given. The key idea of our methods is to combine the decreasing diagrams technique with persistency of confluence (Aoto & Toyama, 1997).

ABSTRACT. For an infinite-state concurrent system S with a set AP of state predicates, its predicate abstraction defines a finite-state system whose states are subsets of AP, and its transitions s --> s' are witnessed by concrete transitions between states in S satisfying the respective sets of predicates s and s'. Since it is not always possible to find such witnesses, an over-approximation adding extra transitions is often used. For systems S described by formal specifications, predicate abstractions are typically built using various automated deduction techniques. This paper presents a new method--based on rewriting, semantic unification, and variant narrowing--to automatically generate a predicate abstraction when the formal specification of S is given by a conditional rewrite theory. The method is illustrated with concrete examples showing that it naturally supports abstraction refinement and is quite accurate, i.e., it can produce abstractions not needing over-approximations.

ABSTRACT. We present an algebraic characterization of the complexity classes Logspace and NLogspace, using an algebra with a composition law based on unification. This new bridge between unification and complexity classes is inspired from proof theory and more specifically linear logic and Geometry of Interaction.

We show how unification can be used to build a model of computation by means of specific subalgebras associated to finite permutations groups.

We then prove that the complexity of deciding whenever an observation (the algebraic counterpart of a program) accepts a word can be decided within logarithmic space. We also show that the construction can naturally be related to pointer machines, an intuitive way of understanding logarithmic space computing.

ABSTRACT. Ramsey Theorem for pairs is a combinatorial result that cannot be intuitionistically proved. In this paper we present a new form of Ramsey Theorem for pairs we call H-closure Theorem. H-closure is a property of well founded relations, intuitionistically provable, informative, and possibly simpler to use in intuitionistic proofs. Using our intuitionistic version of Ramsey Theorem we intuitionistically prove the Termination Theorem by Poldenski and Rybalchenko. This theorem concerns an algorithm inferring termination for while-programs, and was originally proved from the classical Ramsey Theorem, then intuitionistically, but using a intuitionistic version of Ramsey Theorem different from our one. Our long-term goal is to extract effective bounds for the while-programs from the proof of Termination Theorem, and our new intuitionistic version of Ramsey Theorem is designed for this goal.

ABSTRACT. We show how to construct a logical relation for countable nondeterminism in a guarded type theory, corresponding to the internal logic of the topos $Sh(\omega_1)$ of sheaves over $\omega_1$. In contrast to earlier work on abstract step-indexed models, we not only construct the logical relations in the guarded type theory, but also give an internal proof of the adequacy of the model with respect to standard contextual equivalence. To state and prove adequacy of the logical relation, we introduce a new propositional modality. In connection with this modality we show why it is necessary to work in the logic of $\Sh(\omega_1)$.

ABSTRACT. Deduction modulo is a framework in which theories are integrated into proof systems such as natural deduction or sequent calculus by presenting them using rewriting rules. When only terms are rewritten, cut admissibility in those systems is equivalent to the confluence of the rewriting system, as shown by Dowek, RTA 2003, LNCS 2706. This is no longer true when considering rewriting rules involving propositions. In this paper, we show that, in the same way that it is possible to recover confluence using Knuth-Bendix completion, one can regain cut admissibility in the general case using standard saturation techniques. This work relies on a view of proposition rewriting rules as oriented clauses, like term rewriting rules can be seen as oriented equations. This also leads us to introduce an extension of deduction modulo with *conditional* term rewriting rules.

ABSTRACT. We implement an online judge for context-free grammars. Our system contains a list of problems describing formal languages, and asking for grammars generating them. A submitted proposal grammar receives a verdict of acceptance or rejection depending on whether the judge determines that it is equivalent to the reference solution grammar provided by the problem setter. Since equivalence of context-free grammars is an undecidable problem, we consider a maximum length L and only test equivalence of the generated languages up to words of length L. This length restriction is very often sufficient for the well-meant submissions. Since this restricted problem is still NP-complete, we design and implement methods based on hashing, SAT, and automata that perform well in practice.

ABSTRACT. We define the tree automata with height constraints between brothers (TACBB_H). Constraints of equalities and inequalities between heights of siblings that restrict the applicability of the rules are allowed in TACBB_H. These constraints allow to express natural tree languages like complete or balanced (like AVL) trees. We prove decidability of emptiness and finiteness for TACBB_H, and also for a more general class that additionally allows to combine equality and disequality constraints between brothers.

ABSTRACT. We give a coinductive proof of confluence, up to equivalence of root-active subterms, of infinitary lambda-calculus. We also show confluence of Böhm reduction (with respect to root-active terms) in infinitary lambda-calculus. In contrast to previous proofs, our proof makes heavy use of coinduction and does not employ the notion of descendants.

ABSTRACT. A constructor rewriting system $R$ is said to characterize a language $D \subseteq \{ 0, 1 \}^\{< \infty}$ if there are designated function symbols $f_0$ and $\mathrm{true}$ such that for every constructor term $s$ that represents a string $\mathtt{s} \in \{0,1\}^{< \infty}$, we have $f_0(s) \rightarrow^* \mathrm{true}$ iff $\mathtt{s} \in D$. A class $\mathfrak{R}$ of rewriting systems is said to characterize a class $\mathfrak{D}$ of languages if every language in $\mathfrak{D}$ is characterized by a system in $\mathfrak{R}$ and every element of $\mathfrak{R}$ characterizes a language in $\mathfrak{D}$. We define the class of \emph{constrained cons-free} rewriting systems and show that this class characterizes $P$, the set of languages decidable in polynomial time on a deterministic Turing machine. The main novelty of the characterization is that it allows very liberal properties of term rewriting, in particular non-deterministic evaluation: no reduction strategy is enforced, and systems are allowed to be non-confluent.

ABSTRACT. The notion of subtyping has gained an important role both in theoretical and applicative domains: in lambda and concurrent calculi as well as in programming languages. The soundness and the completeness, together referred to as the preciseness of subtyping, can be considered from two different points of view: denotational and operational. The former preciseness is based on the denotation of a type which is a mathematical object that describes the meaning of the type in accordance with the denotations of other expressions from the language. The latter preciseness has been recently developed with respect to type safety, i.e. the safe replacement of a term of a smaller type when a term of a bigger type is expected.

We proposes a technique for formalising and proving operational preciseness of the subtyping relation in the setting of a concurrent lambda calculus with intersection and union types. The key feature is the link between typings and the operational semantics. We prove then soundness and completeness getting that the subtyping relation of this calculus enjoys both denotational and operational preciseness.

ABSTRACT. We add an abstract datatype for a closed interval of real numbers to type theory, providing a representation-independent approach to programming with real numbers. The abstract datatype requires only function types and a natural numbers type for its formulation, so can be added to any type theory that extends Goedel's System T. Our main result establishes that programming with the abstract datatype is equivalent in power to programming intensionally with representations of real numbers. We also consider representing arbitrary real numbers using a mantissa-exponent representation in which the mantissa is taken from the abstract interval.

ABSTRACT. We revisit lambda encodings of data, proposing new solutions to several old problems, in particular dependent elimination with lambda encodings. We start with a type assignment form of the Calculus of Constructions, restricted recursive definitions and Miquel’s implicit product. We add a type construct \iota x . T, called a self type, which allows T to refer to the subject of typing. We show how the resulting System S with this novel form of dependency supports dependent elimination with lambda encodings, including induction principles. Strong normalization of S is established by defining an erasure from S to a version of F-omega with positive recursive type definitions, which we analyze. We also prove type preservation for S.

ABSTRACT. This paper discusses the method of formative rules for first-order rewriting, which was previously defined for a class of higher-order rewriting. Dual to the well-known notion of usable rules, this technique allows for further simplifications of the term constraints that need to be solved during a termination proof. Compared to the higher-order definition, we can obtain significant improvements in the first-order setting, with or without types.

ABSTRACT. In this paper we present a simple technique for analysing the runtime complexity of rewrite systems. In complexity analysis many techniques are based on reduction orders. We show how the monotonicity condition for orders can be weakened by using the notion of context-sensitive rewriting. The presented technique is very easy to implement and has been integrated in the Tyrolean Complexity Tool. We provide ample experimental data for assessing the viability of our method.

ABSTRACT. 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 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 their exists a polynomial interpretation that orients R. For this we suitable adapt the standard notion of polynomial interpretations to the typed setting.

ABSTRACT. Knuth and Bendix showed that confluence of a terminating first-order rewrite system can be reduced to the joinability of its finitely many critical pairs. We show that this is still true of a rewrite system RT ∪ RNT such that RT is terminating and RNT is a left-linear, rank non-increasing, possibly non-terminating rewrite system. Confluence can then be reduced to the joinability of the critical pairs of RT and to the existence of decreasing diagrams for the critical pairs of RT inside RNT as well as for the rigid parallel critical pairs of RNT.

ABSTRACT. In this paper we generalize the notion of proof term to the realm of transfinite reduction. Proof terms represent reductions in the first- order term format, thereby facilitating their formal analysis. We show that any transfinite reduction can be faithfully represented as an infinitary proof term, which is unique up to, infinitary, associativity.

Our main use of proof terms is in a definition of permutation equivalence for transfinite reductions, on the basis of permutation equations. This definition involves a variant of equational logic, adapted for dealing with infinite objects.

A proof of the compression property via proof terms is presented, which establishes permutation equivalence between the original and the compressed reductions.

ABSTRACT. In this work we present a paradigm of focusing proof search based on an incremental construction of ''correct'' (i.e, sequentializable) proof structures of the pure (units free) multiplicative and additive fragment of linear logic (J.-Y. Girard, 1987). The correctness of proof construction steps (or expansion steps) is ensured by means of a system of graph retraction rules; this graph rewriting system is shown to be convergent, that is, terminating and confluent. The proposed proof construction follows a specific - ''parsimonious'', indeed - retraction strategy that, at each expansion attempt, allows to take into account (abstract) graphs that are ''smaller'' (w.r.t. the size) than the starting proof structures.

ABSTRACT. We establish that the local store monad defined by Plotkin and Power is a monad with arities for an appropriate notion of arities in the category of presheaves over the category of injections. From this follows that the monad is associated to a graded Lawvere theory. We explain how to present this graded theory by generators and relations, which we then depict in the graphical language of string diagrams.

ABSTRACT. The Lambda-mu-calculus is an extension of Parigot’s lambda-mu-calculus, the untyped variant of which is proved by Saurin to satisfy some fundamental properties such as the standardization and the separation theorem. For the untyped Lambda-mu-calculus, Nakazawa and Katsumata gave extensional models, called stream models, which is a simple extension of the lambda models, and in which terms are represented as functions on streams. However, we cannot construct a term model from the Lambda-mu-calculus. This paper introduces an extension of the Lambda-mu-calculus, called Lambda-mu-cons, on which we can construct a term model as a stream model, and its reduction system satisfying confluence, subject reduction, and strong normalization.

ABSTRACT. We investigate possible extensions of arbitrary given Pure Type Systems with additional sorts and rules which preserve the normalization property. In particular we identify the following interesting extensions: the disjoint union P+Q of two PTSs P and Q, the PTS ∀P.Q which intuitively captures the "Q-logic of P-terms'' and Ppoly which intuitively denotes the "predicative polymorphism" extension of P.

These results suggest a new approach to the study of the meta-theory of PTSs, by examination of the relationships between different calculi and "predicative extensions" which allow more expressiveness with equivalent logical strength.

ABSTRACT. Motivated by the question whether sound and expressive applicative similarities for program calculi with should-convergence exist, this paper investigates expressive applicative similarities for the untyped call-by-value lambda-calculus extended with McCarthy's ambiguous choice operator amb. Soundness of the applicative similarities w.r.t. contextual equivalence based on may- and should-convergence is proved by adapting Howe's method to should-convergence. As usual for nondeterministic calculi, similarity is not complete w.r.t. contextual equivalence which requires a rather complex counter example as a witness.Also the call-by-value lambda-calculus with the weaker nondeterministic construct erratic choice is analyzed and sound applicative similarities are provided. This justifies the expectation that also for more expressive and call-by-need higher-order calculi there are sound and powerful similarities for should-convergence.

ABSTRACT. We show that provability in the implicational fragment of relevance logic is complete for doubly exponential time, using reductions to and from coverability in branching vector addition systems.

ABSTRACT. A connection between lambda calculus and the algebra of near semi-rings is discussed. Among the results is the following completeness theorem. A first-order equation in the language of binary associative distributive algebras is true in all such algebras if and only if the interpretations of the first order terms as lambda terms beta-eta convert to one another. A similar result holds for equations containing free variables.

ABSTRACT. This paper presents a language-independent proof system for proving reachability properties of programs written in non-deterministic (concurrent) languages. The proof system can derive properties with either all-path and one-path semantics, that is, that states satisfying a given precondition reach states satisfying a given postcondition on all terminating execution paths, respectively on one terminating execution path. The proof system may be instantiated with any unconditional operational semantics, and is shown sound (i.e., partially correct) and (relatively) complete, independent of the object language. The proof system is implemented in a tool for semantics-based verification as part of the K framework, and evaluated on a few examples.

ABSTRACT. Monotone algebras are frequently utilized to generate reduction orders in automated termination- and complexity-proofs. To be able to certify these proofs, we formalized several kinds of interpretations in the proof assistant Isabelle/HOL. Here, we report on our integration of matrix interpretations, arctic interpretations, and non-linear polynomial interpretations over various domains, including the reals.

ABSTRACT. This paper describes the Conditional Confluence tool, a fully automatic confluence checker for first-order conditional term rewrite systems. The tool implements various confluence criteria that have been proposed in the literature. A simple technique is presented to test conditional critical pairs for infeasibility, which makes conditional confluence criteria more useful. Detailed experimental data is presented.

ABSTRACT. This paper describes the implementation and techniques of the Nagoya Termination Tool, a termination analyzer for term rewrite systems. The tool is special for its power due to the implementation of the weighted path order which subsumes most of the existing reduction pairs, and the efficiency due to the deep cooperation with SMT solvers. We present some new ideas that contribute to the efficiency and the power of the tool.

ABSTRACT. String rewriting can not only be applied on strings, but also on cycles and even on general graphs. In this paper we investigate ter- mination of string rewriting applied on cycles, shortly denoted as cycle rewriting, which is a strictly stronger requirement than termination on strings. Most techniques for proving termination of string rewriting fail for proving termination of cycle rewriting, but match bounds, arctic ma- trices and tropical matrices can be applied. Further we show how any terminating string rewriting system can be transformed to a terminating cycle rewriting system, preserving derivational complexity.