Bart Jacobs

JAIR Journal 2019 Journal Article

The Mathematics of Changing One’s Mind, via Jeffrey’s or via Pearl’s Update Rule

• Bart Jacobs

Evidence in probabilistic reasoning may be ‘hard’ or ‘soft’, that is, it may be of yes/no form, or it may involve a strength of belief, in the unit interval [0, 1]. Reasoning with soft, [0, 1]-valued evidence is important in many situations but may lead to different, confusing interpretations. This paper intends to bring more mathematical and conceptual clarity to the field by shifting the existing focus from specification of soft evidence to accomodation of soft evidence. There are two main approaches, known as Jeffrey’s rule and Pearl’s method; they give different outcomes on soft evidence. This paper argues that they can be understood as correction and as improvement. It describes these two approaches as different ways of updating with soft evidence, highlighting their differences, similarities and applications. This account is based on a novel channel-based approach to Bayesian probability. Proper understanding of these two update mechanisms is highly relevant for inference, decision tools and probabilistic programming languages.

TCS Journal 2015 Journal Article

Dijkstra and Hoare monads in monadic computation

• Bart Jacobs

The Dijkstra and Hoare monads have been introduced recently for capturing weakest precondition computations and computations with pre- and post-conditions, within the context of program verification, supported by a theorem prover. Here we give a more general description of such monads in a categorical setting. We first elaborate the recently developed view on program semantics in terms of a triangle of computations, state transformers, and predicate transformers. Instantiating this triangle for different computational monads T shows how to define the Dijkstra monad associated with T, via the logic involved. Subsequently we give abstract definitions of the Dijkstra and Hoare monad, parametrised by a computational monad. These definitions presuppose a suitable (categorical) predicate logic, defined on the Kleisli category of the underlying monad. When all this structure exists, we show that there are maps of monads (Hoare) ⇒ (State) ⇒ (Dijkstra), all parametrised by a monad T.

TCS Journal 2011 Journal Article

Preface

• Bart Jacobs
• Milad Niqui
• Jan Rutten
• Alexandra Silva

TCS Journal 2011 Journal Article

Probabilities, distribution monads, and convex categories

• Bart Jacobs

Probabilities are understood abstractly as forming a monoid in the category of effect algebras. They can be added, via a partial operation, and multiplied. This generalizes key properties of the unit interval [ 0, 1 ]. Such effect monoids can be used to define a probability distribution monad, again generalizing the situation for [ 0, 1 ] -probabilities. It will be shown that there are translations back and forth, in the form of an adjunction, between effect monoids and “convex” monads. This convexity property is formalized, both for monads and for categories. In the end, this leads to “triangles of adjunctions” (in the style of Coumans and Jacobs) relating all the three relevant structures: probabilities, monads, and categories.

TCS Journal 2004 Journal Article

Simulations in coalgebra

• Jesse Hughes
• Bart Jacobs

A new approach to simulations is proposed within the theory of coalgebras by taking a notion of order on a functor as primitive. Such an order forms a basic building block for a “lax relation lifting”, or “relator” as used by other authors. Simulations appear as coalgebras of this lifted functor, and similarity as greatest simulation. Two-way similarity is then similarity in both directions. In general, it is different from bisimilarity (in the usual coalgebraic sense), but a sufficient condition is formulated (and illustrated) to ensure that bisimilarity and two-way similarity coincide. Also, suitable conditions are identified which ensures that similarity on a final coalgebra forms an (algebraic) dcpo structure. This involves a close investigation of the iterated applications F n ( ∅ ) and F n ( 1 ) of a functor F with an order to the initial algebras and final objects.

TCS Journal 2003 Journal Article

Coalgebras and monads in the semantics of Java

• Bart Jacobs
• Erik Poll

This paper describes the basic structures in the denotational and axiomatic semantics of sequential Java, both from a monadic and a coalgebraic perspective. This semantics is an abstraction of the one used for the verification of (sequential) Java programs using proof tools in the LOOP project at the University of Nijmegen. It is shown how the monadic perspective gives rise to the relevant computational structure in Java (composition, extension and repetition), and how the coalgebraic perspective offers an associated program logic (with invariants, bisimulations, and Hoare logics) for reasoning about the computational structure provided by the monad.

