View: session overviewtalk overviewside by side with other conferences

09:00 | Invited Talk: Approximating partial by total: fixpoint characterizations of back-and-forth equivalences ABSTRACT. Model comparison games such as Ehrenfeucht-Fraisse, pebble and bisimulation games play a central role in finite and infinite model theory, modal logic and concurrency theory. We show how such games can be understood in terms of comonads on the category of relational structures and homomorphisms. This leads to novel syntax-free characterizations of the equivalences induced by a wide range of logics, and coalgebraic characterizations of key combinatorial parameters such as tree-width and tree-depth. This in turn leads to a novel analysis of back-and-forth equivalences. Instead of considering partial isomorphisms with back- and forth- extension properties, we show how they can be characterized in a uniform fashion in terms of sets of coKleisli morphisms for the associated comonads, satisfying a local invertibility condition. This leads in turn to a fixpoint characterization. An interesting feature of this characterization is that we are approximating partial maps by (sets of) total ones, and replacing extension properties with a greatest fixpoint computation. |

09:40 | Diffeological Spaces and Semantics for Differential Programming SPEAKER: Matthijs Vákár ABSTRACT. Differential programming, particularly systems based on Automatic Differentiation, has recently become a popular method to approach high-dimensional optimisation and integration problems found in machine learning and computational statistics. Examples of systems relying on these techniques are TensorFlow and Stan. The semantics of such systems, however, still remains rather poorly understood. In particular, it is unclear how differentiation should interact with more traditional computer science concepts like recursion. For these purposes, we are exploring a rich semantic framework for differential programming based on generalised smooth spaces known as diffeological spaces. We demonstrate how to construct Fiore's axiomatic domain theory in this setting. |

10:05 | Domain Theory for Intensional Computation ABSTRACT. Intensional computation supports generic queries of internal structure as well as the extensional computation familiar from lambda-calculus and combinatory logic. This paper introduces a denotational semantics for the simplest intensional calculus, namely SF-calculus. Its domain has a basis given by the normal forms of the calculus, extended with a least element. Their functionality is revealed by a mapping from the domain to its function space that is determined by the reduction rules of the calculus. Conversely, step-functions correspond to simple pattern-matching functions. These are representable in SF-calculus, which yields a right inverse to the mapping above. However, this semantics fails for traditional combinatory logic (SK-calculus) as the corresponding mapping into the function space does not have a right inverse. This is because combinatory logic cannot represent enough pattern-matching functions, cannot support intensional computation. This result complements the syntactic proof that SF-calculus is more expressive than SK-calculus. |

11:00 | Invited Talk: A domain theory for quasi-Borel spaces and statistical probabilistic programming ABSTRACT. I will describe ongoing work investigating a convenient category of pre-domains and a probabilistic powerdomain construction suitable for statistical probabilistic programming semantics, as used in statistical modelling and machine learning. Specifically, we provide (1) a cartesian closed category; (2) whose objects are (pre)-domains; and (3) a commutative monad for probabilistic choice and Bayesian conditioning. Jones and Plotkin have shown that conditions (2)--(3) hold when one restricts attention to continuous domains, and Jung and Tix have proposed to search for a suitable category of continuous domains possessing all three properties (1)--(3), a question that remains open to date. I propose an alternative direction, considering spaces with separate, but compatible, measure-theoretic and domain-theoretic structures. On the domain-theoretic side, we require posets with suprema of countably increasing chains (omega-cpos). On the measure-theoretic side, we require a quasi-Borel space (qbs) structure, a recently introduced algebraic structure suitable for modelling higher-order probability theory. There are three equivalent characterisations of this category given by: imposing an order-theoretic separatedness condition on countable-preserving omega-cpo-valued presheaves; internal omega-cpos in the quasi-topos of quasi-Borel spaces; and an essentially algebraic presentation. The category of these omega-qbses validates Fiore and Plotkin's axiomatic domain theory, yielding semantics for recursive types. To conclude, I will describe a commutative powerdomain construction given by factorising the Lebesgue integral from the space of random elements to the space of sigma-linear integration operators. |

