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 x`

constructor to the syntax,
- changing the value domain to
` V ≅ (V_⊥ → D) + D`

to (which I’ll write as `S d`

as 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.