Stream: wg-traits

Topic: coinduction bug


nikomatsakis (May 06 2019 at 19:55, on Zulip):

So I think the bug would actually show up in this situation:

// Send is coinductive:
Send(X) :- Foo(X), Bar(X).
Foo(X) :- Send(X)
nikomatsakis (May 06 2019 at 19:55, on Zulip):

If we were (say) solving Send(u32), then we would go to solve Foo(u32) and conclude that -- since Send(u32) is on the stack -- Foo(u32) is true.

nikomatsakis (May 06 2019 at 19:55, on Zulip):

But, in fact, we will later disprove Send(u32)

nikomatsakis (May 06 2019 at 19:56, on Zulip):

If we used a delayed literal instead, then the result of Foo(u32) would be Send(u32) | (i.e., with a delay), and we would ultimately reject it as false.

nikomatsakis (May 06 2019 at 20:55, on Zulip):

So one thing i'm wondering here though -- can we solve this by always selecting "inductive" goals first?

nikomatsakis (May 06 2019 at 20:55, on Zulip):

I think I had convinced myself we cannot but now .. I'm wondering why

nikomatsakis (May 06 2019 at 20:56, on Zulip):

ah, well, of course

nikomatsakis (May 06 2019 at 20:57, on Zulip):

all the predicates could be coinductive

Last update: Nov 12 2019 at 16:55UTC