If we allow monotone, but non-continuous functions in the semantics, we have to re-interpret the domain equation

Do you intend to provide `rseq`

as a “primop”? Then you really need it to be continuous, yes.

But above you were implying that you only want to use it in first-order settings, e.g., to evaluate the heap.

If you never need to pass it as an argument to a function (or let-bind it), it doesn’t need to be embeddable into `D`

.

I think under that circumstances your are fine with saying "`rseq`

is just a monotone function from `D`

to `D`

", if that is enough for you to chew on.

Edit: Well, the problem is probably that you want to define `rseq`

as the greatest fixed-point of an equation in `D`

, which amounts to defining `gfp : (D -> D) -> D`

on monotone functions. Then indeed I have no idea how you get by without continuity (even with continuity I’d be curios how you would define `gfp`

).

Edit2: Actually you only need `gfp : ((D ->m D) ->m (D ->m D)) -> D ->m D`

. maybe that helps? I don’t even think that you would need to say how to construct `gfp`

, you can perhaps just show that it exists. And it should exist by Knaster-Tarski as the lub of all expansive points (monotone functions) of the functional.

Maybe that is enough to “compute”.

Otherwise I’d simply go with guarded domain theory (I would have even done that to start with, but I’m biased), where you don’t have to worry about continuity and strange approximation orders.

Indeed, Birkedal and Schwinghammer are co-authors of that 2010 article, after which they went on to focus their research on guarded recursive types.

I think you might get a reasonable model of Clairvoyance by factoring apart the non-determinism (finite subset lattices should be possible to do in a guarded setting) and the “minimum number of steps” thing.

Happy to collaborate in about 2 weeks of time