We refine the weighted type graph technique for proving termination of double pushout (DPO) graph transformation systems. We increase the power of the approach for graphs, we generalize the technique to other categories, and we allow for variations of DPO that occur in the literature.

We introduce a termination method for the algebraic graph transformation framework PBPO+, in which we weigh objects by summing a class of weighted morphisms targeting them. The method is well-defined in rm-adhesive quasitoposes (which include toposes and therefore many graph categories of interest), and is applicable to non-linear rules. The method is also defined for other frameworks, including SqPO and left-linear DPO, because we have previously shown that they are naturally encodable into PBPO+ in the quasitopos setting. We have implemented our method, and the implementation includes a REPL that can be used for guiding relative termination proofs.

We extend the powerful Pullback-Pushout (PBPO) approach for graph rewriting with strong matching. Our approach, called PBPO+, allows more control over the embedding of the pattern in the host graph, which is important for a large class of rewrite systems. We argue that PBPO+ can be considered a unifying theory in the general setting of quasitoposes, by demonstrating that PBPO+ can define a strict superset of the rewrite relations definable by PBPO, AGREE and DPO. Additionally, we show that PBPO+ is well suited for rewriting labeled graphs and some classes of attributed graphs, by introducing a lattice structure on the label set and requiring graph morphisms to be order-preserving.

Like termination, confluence is a central property of rewrite systems. Unlike for termination, however, there exists no known complexity hierarchy for confluence. In this paper we investigate whether the decreasing diagrams technique can be used to obtain such a hierarchy. The decreasing diagrams technique is one of the strongest and most versatile methods for proving confluence of abstract rewrite systems. It is complete for countable systems, and it has many well-known confluence criteria as corollaries. So what makes decreasing diagrams so powerful? In contrast to other confluence techniques, decreasing diagrams employ a labelling of the steps with labels from a well-founded order in order to conclude confluence of the underlying unlabelled relation. Hence it is natural to ask how the size of the label set influences the strength of the technique. In particular, what class of abstract rewrite systems can be proven confluent using decreasing diagrams restricted to 1 label, 2 labels, 3 labels, and so on? Surprisingly, we find that two labels suffice for proving confluence for every abstract rewrite system having the cofinality property, thus in particular for every confluent, countable system. Secondly, we show that this result stands in sharp contrast to the situation for commutation of rewrite relations, where the hierarchy does not collapse. Thirdly, investigating the possibility of a confluence hierarchy, we determine the first-order (non-)definability of the notion of confluence and related properties, using techniques from finite model theory. We find that in particular Hanf's theorem is fruitful for elegant proofs of undefinability of properties of abstract rewrite systems.

Abstract We add MostXareYto the syllogistic logic of AllXareYand SomeXareY. We prove soundness, completeness, and decidability in polynomial time. Our logic has infinitely many rules, and we prove that this is unavoidable.

We present a coinductive framework for defining and reasoning about the infinitary analogues of equational logic and term rewriting in a uniform, coinductive way. The setup captures rewrite sequences of arbitrary ordinal length, but it has neither the need for ordinals nor for metric convergence. This makes the framework especially suitable for formalizations in theorem provers.

One of the best-known methods for discriminating λ-terms with respect to β-convertibility is due to Corrado Böhm. The idea is to compute the infinitary normal form of a λ-term M, the Böhm Tree (BT) of M. If λ-terms M, N have distinct BTs, then M ≠βN, that is, M and N are not β-convertible. But what if their BTs coincide? For example, all fixed point combinators (FPCs) have the same BT, namely λx.x(x(x(. . .))). We introduce a clocked λ-calculus, an extension of the classical λ-calculus with a unary symbol τ used to witness the β-steps needed in the normalization to the BT. This extension is infinitary strongly normalizing, infinitary confluent and the unique infinitary normal forms constitute enriched BTs, which we call clocked BTs. These are suitable for discriminating a rich class of λ-terms having the same BTs, including the well-known sequence of Böhm's FPCs. We further increase the discrimination power in two directions. First, by a refinement of the calculus: the atomic clocked λ-calculus, where we employ symbols τp that also witness the (relative) positions p of the β-steps. Second, by employing a localized version of the (atomic) clocked BTs that has even more discriminating power.