11:40 | Abstractness of Continuation Semantics for Asynchronous Concurrency SPEAKER: Eneia Nicolae Todoran ABSTRACT. The full abstractness problem was raised by Robin Milner and the diculty of designing fully abstract semantics is well-known. A denotational semantics is said to be fully abstract if it is correct and complete. The correctness condition is usually easy to establish. However, it may be difficult to establish the completeness condition. In this paper we study the abstractness of denotational models designed with continuation semantics for concurrency (CSC). Due to the interplay between denotations and continuations, the full abstractness problem seems to be even more dicult in continuation semantics. Although several papers employ continuations in the denotational design of concurrent languages, we are not aware of any full abstractness result for a concurrent language designed with continuations. Therefore we introduce a new criterion that we name weak abstractness (which is specific of the CSC technique): it preserves the correctness condition, but relaxes the completeness condition of the classic full abstractness criterion. Weak abstractness may be useful for a wide class of denotational models designed with continuations in which full abstractness is difficult (or impossible) to achieve. To illustrate this approach we present a denotational model for a simple asynchronous concurrent language designed with continuations over metric spaces. We show that this denotational semantics is weakly abstract with respect to a corresponding operational model. |

12:05 | Algebra semantics of recursive computation types SPEAKER: Paul Blain Levy ABSTRACT. Giving algebra semantics for recursive computation types in a language with effects has been an open problem. We explain how to solve it by expanding the category of cppo algebras to Fiore's category in which the maps are lax homomorphisms. |

