Given two values of a coinductive type, is it possible to have a function determining whether they represent they are equal?
Like Stream
from https://coq.inria.fr/stdlib/Coq.Lists.Streams.html.
Is a function like
Definition strm_eq {A:Type} (a b:Stream A) : bool := ..
possible?
No. From strm_eq
, you can solve the halting problem. The idea is that for each Turing machine with each input, there's a stream representing its trace. You can then do some transformations on this trace so that the machine (not) halting is equivalent to the stream being all 0s.
The closest you could do, assuming decidable equality on A
, is basically semi-deciding if they are different via a function in the delay monad, i.e. of type: Definition strm_eq (a b : Stream A) : Delay bool.
. Fixing A
to nat, something of this style:
From Coq Require Import Arith.
Set Primitive Projections.
CoInductive stream := cons { hd: nat; tl: stream }.
Variant step (R : Type) := | Error | Next (r : R).
CoInductive delay := go { next: step delay }.
Notation different := (go (@Error delay)).
Notation "'wait' x" := (go (@Next delay x)) (at level 20).
Definition str_eq : stream -> stream -> delay :=
cofix F (s t : stream) : delay :=
if hd s =? hd t
then wait (F (tl s) (tl t))
else different.
Thanks!
Julin S has marked this topic as resolved.
Last updated: Sep 26 2023 at 11:01 UTC