I have written an implementation of the `Delay`

monad which coinductively represents possibly divergent computation.

I want to, if possible, implement a function that works like `fix`

in a typed lambda calculus where `fix f --> f (fix f)`

, adding in `Tau`

constructors to help represent divergent computations.

The following code was my attempt to implement this operator, however, the final function does not satisfy Coq's well-formedness checker.

```
Variant DelayF (D R : Type) : Type :=
| RetF (r : R)
| TauF (d : D).
CoInductive Delay (R : Type) : Type :=
go { _observe : DelayF (Delay R) R }.
Arguments TauF {D R}.
Arguments RetF {D R}.
Arguments go {R}.
Notation Delay' R := (DelayF (Delay R) R).
Notation Tau d := {| _observe := TauF d |}.
Notation Ret r := {| _observe := RetF r |}.
CoFixpoint spin {R} : Delay R := Tau spin.
Fail CoFixpoint delay_fix {R : Type} (f : Delay R -> Delay R) : Delay R :=
Tau (f (delay_fix f) ).
```

The definitions of `delay_fix`

fails because Coq says `f (delayed_fix f)`

is not in guarded form. However, I believed it was in guarded form because it is under the `Tau`

constructor.

Can someone help me understand precisely what is going wrong, and, if possible, help me understand if this is something fundamental or just a quirk of Coq that can be circumvented?

The corecursive call is definitely not guarded, because `f`

can do arbitrary things to it.

Imagine for instance if `f`

is a function that peels a `Tau`

node of its argument, you'd get a loop.

In order to do what you want, you need a more semantical criterion à la Löb rule

Namely, the type of `f `

must reflect the fact it does not do anything to its argument apart from passing it around.

Ok, I think I understand why it rejected my program. As a follow up questions, I know Coq has support for well founded induction, does it have support for some kind of semantic criterion for cofixpoints? I've never come accross that before

You can follow the Paco approach.

I think there are three principal coinductive automation projects these days:

- Paco
- Lukasz Czajka's Coinduction plugin
- Damien Pous' Coinduction library

You can also encode the ALMIGHTY TOPOS OF TREES by hand, i.e. a glorified fuel trick.

Thanks for the pointers, everyone. I'm already familiar with Paco so I will see if I can use that to get the result that I am looking for

You could also consider the recursion combinators in itree as ways of working around those limitations surrounding delay_fix. You can define iter for the delay monad, while mrec requires the free monad structure, but that could be the price to pay for expressing higher-order recursive computations, and once you handle all of the effects you are back to the delay monad (cf. McBride's "Turing Completeness Totally Free")

Hey Li-yao , I actually tried an `mrec`

based approach already. It led me to the following definition

```
Polymorphic Variant callInitE (A B : Type) : Type -> Type :=
| Call : A -> callInitE A B B
| CallInit : callInitE A B B.
Polymorphic Definition mrec_itree_fix {E R} (k : R -> itree E R) : itree E R :=
mrec
(fun (T : Type) (call : callInitE R R T) =>
interp inr_
match call in (callInitE _ _ T0) return (itree E T0) with
| Call _ _ r => k r
| CallInit _ _ => ITree.spin
end)
(CallInit R R).
```

Where `Call a`

represents a recursive call that returned a value `a`

and `CallInit`

represents an ill-founded recursive call and is what is used to initialize the `mrec`

.

This looked like it could be the solution, however, it leads to universe inconsistency issues. That can be seen in this attempt to define `fact`

.

```
Polymorphic Definition fact_itree_fix_body' {E} (rec : nat -> itree E nat) : itree E (nat -> itree E nat) :=
Ret (fun n => if Nat.eqb n 0 then Ret 1 else m <- rec (n - 1);; Ret (n * m) ).
Fail Definition fact_itree {E} (n : nat) : itree E nat :=
fact <- @mrec_itree_fix E (nat -> itree E nat) fact_itree_fix_body';;
fact n.
(*
The command has indeed failed with message:
In environment
E : Type -> Type
n : nat
The term "nat -> itree E nat" has type
"Type@{max(Set,ITree.Core.ITreeDefinition.2,ITree.Core.ITreeDefinition.3,itreeF.u1+1)}"
while it is expected to have type "Type@{ITreeFix.129}" (universe inconsistency: Cannot enforce
itreeF.u1 < ITreeFix.129 because ITreeFix.129 <= pweqeq.u3 = itreeF.u1).
*)
```

One limitation is that an event in an itree can't return an itree, so `callInitE (nat -> itree E nat)`

leads to problems.

But recursive function bodies `(nat -> nat) -> (nat -> nat)`

are often better represented as `nat -> itree (callE nat nat) nat`

, turning the recursive call into an event.

Ayush Jaiswal has marked this topic as resolved.

Last updated: Jun 23 2024 at 01:02 UTC