Encodings, that is, injective functions from words to words, have been studied extensively in several settings. In computability theory the notion of encoding is crucial for defining computability on arbitrary domains, as well as for comparing the power of models of computation. In language theory much attention has been devoted to regularity preserving functions. A natural question arising in these contexts is: Is there a bijective encoding such that its image function preserves regularity of languages, but its pre-image function does not? Our main result answers this question in the affirmative: For every countable class C of languages there exists a bijective encoding f such that for every language L ∈ L its image f[L] is regular. Our construction of such encodings has several noteworthy consequences. Firstly, anomalies arise when models of computation are compared with respect to a known concept of implementation that is based on encodings which are not required to be computable: Every countable decision model can be implemented, in this sense, by finite-state automata, even via bijective encodings. Hence deterministic finite-state automata would be equally powerful as Turing machine deciders. A second consequence concerns the recognizability of sets of natural numbers via number representations and finite automata. A set of numbers is said to be recognizable with respect to a representation if an automaton accepts the language of representations. Our result entails that there is one number representation with respect to which every recursive set is recognizable.

We present a coinductive framework for defining infinitary analogues of equational reasoning and rewriting in a uniform way. The setup captures rewrite sequences of arbitrary ordinal length, but it has neither the need for ordinals nor for metric convergence. This makes the framework especially suitable for formalizations in theorem provers.

A new technique is presented to prove non-termination of term rewriting. The basic idea is to find a non-empty regular language of terms that is closed under rewriting and does not contain normal forms. It is automated by representing the language by a tree automaton with a fixed number of states, and expressing the mentioned requirements in a SAT formula. Satisfiability of this formula implies non-termination. Our approach succeeds for many examples where all earlier techniques fail, for instance for the S-rule from combinatory logic.

Abstract We study the complexity of deciding the equality of streams specified by systems of equations. There are several notions of stream models in the literature, each generating a different semantics of stream equality. We pinpoint the complexity of each of these notions in the arithmetical or analytical hierarchy. Their complexity ranges from low levels of the arithmetical hierarchy such as Π 0 2 for the most relaxed stream models, to levels of the analytical hierarchy such as Π 1 1 and up to subsuming the entire analytical hierarchy for more restrictive but natural stream models. Since all these classes properly include both the semi-decidable and co-semi-decidable classes, it follows that regardless of the stream semantics employed, there is no complete proof system or algorithm for determining equality or inequality of streams. We also discuss several related problems, such as the existence and uniqueness of stream solutions for systems of equations, as well as the equality of such solutions.

We study the complexity of deciding the equality of infinite objects specified by systems of equations, and of infinite objects specified by λ-terms. For equational specifications there are several natural notions of equality: equality in all models, equality of the sets of solutions, and equality of normal forms for productive specifications. For λ-terms we investigate Böhm-tree equality and various notions of observational equality. We pinpoint the complexity of each of these notions in the arithmetical or analytical hierarchy.

