Domains X 2011 - Abstracts

Invited talks

Nick Benton (Microsoft Research, United Kingdom) Ultrametric Spaces and Reactive Programming

Reactive systems engage in extended interactions with their environments, consuming input events and producing corresponding output events. Examples range from embedded controllers to graphical user interfaces, simulations and games. Synchronous dataflow languages have been very successful as a way of programming reactive systems, but present a somewhat restricted, first-order computational model. At the other end of the spectrum, functional reactive programming (FRP) implements a rich, higher-order model, but does not enforce causality or well-definedness. I'll describe some work that Neel Krishnaswami, Jan Hoffmann and I have been doing on an approach to reactive programming that derives from a denotational semantics in the Cartesian closed category of ultrametric spaces and non-expansive maps. The model supports higher-order features whilst still enforcing causality and well-foundedness of recursive definitions. I'll also talk about the imperative implementation of a language based on this model, its use for writing GUIs, and a further refinement that also bounds the space usage of reactive programs.

Lars Birkedal (Copenhagen, Denmark) A Logic of Sequentiality

We present the topos of trees S as a model of guarded recursion. We study the internal dependently-typed higher-order logic of S and show that S models two modal operators, on predicates and types, which serve as guards in recursive definitions of terms, predicates, and types. In particular, we show how to solve recursive type equations involving dependent types. We propose that the internal logic of S provides the right setting for the synthetic construction of abstract versions of step-indexed models of programming languages and program logics. As an example, we show how to construct a model of a programming language with higher-order store and recursive types entirely inside the internal logic of S.

Margarita Korovina (Manchester, United Kingdom) Time Optimal Control for Polynomial Dynamical Systems (Joint work with Nicolai Vorobjov Univ. of Bath)

A fundamental problem in the design of biological, chemical or physical processes is to automatically synthesise models from performance specifications. In general, by practical and theoretical reasons, it is highly non-trivial to achieve. However, in some cases, given by partial designs, it could be possible to automatically complete modelling in order to get desired properties. In this talk we discuss synthesis of finite control strategies to meet reachability and time requirements for partial designs given by controlled polynomial dynamical systems.

Dag Normann (Oslo, Norway) Fixed point computability of total functionals

We introduce the Kleene-Kreisel continuous functionals via the limit space characterization in order to see how much of the computability theory of these functionals we can develop within this framework. In order to go beyond mu-recursion, we consider fixed points of computable contractors at all types. It turns out that there is a natural class of total contractors that will generate exactly the externally computable functionals. The talk may be considered as a survey talk on the computability theory of the continuous functionals, and the aim is to simplify proofs of some basic facts.

John Power (Bath, United Kingdom) An Historical Reflection on Monads as Notions of Computation

In the late 1980's, Eugenio Moggi introduced the idea of monads as notions of computation, and that has since been adopted perhaps most prominently by the Haskell community. The notion of monad had been used by category theorists for twenty years, but for different purposes and with different examples. Kleisli categories, which were the construction of primary interest to Moggi, had been used a little, but not much. The theory of monads, prior to Moggi's work, had focused primarily on universal algebra. But Moggi did not adopt that, and neither did successors, despite universal algebra being well known and used by closely related theoretical computer scientists, for instance in algebraic specification. So how did we get here? Could other choices have been made, either by Moggi or by others? Could other choices, if developed now, lead to a richer body of theory of computational effects? These are the questions we consider here. The relevant history stretches back at least to the 1930's and suggests new research directions now.

Matija Pretnar (Ljubljana, Slovenia) The f-calculus

To see how useful Plotkin and Power's algebraic effects are in programming, Andrej Bauer and I have developed a language called eff, based on such an approach. As it turns out, eff is very suitable for writing programs that use nondeterminism, rollback, delimited continuations, scheduling, and many other effects. In the talk, I will present the f-calculus, which formalizes eff's core, its type system, and its semantics.

Thomas Streicher (Darmstadt, Germany) Quantum Theory in Topological Domain Theory

The Hilbert lattice $\mathcal{L}$ of closed subspaces of separable infinite dimensional Hilbert space $\mathcal{H}$ is not a continuous lattice. Still one might want to develop a kind of Synthetic Domain Theory where the role of Sierpi\'nski space $\Sigma$ is played by $\mathcal{L}$. In our talk we investigate how this is possible in the framework of Simpson and Schr\"oder's Topological Domain Theory based on the observation that $\mathcal{L}$ lives in $\mathbf{QCB}_0$, the $\Sigma$-extensional objects of the function realizability topos.

Jeff Zucker (McMaster, Canada) Analog systems: Continuity and Computability

We study the semantics of networks of streams of data from a complete metric space. We develop these semantics as stream transformers, given as the fixed points of contracting operators on the stream spaces. We consider two types of data streams: those based on continuous time (used in networks of analog modules and channels), and those based on discrete time (used in synchronous concurrent algorithms), in both cases with global clocks. We combine their study into a unified theory, and develop this theory by proving certain desirable properties of these fixed point semantic functions, namely continuity and (concrete and abstract) computability.

