Thanks! Pottier again, he seems to pop up in every second related work 
However
we cannot do this using “off-the-shelf” techniques for solving recursive domain equations, like those of Rutten [12] or Birkedal et al. [13]. Instead, we obtain a solution by explicitly constructing the inverse limit of an appropriately chosen sequence of approximations …
doesn’t sound very encouraging, I fear (not that I fully understand that paper.)
From a rummage through my ol’ bookmarks file:
Encapsulating non-determinacy in an abstract data type with determinate semantics (1991).
Permission-Based Ownership: Encapsulating State in Higher-Order Typed Languages (2005).
Perhaps something in those could be useful…
@atraverse pointed me to Nielson: Strictness Analysis and Denotational Abstract Interpretation (1988).
Indeed they consider monotone functions. On page 64 in comparison with prior work they write
One small point is that we have only required functions to be monotonic whereas in Mycroft and Jones (1985) they are in fact assumed to be continuous. Nonetheless it is correct to claim that this demonstrates that the setup of Mycroft and Jones (1985) is expressible in the present framework
which I find a bit thin… ah, and later (p76) they write
On a more technical side the present development should be extended to allow recursive domains. Before this can be accomplished we must replace monotonic function space by continuous function space as otherwise recursive domain equations need not have solutions.
which kinda answers my question negatively, unfortunately 
(Maybe it somehow helps that rseq is always ⊥ for function values? So maybe we can restrict → to the space of “functions that are either continuous, or always bottom for function values”? But now I am just guessing…)
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
I made more progress on the Denotational Semantics, and was able to write something that seems to hold water. Some high-level observations:
Latest version at https://www.joachim-breitner.de/publications/rec-def-denotational.pdf
I’ll probably let it rest at that for now, as a first goal has been reached. Maybe after digesting any possible feedback at ICFP I’ll pick it up again.
A Scott-continuous function is always monotonic.
Are you using a different notion of continuity or a different notion of monotonicity?
No, same notion. Continuity implies monotonicity, but not the other way around, unfortunately.
An observation - Hackett and Hutton only use two terms in reference to their technique:
“clairvoyant evaluation” (first page, in the abstract)
“clairvoyant call-by-value” (second page, in the introduction)
…they never use the term/s “clairvoyant call-by-need/name”.
Have you (subtly) extended their approach in some way for your purposes here?
Nope, merely a mistake on my part :-). Should be “ clairvoyant call-by-value”. Thanks!
The semantics become non-continous, but monotone (and thus still a well-defined fixed-point of its equations).
Fixed-points might exist alright, but can you embed arbitrary monotone functions D ->m D into D? E.g., is fix : (D ->m D) -> D satisfying fix(f) = f(fix(f)) a monotone function and an element of (edit: perhaps the latter is not necessary)? (This is an identity that we use in the Lambda case of the semantics.) What is a model for DD?
Sorry to play the devil’s advocate here, but this seems a bit too good to be true. After all, why would Scott have to force continuity down our throats if monotonicity would have sufficed? (Note that continuity already is weaker than computability, so parity was never an issue.)
Edit: Ah, perhaps I should have given a closer look: You restrict yourself to simply-typed lambda calculus. So not Turing-complete, fair enough. On the other hand, your Let expressions are recursive, so it’s more like PCF, which is Turing-complete. And then you invite all the same trouble into your domain, because you have to prove that fix is a monotone function at every type, I think. Also you have to prove that monotone functions between DCPOs form a DCPO. I remain vary.
Yes, simple types are my way out. I do have recursive let, so I think it is turing complete. I think fix still exists.
I think it’s because he has recursive types (well, a single recursive uni-type).
I wouldn’t be surprised if I blundered somewhere, so please keep playing!
It just occurred to me that (in a sense) you’re trying to achieve some level of totality in the presence of recursion - from this SPLS Meeting in March 2012: