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
I think under that circumstances your are fine with saying "
rseq is just a monotone function from
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
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