We build a logical system named a conjunctive sequent calculus which is a conjunctive fragment of the classical propositional sequent calculus in the sense of proof theory. We prove that a special class of formulae of a consistent conjunctive sequent calculus forms a bounded complete continuous domain without greatest element (for short, a proper BC domain), and each proper BC domain can be obtained in this way. More generally, we present conjunctive consequence relations as morphisms between consistent conjunctive sequent calculi and build a category which is equivalent to that of proper BC domains with Scott-continuous functions. A logical characterization of purely syntactic form for proper BC domains is obtained.

Network models, which abstractly are given by lax symmetric monoidal functors, are used to construct operads for modeling and designing complex networks. Many common types of networks can be modeled with simple graphs with edges weighted by a monoid. A feature of the ordinary construction of network models is that it imposes commutativity relations between all edge components. Because of this, it cannot be used to model networks with bounded degree. In this paper, we construct the free network model on a given monoid, which can model networks with bounded degree. To do this, we generalize Green’s graph products of groups to pointed categories which are finitely complete and cocomplete.

Recurrence can be used as a function definition schema for any nontrivial free algebra, yielding the same computational complexity in all cases. We show that primitive-recursive computing is in fact independent of free algebras altogether, and can be characterized by a generic programming principle, namely the control of iteration by the depletion of finite components of the underlying structure.

A desired closure property in Bayesian probability is that an updated posterior distribution be in the same class of distributions – say Gaussians – as the prior distribution. When the updating takes place via a statistical model, one calls the class of prior distributions the ‘conjugate priors’ of the model. This paper gives (1) an abstract formulation of this notion of conjugate prior, using channels, in a graphical language, (2) a simple abstract proof that such conjugate priors yield Bayesian inversions and (3) an extension to multiple updates. The theory is illustrated with several standard examples.

This paper surveys a new perspective on tree automata and Monadic second-order logic (MSO) on infinite trees. We show that the operations on tree automata used in the translations of MSO-formulae to automata underlying Rabin’s Tree Theorem (the decidability of MSO) correspond to the connectives of Intuitionistic Multiplicative Exponential Linear Logic (IMELL). Namely, we equip a variant of usual alternating tree automata (that we call uniform tree automata) with a fibered monoidal-closed structure which in particular handles a linear complementation of alternating automata. Moreover, this monoidal structure is actually Cartesian on non-deterministic automata, and an adaptation of a usual construction for the simulation of alternating automata by non-deterministic ones satisfies the deduction rules of the !(–) exponential modality of IMELL. (But this operation is unfortunately not a functor because it does not preserve composition.) Our model of IMLL consists in categories of games which are based on usual categories of two-player linear sequential games called simple games, and which generalize usual acceptance games of tree automata. This model provides a realizability semantics, along the lines of Curry–Howard proofs-as-programs correspondence, of a linear constructive deduction system for tree automata. This realizability semantics, which can be summarized with the slogan “automata as objects, strategies as morphisms,” satisfies an expected property of witness extraction from proofs of existential statements. Moreover, it makes it possible to combine realizers produced as interpretations of proofs with strategies witnessing (non-)emptiness of tree automata.