The Coq mailing list

[Max New <maxsnew AT gmail.com>]

The concept your looking describing looks very close to "rationality": closure not under arbitrary omega-chains, but only those obtained by iterating some morphism.

I think the concept was introduced in Abramsky, Jagadeesan and Malacaria "Full Abstraction for PCF" available very post-dated on the arxiv: https://arxiv.org/abs/1311.6125

McCusker's thesis "Games and Full Abstraction for a Functional Metalanguage with Recursive Types" has a chapter laying out the theory of "rational categories" if you can get your hands on it

-Max Stewart New

On Mon, May 7, 2018 at 8:57 PM, Eddy Westbrook <westbrook AT galois.com> wrote:

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