This paper studies normalisation by evaluation for typed lambda calculus from a categorical and algebraic viewpoint. The first part of the paper analyses the lambda definability result of Jung and Tiuryn via Kripke logical relations and shows how it can be adapted to unify definability and normalisation, yielding an extensional normalisation result. In the second part of the paper, the analysis is refined further by considering intensional Kripke relations (in the form of Artin–Wraith glueing) and shown to provide a function for normalising terms, casting normalisation by evaluation in the context of categorical glueing. The technical development includes an algebraic treatment of the syntax and semantics of the typed lambda calculus that allows the definition of the normalisation function to be given within a simply typed metatheory. A normalisation-by-evaluation program in a dependently typed functional programming language is synthesised.

We describe quantum circuits generating four-qubit maximally entangled states, the amount of entanglement being quantified by using the absolute value of the Cayley hyperdeterminant as an entanglement monotone. More precisely we show that this type of four-qubit entangled states can be obtained by the action of a family of $\mathtt{CNOT}$ circuits on some special states of the LU orbit of the state $|0000\rangle$ .

A model of Martin-Löf extensional type theory with universes is formalized in Agda, an interactive proof system based on Martin-Löf intensional type theory. This may be understood, we claim, as a solution to the old problem of modeling the full extensional theory in the intensional theory. Types are interpreted as setoids, and the model is therefore a setoid model.We solve the problem of interpreting type universes by utilizing Aczel’s type of iterative sets and show how it can be made into a setoid of small setoids containing the necessary setoid constructions. In addition, we interpret the bracket types of Awodey and Bauer. Further quotient types should be interpretable.

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.

Bishop’s presentation of his informal system of constructive mathematics BISH was on purpose closer to the proof-irrelevance of classical mathematics, although a form of proof-relevance was evident in the use of several notions of moduli (of convergence, of uniform continuity, of uniform differentiability, etc.). Focusing on membership and equality conditions for sets given by appropriate existential formulas, we define certain families of proof sets that provide a BHK-interpretation of formulas that correspond to the standard atomic formulas of a first-order theory, within Bishop set theory $(\mathrm{BST})$ , our minimal extension of Bishop’s theory of sets. With the machinery of the general theory of families of sets, this BHK-interpretation within BST is extended to complex formulas. Consequently, we can associate to many formulas $\phi$ of BISH a set ${\texttt{Prf}}(\phi)$ of “proofs” or witnesses of $\phi$ . Abstracting from several examples of totalities in BISH, we define the notion of a set with a proof-relevant equality, and of a Martin-Löf set, a special case of the former, the equality of which corresponds to the identity type of a type in intensional Martin-Löf type theory $(\mathrm{MLTT})$ . Through the concepts and results of BST notions and facts of MLTT and its extensions (either with the axiom of function extensionality or with Vooevodsky’s axiom of univalence) can be translated into BISH. While Bishop’s theory of sets is standardly understood through its translation to MLTT, our development of BST offers a partial translation in the converse direction.

The paper describes three models of the real field based on subsets of the integer sequences. The three models are compared to the Harthong–Reeb line. Two of the new models, contrary to the Harthong–Reeb line, provide accurate integer “views” on real numbers at a sequence of growing scales $B^n$ ( $B\ge2$ ).

It is well known that classical varieties of $\Sigma$ -algebras correspond bijectively to finitary monads on $\mathsf{Set}$ . We present an analogous result for varieties of ordered $\Sigma$ -algebras, that is, categories of algebras presented by inequations between $\Sigma$ -terms. We prove that they correspond bijectively to strongly finitary monads on $\mathsf{Pos}$ . That is, those finitary monads which preserve reflexive coinserters. We deduce that strongly finitary monads have a coinserter presentation, analogous to the coequalizer presentation of finitary monads due to Kelly and Power. We also show that these monads are liftings of finitary monads on $\mathsf{Set}$ . Finally, varieties presented by equations are proved to correspond to extensions of finitary monads on $\mathsf{Set}$ to strongly finitary monads on $\mathsf{Pos}$ .

We study combinatorial and order theoretic structures arising from the fragment of combinatory logic spanned by the basic combinator ${{\mathbf{M}}}$ . This basic combinator, named as the Mockingbird by Smullyan, is defined by the rewrite rule ${{\mathbf{M}}} \mathsf{x}_1 \to \mathsf{x}_1 \mathsf{x}_1$ . We prove that the reflexive and transitive closure of this rewrite relation is a partial order on terms on ${{\mathbf{M}}}$ and that all connected components of its rewrite graph are Hasse diagram of lattices. This last result is based on the introduction of new lattices on duplicative forests, which are sorts of treelike structures. These lattices are not graded, not self-dual, and not semi-distributive. We present some enumerative properties of these lattices like the enumeration of their elements, of the edges of their Hasse diagrams, and of their intervals. These results are derived from formal power series on terms and on duplicative forests endowed with particular operations.