Contributed talks

Steffen Van Bakel, Franco Barbanera and Ugo De Liguoro: A Domain Logic Approach to Models of $\lambda\mu$ and Related Calculi

We present a filter-domain which is an instance of Streicher and Reus's continuation model for $\lambda\mu$-calculus in the category of $\omega$-algebraic lattices. The construction is based on (a simplified form of) Abramsky's theory of domains in logical form, namely the domains $R$, $D$ and $C$ satisfying the equations $D = C \to R$ and $C = D \times C$ are described via languages and theories of types whose Lindembaum algebras are isomorphic to their compact substructures. By considering w.r.t. this model the interpretation of Parigot's $\lambda\mu$ we reconstruct an intersection type assignment system for the pure calculi. Such an assignment system comes out to be sound and complete w.r.t. continuation models, and in fact it enjoys the fundamental property of being invariant under subject reduction and expansion. The system can be easily adapted e.g. to de Groote's variant, known as $\Lambda\mu$. The meaning of types in our sense is obviously different than logical formulas, and every pure $\lambda\mu$-term has a type in our system, possibly the trivial one which we call $\omega$ as usual in the Coppo-Dezani intersection type assignment systems. However we also show that any term which is typeable either in Parigot's or in de Groote's type assignement system, has a non trivial type in the respective intersection assignment systems, and that this is the case for all its subterms. This fact is related to Pottinger's theorem, characterizing strongly normalising pure $\lambda$-terms in terms of their non-trivial typings in intersection type assignment systems.

Ingo Battenfeld: Observationally-induced lower and upper powerspace constructions

In recent work we have investigated lower and upper powerspace constructions in the vein of Alex Simpson's observationally-induced approach to computational monads, which is based on the idea of defining algebraic and completeness properties from a pre-chosen computational prototype. In the category of topological spaces and continuous maps, a suitable prototype for the lower powerspace construction is given by Sierpinski space with the join-operation, and for the upper powerspace construction it is given by Sierpinski space with the meet-operation. It turns out that our constructions generalise the lower and upper powerdomain constructions known from classical domain theory. In particular, one has that for every topological space, the observationally-induced lower powerspace is given by its set of nonempty closed subsets equipped with the lower Vietoris topology. On the other hand, the observationally-induced upper powerspace for a topological space satisfying the Wilker condition is given by the Scott-open filters of its topology equipped with the upper Vietoris topology. In essence, the Wilker condition can be described as a decomposition property of open filters - or on sober spaces as a decomposition property of compact subsets. We do not know if the Wilker condition is necessary for the upper powerspace construction to be given by the Scott-open filters. However, there is a counterexample showing that this characterisation does not hold for arbitrary topological spaces. We shall give a detailed account of the observationally-induced lower and upper powerspace constructions, describing in which aspects their constructions correspond to each other and in which aspects they do not. We shall also present the counterexample, which is a non-sober compact sequential topological space in which sequences have unique limits, and examine its topological properties in the hope to elaborate properties which imply the familiar characterisation to fail. This is joint work with Matthias Schröder and the results have been presented at this year's MFPS.

Andrej Bauer and Karin Cvetko Vah: Stone Duality for Skew Boolean Algebras with Intersections

Classical Stone duality states that the category of generalized Boolean algebras, or the category of idempotent rings, is dual to the category of Boolean spaces, which are the zero-dimensional locally-compact Hausdorff spaces. We extend the duality to a non-commutative setting. We first show that right- handed skew Boolean algebras with intersections are dual to the category of surjective etale maps between Boolean spaces. We then extend the duality to all skew Boolean algebras with intersections, and consider several variations in which the morphisms are restricted. Finally, we use the duality to construct a right-handed skew Boolean algebra without a lattice section, which solves the open question of existence of such structures.
The full version of the paper is available at arXiv:1106.0425.

Paul Bilokon and Abbas Edalat: Towards a domain-theoretic, computable approach to stochastic processes

We represent discrete-time stochastic processes on the real line as the set of maximal elements of the powerdomain on powers of interval domains. This enables us to define a computable stochastic process as the least upper bound on an increasing chain of simple valuations satisfying certain convergence criteria. A continuous-time stochastic process is represented as a weakly continuous function from the time interval [0, 1] to a probabilistic powerdomain. The corresponding function space is a continuous domain but it is not bounded-complete. However, given a stochastic process, we construct an increasing chain of step functions and show that it converges to this stochastic process. We use this construction to define an effectively given stochastic process as the least upper bound of increasing step functions satisfying certain convergence criteria. These constructions enable us to compute useful probabilistic quantities. In particular, they enable us to take expectations.

Ernst-Erich Doberkat: Towards a coalgebraic interpretation of PDL

