Ist die Gleichheit bei jedem Koinzidenztyp entscheidbar?

Question

Dies ist mein erster Beitrag, Entschuldigung, wenn ich Fehler gemacht habe.

Ich vermute, dass in Coq coinductive Typen wie Stream keine entscheidbare Gleichheit haben. Das heißt, bei zwei Strömen s und t ist es nicht möglich zu identifizieren, ob s = t oder ~ (s = t). Ich vermute, dass dies für alle koinduktiven Typen in Coq gilt.

Eine schnelle Google und Suche durch Stapelwechsel zeigt keine Bestätigung. Kann mir das bestätigen oder korrigieren?

Answer 1

Ich denke, du hast Recht. Nach meinem besten Wissen kann man nicht einmal richtig angeben, was es bedeutet, dass zwei Ströme gleich sind, da es impliziert, dass man sie in endlicher Zeit untersuchen kann, aber sie sind unendliche Terme.

Was Sie tun können, ist der Zustand, dass jede endliche Inspektion Ihrer Co-induktiven Bedingungen gleich ist, oder einen „Co-induktiven“ Begriff der Gleichheit definieren, ähnlich wie es in der Standardbibliothek durchgeführt wird:

https://coq.inria.fr/library/Coq.Lists.Streams.html