 | |
All
sessions take place in auditorium 3.| 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. |
| 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. |
| 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 [D→D]→[D→D] is 2/3
SFP,
then D must be finitary. This is a crucial
step forward in settling Amadio and Curien's question. |
| 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. |
| |
![[previous]](../img/prev.gif){kind=small}
![[up]](../img/up.gif){kind=small}
![[next]](../img/next.gif){kind=small}
