[Agda] Nice programming challenge

[Martin Escardo]

On 02/06/11 07:07, Andrea Vezzosi wrote:
> By the way, is there a standard generalization of the continuity axiom
> to more structures than streams, and that doesn't require the codomain
> to be discrete?

For simple types (closure of the natural number under finite products
and function spaces), you have the so-called Kleene--Kreisel
functionals, whose topology has been described in many equivalent ways
(see e.g. my paper "Exhaustible sets in higher-type computation"). But
this probably requires a lot of background.

Still for simple types, you can use Scott domains (see e.g. my paper
"Operational domain theory and topology of sequential programming
languages" for an account that doesn't require too much background but
that develops things in considerable depth). (There is also my paper
"Synthetic topology of program types and classical spaces", which
contains lots of references.)

I also recommend "Computing with functionals - computability theory or
computer science?" and the slides "50 years of continuous functionals"
by Dag Normann, although they are perhaps more advanced.

For dependent types, work has been done by a number of people. Perhaps
the most recent is that by Coquand and Spivack ("Proof of
normalization using domain theory").

All these references are on the web and easily obtainable with google,
and of course there are many more references regarding this.

Best wishes,
Martin