We consider infinite sequences of symbols, also known as streams, and the decidability question for equality of streams defined in a restricted format. (Some formats lead to undecidable equivalence problems.) This restricted format consists of prefixing a symbol at the head of a stream, of the stream function `zip', and recursion variables. Here `zip' interleaves the elements of two streams alternatingly. The celebrated Thue- Morse sequence is obtained by the succinct `zip-specification' M = 0 : X X = 1 : zip(X, Y) Y = 0 : zip(Y, X) The main results are as follows. We establish decidability of equivalence of zip-specifications, by employing bisimilarity of observation graphs based on a suitably chosen cobasis. Furthermore, our analysis, based on term rewriting and coalgebraic techniques, reveals an intimate connection between zip-specifications and automatic sequences. This leads to a new and simple characterization of automatic sequences. The study of zip-specifications is placed in a wider perspective by employing observation graphs in a dynamic logic setting, yielding yet another alternative characterization of automatic sequences. By the first characterization result, zip-specifications can be perceived as a term rewriting syntax for automatic sequences. For streams σ the following are equivalent: (a) σ can be specified using zip; (b) σ is 2-automatic; and (c) σ has a finite observation graph using the cobasis (hd, even, odd). Here even and odd are defined by even(a : s) = a : odd(s), and odd(a : s) = even(s). The generalization to zip-k specifications (with zip-k interleaving k streams) and to k-automaticity is straightforward. As a natural extension of the class of automatic sequences, we also consider `zip-mix' specifications that use zips of different arities in one specification. The corresponding notion of automaton employs a state-dependent input-alphabet, with a number representation (n)A = dm... d0where the base of digit di is determined by the automaton A on input di-1... d0. Finally we show that equivalence is undecidable for a simple extension of the zip-mix format with projections analogous to even and odd.

Streams are infinite sequences over a given data type. A stream specification is a set of equations intended to define a stream. In this paper we focus on equality of streams, more precisely, for a given set of equations two stream terms are said to be equal if they are equal in every model satisfying the given equations. We investigate techniques for proving equality of streams suitable for automation. Apart from techniques that were already available in the tool CIRC from Lucanu and Rosu, we also exploit well-definedness of streams, typically proved by proving productivity. Moreover, our approach does not restrict to behavioral input format and does not require termination. We present a tool Streambox that can prove equality of a wide range of examples fully automatically.

Fixed point combinators (and their generalization: looping combinators) are classic notions belonging to the heart of λ-calculus and logic. We start with an exploration of the structure of fixed point combinators (fpc's), vastly generalizing the wellknown fact that if Yis an fpc, Y(SI) is again an fpc, generating the Böhm sequence of fpc's. Using the infinitary λ-calculus we devise infinitely many other generation schemes for fpc's. In this way we find schemes and building blocks to construct new fpc's in a modular way. Having created a plethora of new fixed point combinators, the task is to prove that they are indeed new. That is, we have to prove their β-inconvertibility. Known techniques via Böhm Trees do not apply, because all fpc's have the same Böhm Tree (BT). Therefore, we employ 'clocked BT's', with annotations that convey information of the tempo in which the data in the BT are produced. BT's are thus enriched with an intrinsic clock behaviour, leading to a refined discrimination method for λ-terms. The corresponding equality is strictly intermediate between =βand =BT, the equality in the classical models of λ-calculus. An analogous approach pertains to Lévy-Longo and Berarducci trees. Finally, we increase the discrimination power by a precision of the clock notion that we call 'atomic clock'.

We propose a natural generalisation of asynchronous bounded delay (ABD) network models. The commonly used ABD models assume a known bound on message delay. This assumption is often too strict for real-life applications. To this end we introduce a novel probabilistic network model, called asynchronous bounded expected delay (ABE), which requires a known bound on the expected message delay. While the conditions of ABD networks restrict the set of possible executions, in ABE networks all asynchronous executions are possible, but executions with extremely long delays are less probable. The ABE model captures asynchrony that occurs in sensor networks and ad-hoc networks.

We present some contributions to the theory of infinitary rewriting for weakly orthogonal term rewrite systems, in which critical pairs may occur provided they are trivial. We show that the infinitary unique normal form property (UNinf) fails by a simple example of a weakly orthogonal TRS with two collapsing rules. By translating this example, we show that UNinf also fails for the infinitary lambda-beta-eta-calculus. As positive results we obtain the following: Infinitary confluence, and hence UNinf, holds for weakly orthogonal TRSs that do not contain collapsing rules. To this end we refine the compression lemma. Furthermore, we consider the triangle and diamond properties for infinitary developments in weakly orthogonal TRSs, by refining an earlier cluster-analysis for the finite case.