ABSTRACT. In 2005, Abramsky introduced various linear/affine combinatory algebras consisting of partial involutions over a suitable formal language, in order to discuss reversible computation in a game-theoretic setting. These algebras arise as instances of the general paradigm explored by E. Haghverdi, called "Abramsky's Programme", which amounts to defining a lambda-algebra starting from a so called "Geometry of Interaction" (GoI) Situation in a traced symmetric monoidal category.

In this paper, we investigate this construction from the point of view of the model theory of lambda-calculus. We focus on the strictly linear and the strictly affine parts of Abramsky's Affine Combinatory Algebras. We outline briefly how to encompass the full algebra.

The gist of our approach is that the GoI interpretation of a term based on involutions is "dual" to the principal type of the term, with respect to the simple types discipline for a linear/affine lambda-calculus. Our analysis unveils three conceptually independent, but ultimately equivalent, accounts of application in the lambda-calculus: beta-reduction, the GoI application of involutions based on symmetric feedback (Girard's Execution Formula), and unification of principal types.

Our result provides an answer, in the strictly affine case, to the question raised in [1] of characterising the partial involutions arising from bi-orthogonal pattern matching automata, which are denotations of affine combinators, and it points to the answer to the full question. Furthermore, we prove that the strictly linear combinatory algebra of partial involutions is a strictly linear lambda-algebra, albeit not a combinatory model, while both the strictly affine combinatory algebra and the full affine combinatory algebra are not.

In order to check all the necessary equations involved in the definition of affine lambda-algebra we implement in Erlang application of involutions.

ABSTRACT. Uniform sampling has drawn diverse applications in programming languages and software engineering, like in constrained-random verification (CRV), constrained-fuzzing and bug synthesis. The effectiveness of these applications depend on the uniformity of test stimuli generated from a given set of constraints. Despite significant progress over the past few years, the performance of the state of the art techniques still falls short of those of heuristic methods employed in the industry which sacrifice either uniformity or scalability when generating stimuli.

In this paper, we propose a new approach to the uniform generation that builds on recent progress in knowledge compilation. The primary contribution of this paper is marrying knowledge compilation with uniform sampling: our algorithm, KUS, employs the state-of-the-art knowledge compilers to first compile constraints into d-DNNF form, and then, generates samples by making two passes over the compiled representation.

We show that KUS is able to significantly outperform existing state-of-the-art algorithms, SPUR and UniGen2, by up to 3 orders of magnitude in terms of runtime while achieving a geometric speedup of 1.7 and 8.3 over SPUR and UniGen2 respectively. Also, KUS achieves a lower PAR-2 score, around 0.82× that of SPUR and 0.38× that of UniGen2. Furthermore, KUS achieves speedups of up to 3 orders of magnitude for incremental sampling. The distribution generated by KUS is statistically indistinguishable from that generated by an ideal uniform sampler. Moreover, KUS is almost oblivious to the number of samples requested.

ABSTRACT. We define well-founded rewrite orderings on graphs and show that they can be used to show termination of graph rewrite rules by checking all (infinitely many) cyclic extensions of a given set of graph rewrite rules. We then introduce an ordering on graphs inspired by the recursive path ordering on terms. We show that our graph path ordering is a well-founded rewrite ordering on graphs for which checking termination of a finite set of graph rewrite rules is decidable. Our graph path ordering applies to arbitrary finite, directed, labelled, ordered multigraphs and provides therefore a building block for rewriting with such graphs, which should impact the many areas in which computations take place on graphs.

ABSTRACT. There are various types of automata on infinite words, differing in their acceptance conditions. The most classic ones are weak, Buchi, co-Buchi, parity, Rabin, Streett, and Muller. This is opposed to the case of automata on finite words, in which there is only one standard type. The natural question is why---Why not a single type? Why these particular types? Shall we further look into additional types?

For answering these questions, we clarify the succinctness of the different automata types and the size blowup involved in performing boolean operations on them. To this end, we show that unifying or intersecting deterministic automata of the classic omega-regular-complete types, namely parity, Rabin, Streett, and Muller, involves an exponential size blowup.

We argue that there are good reasons for the classic types, mainly in the case of nondeterministic and alternating automata. They admit good size and complexity bounds with respect to succinctness, boolean operations, and decision procedures, and they are closely connected to various logics.

Yet, we also argue that there is place for additional types, especially in the case of deterministic automata. In particular, generalized-Rabin, which was recently introduced, as well as a disjunction of Streett conditions, which we call hyper-Rabin, where the latter further generalizes the former, are interesting to consider. They may be exponentially more succinct than the classic types, they allow for union and intersection with only a quadratic size blowup, and their nonemptiness can be checked in polynomial time.

ABSTRACT. First-order interpolation properties are notoriously hard to determine, even for logics where propositional interpolation is more or less obvious. One of the most prominent examples is first-order Gödel logic. Lyndon interpolation is a strengthening of the interpolation property in the sense that propositional variables or predicate symbols are only allowed to occur positively (negatively) in the interpolant if they occur positively (negatively) on both sides of the implication. Note that Lyndon interpolation is difficult to establish for first-order logics as most proof-theoretic methods fail. In this paper we provide general derivability conditions for a first-order logic to admit Lyndon interpolation for the prenex ⊃ prenex fragment and apply the arguments to the prenex ⊃ prenex fragment of first-order Gödel logic.

ABSTRACT. Matching concept descriptions against concept patterns was introduced as a new inference task in Description Logics two decades ago, motivated by applications in the Classic system. Shortly afterwards, a polynomial-time matching algorithm was developed for the DL FL0. However, this algorithm cannot deal with general TBoxes (i.e., finite sets of general concept inclusions). Here we show that matching in FL0 w.r.t. general TBoxes is ExpTime-complete, which is the best possible complexity for this problem since already subsumption w.r.t. general TBoxes is ExpTime-complete in FL0. We also show that, w.r.t. a restricted form of TBoxes, the complexity of matching in FL0 can be lowered to PSpace.

ABSTRACT. Past research into decidable fragments of first-order logic (FO) has produced two very prominent fragments: the guarded fragment GF, and the two-variable fragment FO2. These fragments are very important because they provide significant insights into decidability and expressiveness of other (computational) logics, like Modal Logic (ML) and various Description Logics (DLs). In this paper, we take a closer look at GF and FO2, and present a new fragment that subsumes them both. This fragment, called the triguarded fragment (denoted TGF), is obtained by relaxing the standard definition of GF: quantification is required to be guarded only for subformulae with three or more free variables. We show that satisfiability of equality-free TGF is N2ExpTime-complete, but becomes NExpTime- complete if we bound the arity of predicates by a constant (a natural assumption in the context of ML and DLs). Finally, we show that many natural extensions of TGF, including the addition of equality, lead to undecidability.