The Coq mailing list

[Eddy Westbrook <westbrook AT galois.com>]

Hi Coq Club,

I was wondering if anyone could point me to some related work for some 
semantics work I am doing.

I am trying to build a denotational semantics using a category of 
representable functions, where a "representable function” is any function 
that is definable using a fixed set of function-building operations. These 
operations might include composition, the identity function, certain constant 
functions, etc.

In order to define recursion and fixed-points, I need to use a twist on the 
standard machinery of complete partial orders (CPOs), because not every 
ascending chain of representable functions is guaranteed to have a supremum 
that is itself representable. This can be shown by a cardinality argument, 
since we have only countably many representable functions but uncountably 
many ascending chains of functions in, say, the function space Nat -> _|_ + 
Unit.  (This co-domain is my ASCII way of writing the Sierpinski space.)

So, instead, my idea is that my domains only need to be complete for 
representable chains, that is, chains that can be constructed by repeated 
applications of representable functions. More specifically, my chains look 
like this:

proj init  <=  proj (f init)  <=  proj (f (f init)) <= …

for a given starting point init : A, a representable function f : A -> A, and 
a projection function proj : A -> B, such that the functions f and proj are 
both Scott-continuous (monotone and preserve suprema, when they exist), and 
such that init <= f init. I am calling this concept a “representably-complete 
partial order” because the partial order only has to be complete for 
representable chains.

My question is: does anybody know any work that is related to this? The idea 
of using representable functions is certainly not new, and has been used for 
decades (almost a century!) in computability theory. But I have not seen any 
work that talks about doing domain theory on representable functions, and 
would really appreciate any pointers into the literature on it.

Thanks Coq Club!
-Eddy