TCS Journal 2002 Journal Article

Foreword

• Bart Jacobs
• Jan Rutten

TCS Journal 2001 Journal Article

Foreword

• Bart Jacobs
• Larry Moss
• Horst Reichel
• Jan Rutten

TCS Journal 2000 Journal Article

Object-oriented hybrid systems of coalgebras plus monoid actions

• Bart Jacobs

Hybrid systems combine discrete and continuous dynamics. We introduce a semantics for such systems consisting of a coalgebra together with a monoid action. The coalgebra captures the (discrete) operations on a state space that can be used by a client (like in the semantics of ordinary (non-temporal) object-oriented systems). The monoid action captures the influence of time on the state space, where the monoids that we consider are the natural numbers monoid (N, 0, +) of discrete time, and the positive reals monoid (R ⩾0, 0, +) of real time. Based on this semantics we develop a hybrid specification formalism with timed method applications: it involves expressions like s. meth @α, with the following meaning: in state s let the state evolve for α units of time (according to the monoid action), and then apply the (coalgebraic) method meth. In this formalism we specify various (elementary) hybrid systems, investigate their correctness, and display their behaviour in simulations. We further define a suitable notion of homomorphism between our hybrid models (of coalgebras plus monoid actions), in such a way that minimal realizations (of the specified behaviour) appear as terminal models. We identify the terminal models of our example specifications, and give general constructions. This leads to an investigation of various topics related to terminality: bisimilarity, invariance, refinement and behaviour-realization adjunctions. In a final section we briefly discuss non-homogeneous hybrid systems (with continuous inputs).

TCS Journal 1995 Journal Article

Duality beyond sober spaces: Topological spaces and observation frames

• Marcello M. Bonsangue
• Bart Jacobs
• Joost N. Kok

We introduce observation frames as an extension of ordinary frames. The aim is to give an abstract representation of a mapping from observable predicates to all predicates of a specific system. A full subcategory of the category of observation frames is shown to be dual to the category of T 0 topological spaces. The notions we use generalize those in the adjunction between frames and topological spaces in the sense that we generalize finite meets to infinite ones. We also give a predicate logic of observation frames with both infinite conjunctions and disjunctions, just like there is a geometric logic for (ordinary) frames with infinite disjunctions but only finite conjunctions. This theory is then applied to two situations: firstly to upper power spaces, and secondly we restrict the adjunction between the categories of topological spaces and of observation frames in order to obtain dualities for various subcategories of T 0 spaces. These involve nonsober spaces.

TCS Journal 1993 Journal Article

Comprehension categories and the semantics of type dependency

• Bart Jacobs

A comprehension category is defined as a functor P: E→B → satisfying (a) a cod ∘ P is a fibration, and (b) f is cartesian in E implies that P f is a pullback in B. This notion captures many structures which are used to describe type dependency (like display-map categories (Taylor (1986), Hyland and Pitts (1989) and Lamarche (1988)), categories with attributes (Cartmell (1978) and Moggi (1991)), D-categories (Ehrhard (1988)) and comprehensive fibrations (Pavlović (1990)). It also captures comprehension as occurring in topos theory and as described by Lawvere's (1970)) hyperdoctrines. This paper is meant as an introduction to these comprehension categories. A comprehension category will be called closed if it has appropriate dependent products and sums. A few examples of closed comprehension categories will be described here; more of them may be found in Jacobs (1991); applications occur in Jacobs (1991) and Jacobs et al. (1991).

TCS Journal 1992 Journal Article

Filter models with polymorphic types

• Bart Jacobs
• Ines Margaria
• Maddalena Zacchi

Using ideas and results from Barendrecht (1983) and Coppo (1984) on intersection types, a comparable theory is developed for (second order) polymorphic types. The set of filters constructed with polymorphic type forms, with inclusion, a continuous lattice which yields a model of what we call βη-expansion (i. e. the value of a term increases under βη-reduction), but not of β-conversion. Combining intersection with polymorphic types does give filter λ-models, but the two standard ways of interpreting λ-terms do not coincide.