The Coq mailing list

[Gregory Malecha <gmalecha AT gmail.com>]

Hi, Eddy --

I'm just getting to reading all the responses to my (quite popular) thread. I would be interested in your monad transformer if you'd be willing to send it to me. I assume that I'll know once you send it, do you have reasoning principles for the monad? In particular, I've been struggling with generic logics over monads and monad transformers and the non-termination monad is one of those monads.

Thanks so much.

On Thu, Dec 10, 2015 at 8:21 AM, Eddy Westbrook <westbrook AT kestrel.edu> wrote:

Hi Greg,

I have actually thought a lot recently about modeling non-terminating systems, and have mostly come to a similar conclusion as you, that (nat-> A) equivalent to (Stream A), and that the former does not require co-inductive types (which I don't like for a number of theoretical and practical reasons).

Adam has actually defined a non-termination monad based upon this idea, which you can find if you google for "non-termination monad" (or you can probably just ask him). If you are interested, I was also working on a non-termination monad transformer a few months ago, that adds a similar notion of non-termination to any monad, and I can send it to you if you are interested.

-Eddy

Sent from my iPhone

On Dec 7, 2015, at 11:06 AM, Gregory Malecha <gmalecha AT gmail.com> wrote:

Thanks, Pierre-Marie --

At the moment I just prove that this are [Proper], which isn't really too big of a problem since you can define combinators that handle the properness proofs for the most part. I guess I'm wondering more from a model point of view, are there any corner cases that one definition covers that the other does not?

If the co-inductive lists could also be finite, i.e. with this definition

CoInductive ftrace (st : Type) : Type :=

| Cons : st -> ftrace st -> ftrace st

| Done.

Then with functions you need to add some notion of "equal up to the occurrence of 'Done'" which is a bit cumbersome to express. But it seems that for truly infinite, non-dependent structures you might always be able to play this trick of "functions from paths to values". Is that the case, or is there a reason to prefer the CoInductive definition?

On Mon, Dec 7, 2015 at 10:48 AM, Pierre-Marie Pédrot <pierre-marie.pedrot AT inria.fr> wrote:

On 07/12/2015 19:11, Gregory Malecha wrote:
> To reason about the first I use co-induction and I do not need
> functional extensionality.

You'll actually need some form of extensionality to use it with ease.
Indeed, you cannot disprove the following in Coq, and it's pretty useful
in practical use:

CoInductive trace (state : Type) : Type :=
| Cons : state -> trace state -> trace state.

CoInductive bisimilar {state} : trace state -> trace state -> Prop :=
| Bisimilar : forall s t1 t2, bisimilar t1 t2 -> bisimilar (Cons _ s t1)
(Cons _ s t2).

Axiom trace_extensionality : forall state (t1 t2 : trace state),
bisimilar t1 t2 -> t1 = t2.

If you don't assume it, you'll have to show that all of your predicates
are Proper (and they meta-are), just like for the functional case.

PMP

--

gregory malecha

--

gregory malecha