Confluence
Closed this issue · 8 comments
so I read a little more about confluence (a.k.a. the church-rosser property) over the weekend and I think we don't actually have it for our calculus. you need a "strong calculus" which means reduction under binders to get confluence. see the non-commuting diagram on page 3 of this paper for example: http://gallium.inria.fr/~maranget/papers/jwk60.pdf.
So either we need to add a rule for stepping under binders, which can take a slightly weaker form (see linked paper) where you maybe only need to step closed sub-terms under binders (i.e. those that do not depend on the bound variable), or we need to just be satisfied with just the commutativity theorem from the notes, without the resumption theorem.
OK -- I don't really know much about it one way or the other, and certainly haven't spent any meaningful amount of time thinking about how to prove this yet, so I'm happy to take your word for it.
Do you have a counter example that you can think of to make this more concrete? Do you have a preference about changing the rules to step under binders vs being happy with just commutativity?
Counterexample:
(\x.\y.x) (2 + 2) ---> (\x.\y.x) 4 ---> \y.4
and also
(\x.\y.x) (2 + 2) --> (\y.2 + 2)
but (\y.2 + 2) does not step to (\y.4).
I think the "right" solution to this conundrum is to use the approach from the paper I linked (and the paper it references as prior work), but I don't know that there is enough time right now to work that out so for now I think let's just satisfy ourselves with the Commutativity theorem and then briefly discuss the implications for resumption in the paper.
Oh, yeah, I see. Is this one of the consequences of non-determinism? Like if we had the bracketed premises would this hold?
If you had the bracketed premises then you'd have confluence trivially because stepping is deterministic, but you'd lose commutativity.
So should I remove the stubs from confluence from this repo? That would also mean removing final-confluence. Anything else?