In this paper, we address the problem of proving confluence for string diagram rewriting, which was previously shown to be characterised combinatorially as double-pushout rewriting with interfaces (DPOI) on (labelled) hypergraphs. For standard DPO rewriting without interfaces, confluence for terminating rewriting systems is, in general, undecidable. Nevertheless, we show here that confluence for DPOI, and hence string diagram rewriting, is decidable. We apply this result to give effective procedures for deciding local confluence of symmetric monoidal theories with and without Frobenius structure by critical pair analysis. For the latter, we introduce the new notion of path joinability for critical pairs, which enables finitely many joins of a critical pair to be lifted to an arbitrary context in spite of the strong non-local constraints placed on rewriting in a generic symmetric monoidal theory.

Sharing analysis is used to statically discover data structures which may overlap in object-oriented programs. Using the abstract interpretation framework, we show that sharing analysis greatly benefits from linearity information. A variable is linear in a program state when different field paths starting from it always reach different objects. We propose a graph-based abstract domain which can represent aliasing, linearity, and sharing information and define all the necessary abstract operators for the analysis of a Java-like language.

Based on the framework of disjunctive propositional logic, we first provide a syntactic representation for Scott domains. Precisely, we establish a category of consistent disjunctive sequent calculi with consequence relations, and show it is equivalent to that of Scott domains with Scott-continuous functions. Furthermore, we illustrate the approach to solving recursive domain equations by introducing some standard domain constructions, such as lifting and sums. The subsystems relation on consistent finitary disjunctive sequent calculi makes these domain constructions continuous. Solutions to recursive domain equations are given by constructing the least fixed point of a continuous function.

Cartesian reverse differential categories (CRDCs) are a recently defined structure which categorically model the reverse differentiation operations used in supervised learning. Here, we define a related structure called a monoidal reverse differential category, prove important results about its relationship to CRDCs, and provide examples of both structures, including examples coming from models of quantum computation.

This work concerns the representation of a class of continuous functions into Logic, so that one may automatically reason about properties of these functions using logical tools. Rational McNaughton functions may be implicitly represented by logical formulas in Łukasiewicz Infinitely-valued Logic by constraining the set of allowed valuations; such a restriction contemplates only those valuations that satisfy specific formulas. This work investigates two approaches to such depiction, called representation modulo satisfiability. Furthermore, a polynomial-time algorithm that builds this representation is presented, producing a pair of formulas consisting of the representative formula and the constraining one, given as input a rational McNaughton function in a suitable encoding. An implementation of the algorithm is discussed.

The family ${\mathcal{R}} X^*$ of regular subsets of the free monoid $X^*$ generated by a finite set X is the standard example of a ${}^*$ -continuous Kleene algebra. Likewise, the family ${\mathcal{C}} X^*$ of context-free subsets of $X^*$ is the standard example of a $\mu$ -continuous Chomsky algebra, i.e. an idempotent semiring that is closed under a well-behaved least fixed-point operator $\mu$ . For arbitrary monoids M, ${\mathcal{C}} M$ is the closure of ${\mathcal{R}}M$ as a $\mu$ -continuous Chomsky algebra, more briefly, the fixed-point closure of ${\mathcal{R}} M$ . We provide an algebraic representation of ${\mathcal{C}} M$ in a suitable product of ${\mathcal{R}} M$ with $C_2'$ , a quotient of the regular sets over an alphabet $\Delta_2$ of two pairs of bracket symbols. Namely, ${\mathcal{C}}M$ is isomorphic to the centralizer of $C_2'$ in the product of ${\mathcal{R}} M$ with $C_2'$ , i.e. the set of those elements that commute with all elements of $C_2'$ . This generalizes a well-known result of Chomsky and Schützenberger (1963, Computer Programming and Formal Systems, 118–161) and admits us to denote all context-free languages over finite sets $X\subseteq M$ by regular expressions over $X\cup\Delta_2$ interpreted in the product of ${\mathcal{R}} M$ and $C_2'$ . More generally, for any ${}^*$ -continuous Kleene algebra K the fixed-point closure of K can be represented algebraically as the centralizer of $C_2'$ in the product of K with $C_2'$ .

In this paper, in connection with the program of extending the Curry–Howard isomorphism to classical logic, we study the $\lambda \mu$ -calculus of Parigot emphasizing the difference between the original version of Parigot and the version of de Groote in terms of normalization properties. In order to talk about a satisfactory representation of the integers, besides the usual $\beta$ -, $\mu$ -, and $\mu '$ -reductions, we consider the $\lambda \mu$ -calculus augmented with the reduction rules $\rho$ , $\theta$ and $\varepsilon$ . We show that we need all of these rules for this purpose. Then we prove that, with the syntax of Parigot, the calculus enjoys the strong normalization property even when we add the rules $\rho$ , $\theta$ , and $\epsilon$ , while the $\lambda \mu$ -calculus presented with the more flexible de Groote-style syntax, in contrast, has only the weak normalization property. In particular, we present a normalization algorithm for the $\beta \mu \mu '\rho \theta \varepsilon$ -reduction in the de Groote-style calculus.