Thanks! That paper “Call-by-need is clairvoyant call-by-value” is super helpful, maybe Clairvoyant Call by Need indeed solves my problems.
@Lysxia, you formalized Clairvoyant Call by Need in Coq… what do you think? (Based on your paper you did not consider non-structurally-recursive definitions, so probably no knot-tying in your formalization, right?)
The paper doesn’t give the denotational semantics for the language extended with data types, but I can guess what it would look like:
- adding a (simple)
S xconstructor to the syntax, - changing the value domain to
V ≅ (V_⊥ → D) + Dto (which I’ll write asS das well) - Adding the equation equation
[[ S x ]]ϱ = 0 ▹ S (ϱ)
Now the denotation of
let x = S x in x
seems to be, if my scribblings are correct, 2 ▹ (µ x. C (0 ▹ x)), while for
let x = λ y. S (x y) in x e
(for arbitrary e) I get 6 ▹ (µ x. C (4 ▹ x)) (the cost counters may be off a bit).
So if “cost zero” means “ value is shared”, then indeed this denotational semantics allows me to distinguish knot-tying vs. untied knots!
(And probably I can simplify by only keeping track of 0 vs. not-0 in the semantics.)
What I am unsure now: Can I introduce an operation rseq x that is () if x evaluates to a cyclic data structure, and ⊥ else? It seems that “evaluates to a cyclic data structure” means “can be evaluated to a (infinite) tree of constructor applications where the overall cost is finite” or equivalently “all but finitely many costs are 0”. I can certainly define an operation D → D that way, but I worry: is it continuous?
It seems not. In this particular partial order we have
(µ x. C (1 ▹ x))
⊏ C (0 ▹ (µ x. C (1 ▹ x)))
⊏ C (0 ▹ C (0 ▹ (µ x. C (1 ▹ x))))
…
⊏ (µ x. C (0 ▹ x))
but rseq (µ x. C (1 ▹ x)) = ⊥ and C (0 ▹ (µ x. C (1 ▹ x))) = ⊥ and also (µ x. C (0 ▹ x)) = (). This is monotonic, but not continuous.
So we cannot “simply” add this operation to the language. Too bad.
