DOMAIN on Sunday

Detailed program
Sunday July 21st, 2002
See also the unified by-slot program


All sessions take place in auditorium 3.

Session 5

09:00-10:00  Bill Lawvere, State U of New York-Buffalo, USA
Invited talk: Some open problems concerning cartesian closed categories
Dana Scott showed in 1970 that there are many cartesian closed categories containing arbitrarily large objects which are isomorphic to their own self-exponential. Tarski's high school identities suggest a more general question:
(1) Which exponential rigs can be objectively realized?
Hurewicz's homotopy category is also cartesian-closed, but has the unusual property that its points functor is the left adjoint of its own left adjoint.
(2) Can any CCC be mapped to one with that property?
That property also applies to infinitesimals which moreover enjoy further right adjoints, so that functionals (such as differential forms) are actually functions with a bigger codomain.
(3) Can the lambda-calculus be expanded so as to provide an efficient means of presenting CCC's with such additional right adjoints?
A topos has exponential types as a consequence of the power types. The power types also permit, via Dedekind's infinite intersection method, the construction of a "natural" number object given only the geometrical phenomenon of a monomorphic endo-map which is not an isomorphism.
(4) Are exponential types really qualitatively tamer than the power types?
For example, could a CCC generated by an 0-minimal model still avoid bad infinity?

10:00-10:30  Benjamín René Callejas Bedregal, Federal U of Rio Grande do Norte, Brazil
Roberto Callejas-Bedregal, Federal U of Paraíba, Brazil
biScott domain as a Cartesian closed category
In this work we use an interval constructor on posets which when applied to a poset D gives a new poset whose elements are intervals of D. We study this interval constructor from a categorical viewpoint: we verify some domain categories which are closed under this constructor. We also use this constructor in order to generalize some usual notions of the Moore interval theory, such as the interval extension of a continuous real function. The category of biScott domain as object and bicontinuous functions as morphisms is introduced in order to, provide a category of domain closed under the interval constructor. We will show the constructors to the categorical cartesian product and to the categorical function space. Finally, we will show that it category of domain is cartesian closed.

Session 6

11:00-11:30  Benjamín René Callejas Bedregal, Federal U of Rio Grande do Norte, Brazil
An information systems representation to SFP and retract of SFP domains
In this paper we exhibit a representation for ω-continuous cpo's, ω-algebraic cpo's, SFP domains and retracts of SFP domains, with the intention of keeping as close as posible the spirit of Scott's original construction of information systems and, in this way, to provide a more concrete and logical account of theses domains. In this sense, we introduce the notion of pre-information system and Plotkin information system, which are simples generalizations of Scott Information Systems [Sco82b], and we show their equivalence (categorical) with ω-algebraic cpo and SFP domains. Analogously, we show that pre-continuous information system represent adequately ω-continuous cpo's and a subclass of them, constructed from Plotkin Information systems, corresponding to retract of SFP domains.

11:30-12:00  Ho Weng Kin, National Inst. of Education, Singapore
Zhao Dongsheng, National Inst. of Education, Singapore
On characterization of Scott closed set lattices
It is well known that a dcpo P is a continuous poset if and only if the Scott topoly σ(P) is a completely distributive lattice with respect to the inclusion relation ⊆. The later is also equivalent to that the set C(P) of all Scott closed subsets sets of P is a completely distributive lattice. However, it is still not clear what are the order characterizations of C(P) for noncontinuous P. For instance, how to characterize the lattice C(A) for complete lattice A?
The main results in our work include:
(1) A complete lattice L is isomorphic to the Scott closed set lattice C(K) for an upper-bound complete dcpo if and only if P is weak algebraically smooth.
(2) A complete lattice L is isomorphic to the Scott closed set lattice C(A) for a complete lattice A if and only if L is algebraically smooth.
(3) The assignment to every dcpo P the lattice C(P) can be extend into an adjunction between the category DCPO of all dcpos and the category CLAT of all complete lattices and mappings which are left adjoints and preserve the new defined auxiliary relation <s.
(4) We introduced the pre-sober spaces and show that not every Scott space is pre-sober. However, for each complete lattice L, the Scott space Σ must be pre-sober.

12:00-12:30  Paula Severi, U Turin, Italy
Fer-Jan de Vries, U Leicester, UK
A lambda calculus for D
We define an extension of lambda calculus which is fully abstract for Scott's D-models. We do so by constructing an infinitary lambda calculus which not only has the confluence property, but also is normalising: every term has its ∞η-Böhm tree as unique normal form.
The extension incorporates a strengthened form of η-reduction besides infinite terms, infinite reductions and a bottom rule allowing to replace terms without head normal form by bottom. The new η!-reduction is the key idea of this paper. It allows us to capture in a compact and natural way Barendregt's complex ∞η-operation on Böhm trees.
As a corollary we obtain a new congruence proof for Böhm tree equivalence modulo infinite η-expansion.

Session 7

14:00-15:00  Gordon Plotkin, U Edinburgh, UK
Invited talk: Algebraic aspects of domain theory
The subject of domain theory, invented by Dana Scott, is a rich one, whose structure intertwines order theory, algebra, topology and computability. One approach is to take the ordered part as fundamental, building the rest in an order-theoretic context. Taking this point of view we explore the algebraic aspects of domain theory. These are both finitary and infinitary. On the former side one considers such conditions as bounded sups or meets, or characterisations of constructions, e.g., viewing powerdomains as various kinds of free semilattices; on the other side the definition of ω-complete partial orders is algebraic, but infinitary.
We have an enriched notion of algebra in view here, where order is taken as given and more than ordinary equational logic is needed. We develop and illustrate an appropriate logic, building on Power's work on enriched Lawvere theories and monads. This works well for enrichment relative to partial orders. For enrichment relative to ω-complete cpos, the theory also applies, but in a more complex manner. However it does not apply to enrichment relative to directed complete partial orders, which are however the more appropriate from a topological point of view. thereby illustrating a certain clash between the two domain-theoretic aspects of algebra and topology.

15:00-15:30  Guo-Qiang Zhang, Case Western Reserve U, USA
Ying Jiang, Chinese Academy of Sciences, China
Yixiang Chen, Shanghai Normal U, China
Stable bifinite domains: the finite antichain condition
In [1], Amadio and Curien raised the question of whether the category of stable bifinite domains is the largest cartesian closed full sub-category of the category of ω-algebraic meet-cpos with stable functions. This paper provides a progress report on our understanding of the situation, in part using a characterization of traces developed for this purpose. This characterization states that a set of compact-element pairs is the trace of a stable function if and only if it is joinable. The joinability condition offers intuition as well as another possible way for the creation of stable functions, a step lying at the heart of maximality proofs. We show that for an ω-algebraic meet-cpo D, if the higher-order stable function space [DD]→[DD] is 2/3 SFP, then D must be finitary. This is a crucial step forward in settling Amadio and Curien's question.

Session 8

16:00-17:00  Glynn Winskel, U Cambridge, UK
Invited talk: Domain theory for concurrency
Classical domain theory and denotational semantics, pioneered by Dana Scott and Christopher Strachey, has been inspirational in suggesting programming languages, their types and ways to understand them. Domain theory has played a much lesser role in research in interactive/concurrent/distributed computation. One reason perhaps is that classical domain theory has not scaled up to the more intricate models we find used in concurrency. In this talk I will describe what I see as the aims, challenges and promising approaches to a domain theory for concurrency.