Sticky Existential Rules and Disjunction are Incompatible

Stickiness is one of the well-known properties in the literature that guarantees decidability of query answering under sets of existential rules, that is, Datalog rules extended with existential quantification in rule heads. In this note, we investigate whether this remains true in the case when rule heads are allowed to be disjunctive. We answer this question in the negative, providing a strong undecidability result that shows that the concept of stickiness cannot be extended to disjunctive existential rules, even when considering only fixed atomic queries and a fixed set of rules. This provides evidence that, in order to keep query answering decidable, a stronger property than stickiness is needed in the disjunctive case.

Asynchronous session subtyping as communicating automata refinement

We study the relationship between session types and behavioural contracts, representing Communicating Finite State Machines (CFSMs), under the assumption that processes communicate asynchronously. Session types represent a syntax-based approach for the description of communication protocols, while behavioural contracts, formally expressing CFSMs, follow an operational approach. We show the existence of a fully abstract interpretation of session types into a fragment of contracts that maps session subtyping into binary compliance-preserving CFSMs/behavioural contract refinement. In this way, on the one hand, we enrich the theory of session types with an operational characterization and, on the other hand, we use recent undecidability results for asynchronous session subtyping to obtain an original undecidability result for asynchronous CFSMs/behavioural contract refinement.

HOW MUCH PROPOSITIONAL LOGIC SUFFICES FOR ROSSER’S ESSENTIAL UNDECIDABILITY THEOREM?

In this paper we explore the following question: how weak can a logic be for Rosser’s essential undecidability result to be provable for a weak arithmetical theory? It is well known that Robinson’s Q is essentially undecidable in intuitionistic logic, and P. Hájek proved it in the fuzzy logic BL for Grzegorczyk’s variant of Q which interprets the arithmetic operations as nontotal nonfunctional relations. We present a proof of essential undecidability in a much weaker substructural logic and for a much weaker arithmetic theory, a version of Robinson’s R (with arithmetic operations also interpreted as mere relations). Our result is based on a structural version of the undecidability argument introduced by Kleene and we show that it goes well beyond the scope of the Boolean, intuitionistic, or fuzzy logic.

On the Satisfiability Problem for SPARQL Patterns

The satisfiability problem for SPARQL 1.0 patterns is undecidable in general, since the relational algebra can be emulated using such patterns. The goal of this paper is to delineate the boundary of decidability of satisfiability in terms of the constraints allowed in filter conditions. The classes of constraints considered are bound-constraints, negated bound- constraints, equalities, nonequalities, constant-equalities, and constant-nonequalities. The main result of the paper can be summarized by saying that, as soon as inconsistent filter conditions can be formed, satisfiability is undecidable. The key insight in each case is to find a way to emulate the set difference operation. Undecidability can then be obtained from a known undecidability result for the algebra of binary relations with union, composition, and set difference. When no inconsistent filter conditions can be formed, satisfiability is decidable by syntactic checks on bound variables and on the use of literals. Although the problem is shown to be NP-complete, it is experimentally shown that the checks can be implemented efficiently in practice. The paper also points out that satisfiability for the so-called ‘well-designed’ patterns can be decided by a check on bound variables and a check for inconsistent filter conditions.

A NOTE ON THE DECIDABILITY OF SUBWORD INEQUALITIES

Extending the general undecidability result concerning the absoluteness of inequalities between subword histories, in this paper we show that the question whether such inequalities hold for all words is undecidable even over a binary alphabet and bounded number of blocks, i.e., unary factors of maximal length.

An Undecidability Result on Limits of Sparse Graphs

Given a set $\mathcal{B}$ of finite rooted graphs and a radius $r$ as an input, we prove that it is undecidable to determine whether there exists a sequence $(G_i)$ of finite bounded degree graphs such that the rooted $r$-radius neighbourhood of a random node of $G_i$ is isomorphic to a rooted graph in $\mathcal{B}$ with probability tending to 1. Our proof implies a similar result for the case where the sequence $(G_i)$ is replaced by a unimodular random graph.

RESTRICTED SETS OF TRAJECTORIES AND DECIDABILITY OF SHUFFLE DECOMPOSITIONS

The decidability of the shuffle decomposition problem for regular languages is a long standing open question. We consider decompositions of regular languages with respect to shuffle along a regular set of trajectories and obtain positive decidability results for restricted classes of trajectories. Also we consider decompositions of unary regular languages. Finally, we establish in the spirit of the Dassow-Hinz undecidability result an undecidability result for regular languages shuffled along a fixed linear context-free set of trajectories.

On the Expressive Power of Concurrent Constraint Programming Languages

The tcc paradigm is a formalism for timed concurrent constraint programming. Several tcc languages differing in their way of expressing infinite behaviour have been proposed in the literature. In this paper we study the expressive power of some of these languages. In particular, we show that:<dl compact="compact"><dt>(1)</dt><dd>recursive procedures with parameters can be encoded into parameterless recursive procedures with dynamic scoping, and vice-versa.</dd><dt>(2)</dt><dd>replication can be encoded into parameterless recursive procedures with static scoping, and vice-versa.</dd><dt>(3)</dt><dd>the languages from (1) are strictly more expressive than the languages from (2).</dd></dl>Furthermore, we show that behavioural equivalence is undecidable for the languages from (1), but decidable for the languages from (2). The undecidability result holds even if the process variables take values from a fixed finite domain.