The interpretation of propositional dynamic logic (PDL) through the usual methods of modal logics using Kripke models requires that the relations in the interpreting Kripke model closely observe the syntactic of the modal operators. For example, the nondeterministic choice $\pi\cup\pi'$ of programs $\pi$ and $\pi'$ is usually interpreted through relation $R_{\pi\cup\pi'}$ which satisfies $R_{\pi\cup\pi'}=R_{\pi}\cup R_{\pi'}$, and the relation for the indefinite iteration $\pi^*$ should satify $R_{\pi^*}=R^*_{\pi}$. This poses a significant challenge for an interpretation of PDL through stochastic Kripke models, because the programs' operations do not always have a natural counterpart in the set of stochastic relations. Clearly, operations like $K_{\pi}\cup K_{\pi'}$ or $K^*_{\pi}$ hardly make sense for transition probabilities $K_{\pi}$ and $K_{\pi'}$. In addition, an interpretation of PDL observe usually some tacit assumptions on the "static" semantics like $\pi_1;(\pi_2\cup\pi_3) = \pi_1;\pi_2\cup \pi_1;\pi_3$.
We convert these rules into rewrite rules, which permits building up an interpretation of PDL through terms in an algebra which admits operators of infinite arity. It is shown that each program corresponds to an essentially unique irreducible tree, which in turn is assigned a natural transformation of a suitable functor, serving as the programm's interpretation. Some technical problems have to be overcome by the observation that the interpretation of the indefinite interpretation requires a base space which is closed under the well-known Souslin operation from set theory. This is in particular inconvenient when the state space is assumed to be Polish: these spaces are closed under this operation only if they are finite. Hence previous results on the coalgebraic interpretation of modal logics are difficult to apply. The paper discusses the expressivity of these models and relates properties like logical and behavioral equivalence or bisimilarity to the corresponding properties of a Kripke model for a closely related non-dynamic logic of the Hennessy-Milner type.

Research funded in part by Deutsche Forschungsgemeinschaft, grant DO 263/12-1, Koalgebraische Eigenschaften stochastischer Relationen

Jean Goubalt-Larrecq: Full Abstraction for Non-Deterministic and Probabilistic Extensions of PCF

We investigate the full abstraction question for extensions of PCF with non-deterministic and probabilistic choice. This is in line with G. Plotkin's seminal work on PCF (1977). In particular, the denotational semantics is a standard domain-theoretic one, living in the category of bc-domains, and using prevision monads for effects. As for PCF, full abstraction fails without any extensions. In addition to parallel-if, we now need an additional (may, must, or probabilistic) testing primitive inside the language. Moreover, we prefer to allow demonic choice to deadlock. This is work in progress: at the time I write this, I am confident that full abstraction is obtained with these extensions, provided non-determinism is angelic or demonic (erratic is plausible, but not confirmed), and with or without probabilistic choice. The purely probabilistic case (no non-determinism) seems out of reach: the need for parallel-if is already a form of demonic non-determinism. This is in contrast to Danos and Harmer's fully abstract game-theoretic semantics for pure probabilistic PCF (2000).

Peng He and Abbas Edalat: Continuity and Computability of Visual Hull from Imprecise Input

The visual hull of a polyhedral scene in R3 is the best 3D shape one can retrieve from its 2D silhouettes. It has great advantage in obstacle avoid- ance, robotic navigation, 3D model acquisition and human motion tracking. The visual hull is bounded by planes and quadratic surfaces. Classical visual hull methods fail to maintain the exactness and robustness when the input is imprecise.
In the solid domain of 3D objects in R3, geometric shapes with imprecision are well modelled and carefully studied. Each partial geometric object is defined by 2 disjoint open sets : interior and exterior. The interior (respectively, exterior) is an open set that contains all the points definitely known to be inside (respectively, outside) the object. Partial objects, ordered with subset inclusion, form a continuous Scott domain in which each object approximates the target object at a certain level of precision.
We study the visual hull in the solid domain which allows the notion of partial visual hull. It captures the imprecision in the input polyhedral scenes and outputs the exact information about what points are definitely inside/outside the visual hull. The partial visual hull algorithm maintains the same computational complexity as the classical method and generates a partial visual hull which converges to the classical visual hull as the input converges to an exact value. We show the Hausdorff and the Scott continuity of the domain-theoretic construction in the Solid domain of the projective 3 space P3 and use this to prove the computability of the classical visual hull.

Weng Kin Ho and Dongsheng Zhao: When exactly is Scott sober?

A topological space is sober if every nonempty irreducible closed set is the closure of a unique singleton set. Sobriety is precisely the topological property that allows one to recover completely a topological space from its frames of opens. Because every Hausdorff space is sober, sobriety is an overt, and hence unnamed notion. Even in non-Hausdorff settings, sober spaces abound. A well-known instance of sober space appears in domain theory: the Scott topology of a continuous dcpo is sober. The converse is false as is witnessed by three counterexamples: the first by P.T. Johnstone, the second by J. Isbell and the third by H. Kou. Since then, there has been limited progress in the quest for an order-theoretic characterisation of those dcpo's for which their Scott topology is sober. This paper provides one answer to this open problem.

Olaf Klinke, Achim Jung and M. Andrew Moshier: A bitopological point-free approach to compactification

We study structures called d-frames which were developed by the last two authors for a bitopological treatment of Stone duality. These structures consist of a pair of frames thought of as the opens of two topologies, together with two relations which serve as abstractions of disjointness and covering of the space. With these relations, the topological separation axioms regularity and normality have natural analogues in d-frames. We develop a bitopological point-free notion of complete regularity and characterise all compactifications of completely regular d-frames. Given that normality of topological spaces does not behave well with respect to products and subspaces, probably the most surprising result is this: The category of d-frames has a normal coreflection, and the Stone-Cech compactification factors through it. Moreover, any compactification can be obtained by first producing a regular normal d-frame and then applying the Stone-Cech compactification to it. Our bitopological compactification subsumes all classical compactifications of frames as well as Smyth's stable compactification.

Paul Blain Levy: Surjectivity in the Powerset Final Sequence

We write Ord for the ordered class of ordinals, regarded as a category.
Definition 1. Let $F$ be an endofunctor on a category $C$ with limits. The final sequence of $F$ is the unique functor from $Ord^{op}$ to $C$ such that
- for every ordinal $i$ we have $A_{i+1} = FA_{i}$
- for $j \le i$ we have $A_{j+1;i+1} = FA_{j;i}$
- for limit $i$ the cone $(A_i; (A{j,i})_{j
It is well known that if $A_{m,m+1}$ is an isomorphism then $(A_m,A^{-1}_{m,m+1})$ is a final $F$-coalgebra. We say that the sequence stabilizes at $m$, and write $p_i$ for the projection $A_{i;m}$.
Let us consider the $\kappa$-bounded powerset functor $P^{\kappa}$, where $\kappa$ is an infinite regular cardinal. The most interesting cases are $P^{\omega}$ and $P^{\omega_1}$ , the finite powerset and countable powerset functors respectively.
The final sequence of $P^{\kappa}$ (and of other functors) was studied in [Wor05]. It was shown that $A_{\kappa,\kappa+1}$ is an injection, and hence $A_{j,i}$ is an injection for all $j \ge\kappa$. Finally, since $P^{\kappa}$ preserves intersections, the sequence stabilizes at $\kappa+\omega$.
The map $A_{j,i}$ is not injective for $j < \kappa$, because the kernel of $p_j$ is the $j$th approximant to bisimilarity, see e.g. [Sta09].
But which connecting maps are surjective? [Wor05] answers this for $P^{\omega}$.
Theorem 1.
1. The final sequence for $P^{\omega}$ does not stabilize until $\omega+\omega$.
2. Each projection $p_{i}$, for $i <\omega$, is surjective.

However, the question for general $\kappa$ remained open. We report progress as follows.
Theorem 2. Let $\kappa$ be a regular infinite cardinal.
1. The final sequence for $P^{\kappa}$ does not stabilize until $\kappa+\omega$.
2. Suppose $\kappa > \omega_1$. Then the projection $p_i$ is surjective for all countable $i$.

This fully answers the surjectivity question for the countable powerset functor. In the case of $\kappa>\omega_1$ it remains open whether $p_i$ is surjective for all $i <\kappa$.

Acknowledgements I thank Jiri Adamek and Stefan Milius for discussions.

[Sta09] Sam Staton. Relating coalgebraic notions of bisimulation. In Proceedings, CALCO, volume 5728 of LNCS, 2009.
[Wor05] James Worrell. On the nal sequence of a nitary set functor. Theoretical Computer Science, 338(1-3):184-199, June 2005.

Supported by EPSRC Advanced Research Fellowship EP/E056091/1

Tadeusz Litak: Constructive Loeb logic: natural deduction, fixed points and proof terms

Several modal type systems and corresponding lambda calculi have been investigated in the literature. These include, in particular, so-called lax logic---which, as discussed by Benton, Bierman and de Paiva, is the Curry-Howard counterpart of Moggi's monadic language for computational effects---and constructive S4, whose associated proof-term calculus has been used by, e.g., Davies and Pfenning to give an account of staged computation. I am going to discuss the constructive variant of the Loeb logic, which can be obtained by adding to constructive K4 calculus the rule "from []p -> p, infer p", and some of its extensions, such as the one obtained by adding the axiom p->[]p. Such systems have made several appearances in type-theoretic literature, in particular in the work of Nakano ("A modality for recursion" and a subsequent TACS paper), in the work of Appel et al. ("A very modal model of a modern, major, general type system") and subsequent line of papers (e.g. Benton and Tabareau); also, in a still unpublished work, Conor McBride proposed a Loeb modality in the context of functional programming to ensure productivity of unbounded corecursion. However, to the best of my knowledge, not only is a clear-cut, definite account of the Curry-Howard correspondence for such system(s) still missing, but---more importantly---some of their most interesting properties known in the modal logic community are yet to be fully used in the type-theoretic context. The most important one I have in mind is the *unique fixed-point theorem*, proved by Giovanni Sambin in mid-1970's. It works in both constructive and classical setting and in the latter case, it has been used in a series of papers by Visser, Van Benthem and Alberucci and Facchini to show eliminability of fixed-point operators over the Loeb logic. I am not aware of similar applications of this theorem for constructive Loeb logic(s); in fact, some of above-mentioned type-theoretic papers, such as those by Nakano, did add *both* an explicit fixed-point operator and a Loeb modality to the type system. One of goals of my work is to investigate whether explicit fixed point operators can be eliminated also over intuitionistic base and, more generally, whether Sambin's celebrated result can throw some light on uses of Loeb-like modalities to reason about both inductive and coinductive properties of programs. Concerning the Curry-Howard correspondence for the constructive Loeb logic and its variants, one possible account of it can be given by taking a starting point a 1985 paper by Bellin on natural deduction for the classical version of the system; in fact, de Paiva and coauthors have already used this work for subsystems such as K and K4, although apparently not for the Loeb logic itself. Another variant currently being investigated is proof term assignment for a natural deduction system with *context stacks* analogous to those given for constructive S4 by Pfenning and Wong or Davies and Pfenning. Such systems tend to yield more tractable and elegant proof terms. Time and progress permitting, I am also going to report on ongoing work on semantics: either operational or denotational. The latter in turn could be formulated either in terms Kripke-style structures or cartesian closed categories (extended with a suitable endofunctor). Note that by Kripke-style semantics I mean semantics in the sense of a seminal Mitchell-Moggi paper, i.e., semantics for proof terms rather just for types (propositions). Ordinary Kripke completeness results for the constructive Loeb logic and its variants were obtained already by Ursini (in 1970's) and Iemhoff (in her PhD Thesis). To sum up, this is very much a work in progress, which can diverge in unexpected directions. I am certainly looking forward to suggestions, feedback and criticism---both constructive and classical.

Yanfang Ma, Yixiang Chen and Min Zhang: Topological Construction of Two-thirds Bisimulation

Abstract: In this paper, we focus on two-thirds bisimulation and the main aim is to describing the mechanism of convergence of implementation under two-thirds bisimulation. Furthermore, we propose the specification of a system can be seen as the limit of the implementation under two-thirds bisimulation. Firstly, two-thirds limit bisimulation and two-thirds bisimulation limit are defined. Some algebraic properties are proved. Secondly, several closure construction of two-thirds limit bisimulation are introduced, such as subnet closure, tail closure, natural extension and iteration. These closure constructions are useful for us to construct two-thirds bisimulation topology. Finally, two-thirds bisimulation limit is shown to form a convergence class, so they induce so-called two-thirds bisimulation topology.

Maria Emilia Maietti and Giuseppe Rosolini Quotients for Doctrines

We apply tools from categorical logic to give an abstract description of constructions used to give models of theories for constructive mathematics based on intensional type theory. We show that the key concept is that of an elementary doctrine in the sense of Lawvere and we describe a notion of quotient completion as a left biadjoint to a fairly natural forgetful 2-functor. Instances of that notion are the exact completion on a category with products and weak pullbacks as well as models of various extensional type theories.

Iosif Petrakis: Extending the basic Scott framework of information systems

We study the domain of ideals |A| of an information system A from the point of view of a regular and Hausdorff-extension N of the standard Scott topology S on |A|. N is defined through the notion of a space in a convergence form, and, as we found out, it is, in the general case of a directed complete poset, already known as the liminf topology. An N-open set can also be characterized by a strong form of the Scott condition. The study of N is also natural from an "approximation" point of view. Using the notion of an approximation structure of V. Stoltenberg-Hansen, we show that the compact ideals of A together with the Scott open sets form an Alexandrov pair of approximations for |A| (satisfying the Alexandrov and the Scott condition, therefore, the strong Scott condition), while the compact ideals of A together with the N-open sets form a Scott pair of approximations for |A| (satisfying the strong Scott condition, therefore, the Scott condition, but not the Alexandrov condition). The aim of our work is to study the degree to which we can extend the basic Scott framework of |A|, centered around the use of S on |A| and on the func- tion space of S-continuous functions, to a corresponding framework centered around N instead of S. Besides N extending S, we also prove that each Scott continuous function is also continuous with respect to N, while a function which is continuous with respect to N is continuous with respect to S iff it is monotone. Using a standard result on regular spaces we show that a function defined on the set of compact ideals satisfying a condition we call N-monotonicity, has a unique N-continuous extension to the set of all ideals. Also, each monotone function on the compact ideals of A is N -monotone. The exact structure of the set of all N-continuous functions with the pointwise order, is still under study.


The classification of cartesian closed categories is a classic theme in domain theory. One thinks of Smyth's theorem [Smy83] that the maximal cc full subcategory of the $\omega$-algebraic $\omega$-cpos with a least element is that of the bifinite $\omega$-cpos, and Jung's characterisation [Jun90] of the maximal cc full subcategory of the $\omega$-continuous $\omega$-cpos with a least element. The (algebraic) Scott domains [Sco82] are the consistently complete $\omega$-algebraic $\omega$-cpos. It is natural to ask which full subcategories of the category Dom of Scott domains (and $\omega$- continuous functions) are cartesian closed (equivalently, which are sub-cccs of Dom). Since one can make any full subcategory cartesian closed simply by closing it under products and function spaces, it is reasonable to restrict the question, and ask instead which full subcategories of Scott domains, additionally closed under retracts, are cartesian closed. This question has been attempted over the years without, however, complete success. Here we report on some recent progress. There are four obvious such categories of Dom: those which are complete lattices [Sco76], the coherent Scott domains [Plo78], and, respectively, their full subcategories of $\omega$-cpos with finitely many elements. The notion of coherence generalises: say that a Scott domain is n-coherent if, for any subset, whenever all its subsets of size n are consistent (i.e., have an upper bound) then so does that subset; the complete lattices are the cases n = 0 and n = 1, and the coherent domains are the case n = 2. The simplest example of a domain which is not n-coherent is the n + 1 dimensional hypercube oriented with least element the origin and with the maximal (= constantly 1) point removed. The full subcategory of n-coherent domains (and their full subcategories of domains with nitely many points) provide further examples of retract-closed cc full subcategories of Dom. However this does not exhaust all the possibilities as points can participate in truncated hypercubes of all dimensions. So we can classify points according to the pattern of their participation in truncated hypercubes and, in turn, other points participation in such participations, and so on. This leads to well-founded countably branching trees of points and so to countable ordinals, as we now make precise.
Definition 1. Let D be a Scott domain. A mic-tree in D is a tree $\tau$ , together with a map $l : \tau \to D^o$ where $D^o$ is the set of finite elements of $D$, such that for any branch $b$ of the tree, the set $l(b)\subseteq D^o$ is inconsistent iff the branch is nite and complete, and, further, such that $l$ is 1-1 on branches.
Here "mic" stands for "minimally inconsistent".
There is a standard assignment of ordinals to nodes in well-founded trees and then to well-founded trees. We assign ordinals $||n||$ to nodes $n$ of a non-empty well-founded countable tree $\tau$ by:
$||n|| = 0$ if $n$ is a leaf
$||n|| = sup{||n'|| + 1 | n' is a child of n} otherwise
The ordinal $||\tau||$ of such a tree $\tau$ is defined to be the ordinal of its root. The ordinals obtained in this way are exactly the countable ones. If $\tau\to D^o$ is a mic tree then $||\tau|| > 0$. Combining these ordinals with mic trees we can first define coherence degrees of domains and then of categories of domains. The coherence degree $coh(D)$ of a Scott domain $D$ is defined by:
$$coh(D) = sup{||\tau||+1 | there is a mic tree \tau\to D, with \tau well-founded and countable}$$
For example, the $n$-coherent domains are those with coherence degree $n$ (for $n \neq 1$).
Proposition 1.
Every Scott domain has coherence degree $\le\omega_1$, and there is a non-trivial Scott domain with every such ordinal (except for 1).
Proof. Given a non-empty well-founded countable tree $\tau$ with more than one node, set $D_\tau$ to be the collection of all subsets of $\tau$ not containing any complete branch. Then $coh(D_\tau) = ||\tau||$. The Scott universal domain has coherence degree $\omega_1$.
Next, the coherence degree $coh(C)$ of a full subcategory $C$ of Dom, the category of Scott domains, is defined by:
$$coh(C) = sup{coh(D) + 1|D \in Ob(C)}$$
We have $coh(C)\le\omega_1 + 1$, but not = 2. (The case $coh(C) = 0$ is when $C$ has no objects.)
Let $Dom_\kappa$ be the full subcategory of all domains with coherence degree $<\kappa$ (for $\tau\le\omega_1 + 1$, but not = 0, 2); it has coherence degree $\kappa$. Let $Dom^f_\kappa$ be the full subcategory of all domains with finitely many points with coherence degree $<\kappa$ (for $\tau\le\omega$, but not = 0, 2); it has coherence degree $\kappa$. We discuss the following conjecture:
Conjecture 1.
The categories $Dom_\kappa$ (for $\tau\le\omega_1 + 1$, but not = 0, 2) and $Dom^f_\kappa$ (for $\tau\le\omega$, but not = 0, 2) are the distinct non-trivial retract-closed sub-ccc's of Dom.
(The trivial ones are those with at most one object.)

[Jun90] Achim Jung, The Classification of Continuous Domains (Extended Abstract), Proc. 5th LICS, 35-40, 1990.
[Plo78] Gordon D. Plotkin, T^omega as a Universal Domain, J. Comput. Syst. Sci., 17(2), 209-236, 1978.
[Sco76] Dana S. Scott, Data Types as Lattices, SIAM J. Comput., 5(3), 522-587, 1976.
[Sco82] Dana S. Scott, Domains for Denotational Semantics, Proc. 9th ICALP, LNCS, 140, 577-613, 1982.
[Smy83] Michael B. Smyth, The Largest Cartesian Closed Category of Domains, Theor. Comput. Sci., 27, 109-119, 1983.

Uday S. Reddy and Brian Dunphy: States and actions: An automata-theoretic semantics for programming languages

The extant semantic models of programming languages fall into one of two major paradigms. In the Scott-Strachey paradigm or the extensional paradigm, computations are modelled as mathematical mappings from inputs to outputs. The success of the paradigm rests on its ability to hide the intermediate stages of computation. But it has a drawback in that the structure of data is exposed in inputs and outputs of computations. In sophisticated programs, the data structures carry considerable representational detail, which the programmers wish to abstract from. In the Milner-Hoare paradigm or the event-based paradigm, computations are thought of as agents whose behaviour is modelled in terms of streams of events observed on their external interfaces. Games semantics is the most successful embodiment of this paradigm. While the paradigm succeeds in hiding the representations of data structures, it makes the intermediate stages of computation visible. In an effort combine the advantages of both the paradigms, we investigate new models inspired by automata theory, where both states (data) and actions (events) are modelled, but states remain hidden as part of the internal structure of the automata and only actions participate in the observable behaviour. While we call these models ``new,'' they were already considered by Reynolds in 1981 in his seminal paper titled ``The Essence of Algol.'' However, Reynolds's approach remained unexplored in the following work, which reverted to a purely state-based extensional approach. In contrast, the ``object-based'' model of the first author and the games models developed along similar lines represent an event-based approach. Recent work in various areas of program reasoning, including the ``rely-guarantee'' reasoning used for concurrent programs, the ``deny-guarantee'' reasoning developed by Parkinson and colleagues, and the ``abstract state machine'' techniques developed Derek Dryer, Amal Ahmed and colleagues, call for a renewed attention to the automata-theoretic approach. As a first step towards developing a semantic foundation for such techniques, we define a semantic model of Idealized Algol using the automata-theoretic ideas and study its properties.

Sam Staton: Presenting partiality and non-determinism

This talk is about ways of presenting algebraic theories of partiality, nondeterminism, and their combination. There are three situations where these issues arise: firstly in the study of lifting and powerdomains in domain theory; secondly in Sangiorgi's axiomatizations of bisimilarity in the pi-calculus [3]; and thirdly in Freyd's topos-theoretic analysis of intuitionistic notions of finiteness [1]. As motivation, consider three monads on the category of sets: the finite powerset monad P, the finite-non-empty powerset monad P+, and the lifting monad L:
P(X) =def {S ⊆ X | S is finite}
P+(X) =def {S ⊆ X | S is finite but not empty}
L(X) =def X ∪ {*}.
We can understand these monads as arising from algebraic theories. Following Plotkin and Power [2] we can in turn understand the algebraic theories as theories of computational effects. The finite-non-empty powerset monad P+ captures the algebraic theory of semilattices; the binary semilattice operation can be understood as the effect of non-determinism. The lifting monad L captures the theory of pointed sets, i.e. the effect of partiality. The finite powerset monad P arises by combining these two theories in an appropriate way. In more general situations, the classical theory of pointed sets is not relevant; rather, the important universal property of L is that it classifies partial maps. The purpose of the talk is to discuss how partial map classifiers can be presented as (enriched) algebraic theories, so that we can combine the effects of partiality and non-determinism.

Some references
[1] P. Freyd. Numerology in topoi. Theory Appl. of Categ., 16(19):522-528, 2006.
[2] G. D. Plotkin and J. Power. Notions of computation determine monads. In Proc. FOSSACS'02, volume 2303 of Lecture Notes in Comput. Sci., pages 342-356, 2002.
[3] D. Sangiorgi. A theory of bisimulation for the pi-calculus. In Proc. CONCUR'93, volume 715 of Lecture Notes in Comput. Sci., pages 127-142, 1993.

Research partly supported by ERC grant Events, Causality and Symmetry.

Hugh Steele and Andrea Schalk: Double Glueing and MLL Full Completeness

Linear Logic (LL) is a deductive system that has garnered a considerable amount of attention over the past two decades. Its correspondence to a polymorphic lambda calculus has made it a topic of particular interest for theoretical computer scientists. The logic's original description takes the form of a sequent calculus, making it ungainly at times; but there has been success expressing the proof theory of LL and of its smaller logical fragments in other ways. Derivations can be described graphically (with propositional atoms and connectives being represented by vertices) or as arrows in an appropriate category. Naturally it is important for a category describing any logic to be as accurate a model as possible in order for it to be considered useful. Abramsky and Jagadeesan [AJ94] formalised this notion and gave it the name `full completeness': a categorical model of a logic is fully complete if all of its arrows correspond directly to a derivation. In this talk we demonstrate how it is possible to create fully complete models of MLL, the strongly normalising multiplicative fragment of LL, from certain compact closed categories. These models are non-trivial in the sense that distinct cut-free derivations are represented within them by di erent arrows. Our approach makes use of the Hyland-Tan `double glueing' construction, originally found in the thesis of Audrey Tan [Tan97]. Using the construction, Tan transforms the category of sets and binary relations (Rel) into a category GRel satisfying MLL full completeness. We extend this result to every tensor-generated compact closed category with biproducts. The new arguments which we employ to do this are based around considering the combinatorics behind the double glueing construction. We present how it is possible to express each graphical representation of a normalised derivation of MLL as a particular family of arrays over the set of scalars (that is, the homset [I; I] for tensor unit I) in any such compact closed category. With this more concrete structure we can use the \arithmetic" of double glueing to show that these are the only natural collections of arrays which describe arrows in the new glued categorical model. The arrays that are of interest to us can be viewed as certain symmetries, and so nally we discuss the possibility of a full completeness proof created from a purely geometric perspective.

[AJ94] S. Abramsky and R. Jagadeesan. Games and full completeness for multiplicative linear logic. J. Symbolic Logic, 59:543-574, 1994.
[Tan97] A.M. Tan. Full completeness for models of linear logic. PhD thesis, University of Cambridge, 1997.

Paul Taylor: Computability in locally compact spaces

Locally compact spaces may be characterised by giving a basis of open and compact subspace pairs together with the containment (cover or way below) relation between them. Continuous functions are then represented by "rounded lattice homomorphisms". This was shown in my paper "Computably based locally compact spaces" and also in independent work by Achim Jung and his collaborators. Whilst this is computable in principle, it is impractical because of the need to apply "rounding" operations and the use of nested lists.
I will show how to overcome these two problems, using bases with just intersections rather than unions too. The key idea is a weakening of the roundedness conditions.
These weaker conditions are satisfied by interval arithmetic and preserved by composition and lambda-abstraction. The outcome is that we may translate the ASD language for topology into familiar styles of logic, functional and interval programming. Moreover, lamdda-abstractions become closures in the usual way.

Pawel Waszkiewicz: Formal ball models of quasimetric spaces

I would like to present solutions to two open problems concerning formal ball models of quasi-metric spaces. I will show that (a) a quasi-metric space X is Yoneda complete i its formal ball model is a dcpo, and (b) a quasi-metric space X is continuous and Yoneda complete i its formal ball model BX is a domain that admits a simple characterisation of approximation. The results have been published in: M. Kostanek, P. Waszkiewicz. The formal ball model for Q-categories. Mathematical Structures in Computer Science 21(1) (2011), pp. 41-64.

Hengyang Wu and Yixiang Chen: The Partial Correctness Semantics of Fuzzy Imperative Programming Language

In this paper, we consider a fuzzy imperative programming language whose syntax is given (in BNF) by $$S::=\mbox{skip}|X:=FUZZ(X)|S_{1};S_{2}|S_{1}[] S_{2}|\mbox{if $b$ then $S_{1}$~else $S_{2}$}|\mbox{while $b$ do $S$}$$ where $X:=FUZZ(X)$ is a fuzzy assignment statement associating with a fuzzy relation $P$ and $b$ is a boolean condition, i.e., a mapping from the state space to $\{0,1\}$. The program $S_{1}[] S_{2}$ nondeterministically executes either $S_{1}$ or $S_{2}$, the rest are as usual. We study the axiomatic and the denotational semantics of this fuzzy imperative programming language in the framework of partial correctness logic. Based on Hoare triple, we prove the soundness and completeness theorems of this language. That is, a Hoare triple can be deduced from the axiomatic system if and only if it is valid. Moreover, we prove the duality between the denotational semantics and the weakest liberal precondition semantics.

Wei Yao and Bin Zhao: A duality between $\Omega$-categories and algebraic $\Omega$-categories

In this paper, we propose a definition of algebraic $\Omega$-categories. Let $\Omega$-{\bf POID} denote the category of $\Omega$-categories with $\Omega$-functors between them such that inverse image of ideals are ideals, $\Omega$-{\bf AlgDom}$_G$ denote the category of algebraic $\Omega$-categories with Scott continuous functors between them having left $\Omega$-adjoints. We show that $\Omega$-{\bf AlgDom}$_G$ and $\Omega$-{\bf POID} are dual equivalent to each other.
Last modified: Fri Sep 2 2011