Inductive Definitions over Domain Representable Spaces

Petter Kristian Kober

(Oslo, visiting Swansea)

We study strictly positive inductive definitions over a class of topological
spaces with admissible domain representation, the qcb0 spaces. In
particular, we prove that if A and B are qcb0 spaces, then there exists a
minimal qcb0 space X which satisfies the equation X = A + [B => X].
This least fixed point is obtained via a similar construction over a certain
class of domains with partial equivalence relations, using standard domain
representations of A and B. In fact, a least fixed point exists for every
strictly positive operator.
We also look at how further generalisations, e.g. admitting generalised
positive induction or free algebra constructions in the defining equation,
tend to somewhat complicate the situation.

Thursday 29th May 2008, 14:00
Robert Recorde Room
Department of Computer Science