## Stream: Coq users

### Topic: ✔ Arbitrary function fixed points with Coinductive types

#### Lucas Silver (Oct 27 2021 at 14:09):

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?

#### Pierre-Marie Pédrot (Oct 27 2021 at 15:12):

The corecursive call is definitely not guarded, because `f` can do arbitrary things to it.

#### Pierre-Marie Pédrot (Oct 27 2021 at 15:13):

Imagine for instance if `f` is a function that peels a `Tau` node of its argument, you'd get a loop.

#### Pierre-Marie Pédrot (Oct 27 2021 at 15:14):

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

#### Pierre-Marie Pédrot (Oct 27 2021 at 15:14):

Namely, the type of `f ` must reflect the fact it does not do anything to its argument apart from passing it around.

#### Lucas Silver (Oct 27 2021 at 16:19):

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

#### Pierre-Marie Pédrot (Oct 27 2021 at 16:22):

You can follow the Paco approach.

#### Karl Palmskog (Oct 27 2021 at 16:25):

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

#### Pierre-Marie Pédrot (Oct 27 2021 at 16:29):

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

#### Lucas Silver (Oct 27 2021 at 16:37):

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

#### Li-yao (Oct 27 2021 at 16:48):

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

#### Lucas Silver (Oct 27 2021 at 17:03):

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).
*)
``````

#### Li-yao (Oct 27 2021 at 17:25):

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.

#### Notification Bot (Oct 28 2021 at 05:05):

Ayush Jaiswal has marked this topic as resolved.

Last updated: Oct 05 2023 at 02:01 UTC