I presume this is the paper you’re referring to:
and one I had forgotten about - it appeared in a search while looking for ways to solve another problem.
Regarding rseq: how would it have worked if it was applied (indirectly) to itself? It seems to vaguely resemble a termination checker…
Vaguely, and that is surely related to the troubles we are having.
But in the operational setting with an explicit heap we can see that it detects finite graphs (and doesn’t terminate for infinite graphs), which is fine. If it is used recursively, it’ll just diverge.
But the denotational setting doesn’t quite work. Maybe because the finite graph is infinitely unrolled, and recognizing that some infinite tree came from a finite graph is now indeed too close to a termination checker, and that’s why it doesn’t work yet?
Several years ago, I noticed this small article:
While the notation is more “machine-like”, perhaps the technique described could be useful for more precisely specifying which graphs are suitable for the intended purpose.
Actually, someone just pointed out to me that I was too pessimistic: If some function in the semantic domain isnt continuous, but still monotonic, that’s still a well-defined semantics! Just not so computable any more, but that might be ok. (Monotonic functions on CPOs have least fixed points, but if the function isn’t continuous, the fixed-point may not simply be the limit of fⁿ(⊥).
So maybe I am on the right track. Will be thinking more about this.
What is the definition of rseq? You give examples, but no closed definition. Perhaps it is
rseq = λd. if d = μ x. C (0 ▹ x) then C (0 ▹ ()) else ⊥
But that lacks detection of “finitely many non-0s”.
Is that continuous? I don’t think it is, but I didn’t really see a proof above.
Here is one: rseq (C (0 ▹^n ⊥)) = ⊥, so rseq (Lub_n {C (0 ▹^n ⊥)}) = rseq (μ x. C (0 ▹ x)) = () /= ⊥ = Lub_n {rseq (C (0 ▹^n ⊥))}.
But if it isn’t continuous, I’m a bit doubtful it is of use.
Since you are calling rseq on something involving a least fixed-point, at some point you want to do fixed-point induction. Then you are out of luck, because it is unlikely that a predicate involving rseq is admissable (which is continuity on D -> Prop).
Of course, you might always have concrete examples in mind where you can unroll the fixed-point once to see that the “remainder” it is something like μ x. C (0 ▹ x) and then you can apply rseq.
A closed definition is somewhat tricky to write down precisely, because rseq has to look at the whole expression. In prose, the definition is
rseq d
= () if d consists only of (possibly inifintely many) applications of C
and only finitely many cost annotaitons are not 0
= ⊥ else
It is monotonic, but not continuous. I think the counter example you give to the one here, with a sequence of values where rset is bottom on all these elements, but () in the limit.
But if it isn’t continuous, I’m a bit doubtful it is of use.
That’s what I thought, but Peter Thiemann pointed out that all you lose is that the least fixed point can no longer be found as the ω-limit of the iterating from bottom, but it still exists (as per some variant of Knaster–Tarski).
And you are right: one loses loses the simple fixed-point iteration as a proof principle. (Quick counter example: ∀ d, rseq d = ⊥ should hold according to that proof principle, based on our examples, but of course it doesn’t.) Maybe there is an analogue proof principle based on transfinite induction. I’ll start worrying about proofs once I wrote down the semantics 
(I have some promising ideas and might write them down today.)
How about this definition: rseq is the largest element of D →D such that
rseq (C (c ▹ x)) = c ▹ rseq x
rseq ⊥ = ⊥, else
and also
rseq d ⊑ 0 ▹ ()
holds. Note that here c₁ ▹ c₂ ▹ = (c₁ + c₂) ▹ …, so this accumulates the costs, so one gets rseq d = n ▹ () if the costs add up to n, but rseq d = ⊥ otherwise. The last equation ensures that we don’t get a value other than () in the success case.
That we are using a largest fixed-point here looks rather promising, this does have a coinductive feel to it after all.
I started a document at https://www.joachim-breitner.de/publications/rec-def-denotational.pdf. Right now it mostly contains how I can put RB.get into a denotational semantics (Treat RS.mk, RS.and etc. as normal constructors, and then solve the infinite formula in RS.get in one go).
The rseq discussion seems to be rather orthogonal actually, although I need both in the end to model the behavior of rec-def.
How about this definition:
rseqis the largest element ofD →Dsuch that
Yes, that seems plausible. One could view evaluating the heap as a coinductive process in which you yield back the cost of the evaluated heap bindings one after another.
On the other hand, rseq (µ x. C (1 ▹ x)) = (µ x. C (1 ▹ x)), so that is different to what you had before (although I’m quite faint on how (µ x. C (1 ▹ x)) is actually represented in the domain), but in a good way: I think the resulting definition is continuous:
rseq (Lub_n {C (c ▹^n ⊥)})
= rseq (μ x. C (c ▹ x))
= (μ x. C (c ▹ x))
= Lub_n {C (c ▹^n ⊥)}
= Lub_n {rseq (C (c ▹^n ⊥))}
So if that definition of rseq works for you, it is likely easier to handle.
I don’t think that’s correct. By the above equations we have
rseq (µ x. C (1 ▹ x))
= rseq (C (1 ▹ (µ x. C (1 ▹ x)))
= rseq (1 ▹ (µ x. C (1 ▹ x)))
= 1 ▹ rseq (µ x. C (1 ▹ x))
(where I’m a bit liberal with applying rseq to either D = (ω^{op} × V)_⊥ or V, see Section 5 of the Clairvoyant paper for details on the semantic domain).
But the equation d = 1 ▹ d only has one solution in this domain, namely d = ⊥, so we get
rseq (µ x. C (1 ▹ x)) = ⊥
as desired!
Just for comparison, for the tied knot (µ x. C (0 ▹ x)) I have
rseq (µ x. C (0 ▹ x))
= rseq (C (0 ▹ (µ x. C (0 ▹ x)))
= rseq (0 ▹ (µ x. C (0 ▹ x)))
= 0 ▹ rseq (µ x. C (0 ▹ x))
= rseq (µ x. C (0 ▹ x))
and the equation d = d has many solutions, but the largest in the range of rseq (which is restricted to {d ∈ D; d ⊑ ⊑ 0 ▹ ()}) is indeed (), as desired.
Ah, re-reading what ▹ does (it is not the lifted pair constructor but an operation that adds the LHS to the cost of the RHS) and realising that C denotes a constructor value, that makes a lot more sense.
But then I’m a bit confused about the meaning of rseq (C (c ▹ x)) = c ▹ rseq C x.
Would you say that rseq (c, C d) = c ▹ rseq d is an accurate clarification?
Then the interesting things look like μ d. (c, C d) and under rseq that is only () for 0, as you say.
Sorry, that was a typo, should have been rseq (C (c ▹ x)) = c ▹ rseq x, as you say. My bad.
There might be another technical problem. If we allow monotone, but non-continuous functions in the semantics, we have to re-interpret the domain equation
D = (D → D)_⊥
(here for just lambda calculus, no cost accounting) because now D → D need to not only hold continuous functions, but any monotonic function.
This raises the question: Do recursive domain equations involving the space of monotonic function still have solutions?
I’m a bit worried that texts like, for example, “THE CATEGORY-THEORETIC SOLUTION OF
RECURSIVE DOMAIN EQUATIONS” by Smyth and Plotkin does not list “DCPOs with monotonic functions” as an example of categories where such domain equations can be solved. Let’s escalate to stack exchange.
A search with solutions recursive domain equation space "monotonic functions" found this article:
Note: the detailed description/example of the technique makes use of an imperative language (albeit one which is deliberately minimal) - you’ll need to determine its suitability for a large non-strict language like Haskell.
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?