16:00 | Frames and frame relations SPEAKER: Imanol Mozo Carollo ABSTRACT. We follow two threads in Dana Scott's mathematics to study frames in a different light. First, injectivity is an important idea. Second, relational reasoning can get at functional behavior (via, for example, approximable maps). These will permit us to situate frames in larger ambient categories in which constructions arise from the combination of injectivity and relational reasoning. In particular, the assembly of a frame comes about as being isomorphic to a sublocale \(\mathcal{Q}(L)\) of the frame of endo-relations on a given frame. We prove this by showing directly that \(\mathcal{Q}(L)\) has the universal property of the assembly. From independent discoveries (Bruns and Lakser \cite{BL70}; Horn and Kimura \cite{HK71}), we know that frames are precisely the injective (meet) semilattices. Simply knowing this does not get us very far in studying frames \emph{qua} frames. But the full subcategory of \(\textsf{SL}\) consisting of injective semilattices comes closer. A semilattice map \(\fromto hML\) between two frames can be viewed ``approximably'' as a relation \(R_h\subseteq L\times M\) defined by \(x\leq h(y)\). Such a relation is closed under weakening: \(x\leq x'\), \(x' \mathrel{R_h}y'\) and \(y'\leq y\) implies \(x\mathrel{R_h}y\). It is a subframe of \(L\times M\). Any such relation, called a \emph{frame relation}, determines a semilattice homomorphism. So the category \(\overline{\textsf{Frm}}\) of frames and frame relations is opposite to the full subcategory of \(\textsf{SL}\) consisting of injective semilattices. In \(\overline{\textsf{Frm}}\), an adjoint pair of morphisms, i.e., an adjoint pair of frame relations corresponds to an adjoint pair of semilattice homomorphisms. So by adjunction, the lower adjoint determines a semilattice homomorphism preserving all joins. Thus the category \(\textsf{Map}(\textsf{Frm})\), consisting of frames and adjoint pairs of frame relations \((\check f\dashv \hat f)\), is isomorphic to the category \(\textsf{Frm}\). A subobject (a sublocale) is then an isomorphism class of extremal epimorphisms in this category. One can check that a sublocale of a frame \(L\) corresponds exactly to an idempotent, reflexive frame relation. What we have said so far is mostly known, at least in folklore. Nevertheless, this points toward studying frames directly via frame relations, as they are (dual to) the natural morphisms of injective semilattices. To illustrate the point, we construct the assembly of a frame via frame relations, showing that its familiar universal property comes about naturally from this approach. Between any two posets \(P\) and \(Q\), the weakening relations from \(P\) to \(Q\) obviously form a completely distributive lattice, hence a frame. If \(P\) is a meet semilattice and \(Q\) is a join semilattice, then the Heyting structure is especially easy to define; \(x\mathrel{(\Phi\to\Psi)}y\) if and only if for all \(w\) and \(z\) \(w\mathrel{\Phi}z\) implies \(w\wedge x\mathrel{\Psi} y\vee z\). One uses this to show that if \(L\) and \(M\) are frames, then the collection of all frame relations \(\overline{\textsf{Frm}}(L,M)\) is in fact a sublocale of the frame of all weakening relations. But composition of frame relations preserves only finite meets, and not arbitrary joins. So it is natural to consider the homsets as injective semilattices and not as frames, per se. Though we continue to call them frames, this suggests that we are actually studying the injective semilattice enriched category of injective semilattices. For a frame \(L\), the frame \(\overline{\textsf{Frm}}(L,L)\) includes the reflexive, idempotent frame relations. These, as we have noted, correspond to sublocales of \(L\). Clearly, they are closed under arbitrary intersections. And a simple calculation using the Heyting arrow shows that they constitute a sublocale of \(\overline{\textsf{Frm}}(L,L)\), denoted by \(\mathcal{Q}(L)\). Moreover, \(L\) embeds in \(\mathcal{Q}(L)\) via the map sending \(a\in L\) to the frame relation \(x\mathrel{\Gamma_a}y\) if and only if \(x\leq y\wedge a\). Note that \(\Gamma_a\) corresponds to the closed sublocale of \(a\). The relation corresponding to the open sublocale is \(x\mathrel{\Upsilon_a}y\) if and only if \(a\vee x\leq y\). Any adjoint pair \(\check f\dashv \hat f\) of frame relations between \(L\) and \(M\) extends by composition with the embedding of \(L\) in \(\mathcal{Q}(L)\) to a pair of frame relations \(f^*,f_*\) between \(\mathcal{Q}(L)\) and \(M\). These \emph{extend} \(\check f\) and \(\hat f\) in a natural way, and furthermore \(f^*;f_* \leq 1_M\). It is natural to ask when these are in fact adjoint. The frame \(M\) has a \emph{center} relation: \(a\prec^*_M b\) if and only if there is some complemented \(w\) so that \(a\leq w\leq b\). Now if \(f=(\check f\dashv \hat f)\) is an adjoint pair of frame relations so that \(\check f;\hat f\subseteq \mathord{\prec^*_M}\), then \(f^*\dashv f_*\) is the unique adjoint pair extending \(f\) along \(\Gamma\). Conversely, using the injectivity of \(M\) and \(\mathcal{Q}(L)\), if \(f^*\) is adjoint to \(f_*\), then \(\check f;\hat f\subseteq \mathord{\prec^*_M}\). Hence, \(\mathcal{Q}(L)\) has the universal property that any adjoint pair of frame relations from \(L\) to \(M\) that sends \(L\) to the center of \(M\) factors uniquely through \(\Gamma\). \begin{references}{99} \bibitem{BL70} Bruns, G. and Lakser, H. Injective hulls of semilattices. \emph{Canadian Mathematics Bulletin}, \textbf{13} (1970), 115--118. \bibitem{HK71} Horn, A. and Kimura, N. The category of semilattices. \emph{Algebra Universalis}, \textbf{1} (1971), 26--38. \end{references} |

16:25 | Extending Stone Duality to Relations SPEAKER: M. Andrew Moshier ABSTRACT. The importance of, on the one hand, categories of relations and, on the other hand, Stone Duality does not seem to be in need of much justification in a workshop on domain theory. The purpose of this presentation is to explain how both can be combined. In other words, given a concrete duality in which arrows are structure preserving functions, extend this duality to a duality of the corresponding categories of relations (Thm 1). We will use this approach to give a reconstruction of domain logics for non-zero dimensional spaces (Thm 2), based on Scott's idea of moving from algebraic to continuous lattices by splitting certain idempotents. |

16:50 | Applications of entailments: de Groot duality ABSTRACT. We study interaction between de Groot duality and the semantic domains of various choices (i.e. powerlocale constructions) on stably compact locales. We give a simple point-free account of the duality on several powerlocale constructions. This is done via the representation of a stably compact locale by means of Scott’s entailment relation with an idempotent relation due to Coquand and Zhang [Theoret. Comput. Sci., 305(1-3):77–84, 2003]. |