We study the reduction in a $\lambda$ -calculus derived from Moggi’s computational one, which we call the computational core. The reduction relation consists of rules obtained by orienting three monadic laws. Such laws, in particular associativity and identity, introduce intricacies in the operational analysis. We investigate the central notions of returning a value versus having a normal form and address the question of normalizing strategies. Our analysis relies on factorization results.

Over the recent years, the theory of rewriting has been used and extended in order to provide systematic techniques to show coherence results for strict higher categories. Here, we investigate a further generalization to Gray categories, which are known to be equivalent to tricategories. This requires us to develop the theory of rewriting in the setting of precategories, which are adapted to mechanized computations and include Gray categories as particular cases. We show that a finite rewriting system in precategories admits a finite number of critical pairs, which can be efficiently computed. We also extend Squier’s theorem to our context, showing that a convergent rewriting system is coherent, which means that any two parallel 3-cells are necessarily equal. This allows us to prove coherence results for several well-known structures in the context of Gray categories: monoids, adjunctions, and Frobenius monoids.

We consider the problem of the unification modulo an equational theory associativity and commutativity (ACh), which consists of a function symbol h that is homomorphic over an associative–commutative operator +. Since the unification modulo ACh theory is undecidable, we define a variant of the problem called bounded ACh unification. In this bounded version of ACh unification, we essentially bound the number of times h can be applied to a term recursively and only allow solutions that satisfy this bound. There is no bound on the number of occurrences of h in a term, and the + symbol can be applied an unlimited number of times. We give inference rules for solving the bounded version of the problem and prove that the rules are sound, complete, and terminating. We have implemented the algorithm in Maude and give experimental results. We argue that this algorithm is useful in cryptographic protocol analysis.

The homotopical Squier’s theorem relates rewriting properties of a presentation of a monoid with homotopical invariants of this monoid. This theorem has since been extended by Guiraud and Malbos, yielding a so-called polygraphic resolution of a monoid starting from a presentation with suitable rewriting properties. In this article, we argue that cubical categories are a more natural setting in which to express and possibly extend Guiraud and Malbos construction. As a proof-of-concept, we give a new proof of Squier’s homotopical theorem using cubical categories.

This article is dedicated to Liesbeth van Houts, editor of the Gesta Normannorum ducum, generous mentor, colleague, and friend.

This article offers an analysis, edition, and translation of the Brevis cronica compendiosa ducum Normannie, a historiographical account of the dukes of Normandy and their deeds, written at the turn of the fifteenth century by the Norman jurist and man of letters, Simon de Plumetot (1371–1443). Having all but escaped the attention of modern scholars, this study is the first to examine and publish the Brevis cronica. It not only demonstrates that the work is of greater importance than its rather scrappy form might at first suggest, but it also looks to place the text within the broader context of Simon's literary and bibliophilic practices and to determine its raison d’être. In doing so, it argues that the Brevis cronica was perhaps created as part of a much larger historiographical project, namely an extended chronicle of Normandy, written in the vernacular, the text of which is now lost. By exploring these important issues, the article sheds new light on a wide range of topics, from early humanist book collecting to the writing of history in France in the later Middle Ages.

This article presents two hitherto unstudied compilations of verses from the Bustān of Saʿdī. Both circulated in the Persianate world in the fifteenth and sixteenth centuries. The article provides an analysis of the compilations’ content as well as their relation to the complete Bustān. By highlighting certain stories and themes at the expense of others, and by ordering these passages in a way that differs from the complete Bustān, each compilation transforms Saʿdī’s text into a shorter, more homogenous composition, with distinct formal, thematic, and generic qualities. The shorter compilation presents a series of aphorisms, forming a mirror for princes. The longer one offers a selection of stories and lessons and emphasizes mystical themes, including aspects of Sufi erotic theology. This article also investigates the manuscript copies of these compilations, revealing their use and transmission in Iran, Turkey, and Central Asia between 1470 and 1550.

The Guarded Negation Fragment (GNFO) is a fragment of first-order logic that contains all positive existential formulas, can express the first-order translations of basic modal logic and of many description logics, along with many sentences that arise in databases. It has been shown that the syntax of GNFO is restrictive enough so that computational problems such as validity and satisfiability are still decidable. This suggests that, in spite of its expressive power, GNFO formulas are amenable to novel optimizations. In this article we study the model theory of GNFO formulas. Our results include effective preservation theorems for GNFO, effective Craig Interpolation and Beth Definability results, and the ability to express the certain answers of queries with respect to a large class of GNFO sentences within very restricted logics.

Constraint Handling Rules (CHR) is both an effective concurrent declarative programming language and a versatile computational logic formalism. In CHR, guarded reactive rules rewrite a multi-set of constraints. Concurrency is inherent, since rules can be applied to the constraints in parallel. In this comprehensive survey, we give an overview of the concurrent, parallel as well as distributed CHR semantics, standard and more exotic, that have been proposed over the years at various levels of refinement. These semantics range from the abstract to the concrete. They are related by formal soundness results. Their correctness is proven as a correspondence between parallel and sequential computations. On the more practical side, we present common concise example CHR programs that have been widely used in experiments and benchmarks. We review parallel and distributed CHR implementations in software as well as hardware. The experimental results obtained show a parallel speed-up for unmodified sequential CHR programs. The software implementations are available online for free download and we give the web links. Due to its high level of abstraction, the CHR formalism can also be used to implement and analyse models for concurrency. To this end, the Software Transaction Model, the Actor Model, Colored Petri Nets and the Join-Calculus have been faithfully encoded in CHR. Finally, we identify and discuss commonalities of the approaches surveyed and indicate what problems are left open for future research.

Answer set programming (ASP) is a well-established logic programming language that offers an intuitive, declarative syntax for problem solving. In its traditional application, a fixed ASP program for a given problem is designed and the actual instance of the problem is fed into the program as a set of facts. This approach typically results in programs with comparably short and simple rules. However, as is known from complexity analysis, such an approach limits the expressive power of ASP; in fact, an entire NP-check can be encoded into a single large rule body of bounded arity that performs both a guess and a check within the same rule. Here, we propose a novel paradigm for encoding hard problems in ASP by making explicit use of large rules which depend on the actual instance of the problem. We illustrate how this new encoding paradigm can be used, providing examples of problems from the first, second, and even third level of the polynomial hierarchy. As state-of-the-art solvers are tuned towards short rules, rule decomposition is a key technique in the practical realization of our approach. We also provide some preliminary benchmarks which indicate that giving up the convenient way of specifying a fixed program can lead to a significant speed-up.