 # ICFP Pearl on rec-def

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.

1 Like

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ⁿ(⊥).

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: `rseq` is the largest element of `D →D` such 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  or Birkedal et al. . 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:

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…)

1 Like

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 2 Likes

I made more progress on the Denotational Semantics, and was able to write something that seems to hold water. Some high-level observations:

• The semantics become non-continous, but monotone (and thus still a well-defined fixed-point of its equations).
• I can do call-by-name style semantics and still get a correct, but not adequate semantics (it is non-bottom in cases where the real program is). This can still be useful.
• I can do a call-by-need style semantics based on Clairvoyant call-by-value It’s not very pretty, but seems to work.
• The semantics are less abstract than one would hope (semantic equality does not include some contextual equivalences we would like to have).

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.

2 Likes

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.

1 Like

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?