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:

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

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