relation.church_rosser

Stream: general

[Yaël Dillies]

How is that lemma known in real life?

lemma church_rosser
  (h : ∀ a b c, r a b → r a c → ∃ d, refl_gen r b d ∧ refl_trans_gen r c d)
  (hab : refl_trans_gen r a b) (hac : refl_trans_gen r a c) : join (refl_trans_gen r) b c :=

I looked around and, up to my humble knowledge, it's not the Church-Rosser theorem, because it doesn't talk about β-reduction. Is it a generalization of the fact that weak Church-Rosser implies strong Church-Rosser? Also, can it not be generalized to the following?

lemma stronger_church_rosser
  (h : ∀ a b c, r a b → r a c → join (refl_trans_gen r) b c)
  (hab : refl_trans_gen r a b) (hac : refl_trans_gen r a c) : join (refl_trans_gen r) b c :=

[Kyle Miller]

It has something to do with the Church-Rosser property for abstract rewrite systems, though the particular form of it is puzzling. Your stronger version is that "locally confluent implies confluent" I think.

[Yaël Dillies]

Yeah that's what I thought. Should I generalize it and then call that "locally confluent implies confluent"?

[Yaël Dillies]

Well, I won't change the lemma name, but I will add a docstring.

[Mario Carneiro]

Is the stronger form true? I think https://en.wikipedia.org/wiki/Confluence_(abstract_rewriting) has a counterexample

[Yaël Dillies]

Ahah! Interesting. And there's no way to get to Newman's lemma? How do we formalise this "no infinite reduction path" condition?

[Mario Carneiro]

that sounds like some inductive condition, for example an element is strongly normalizing if all elements it reduces to are strongly normalizing

[Yaël Dillies]

where strongly normalizing means that it's not related to anything on the right (normalizing) and that every it's transitivitely related to on the left is only transitively related to things it's transitively related to on the right (strongly)?

[Yaël Dillies]

My idea to define this condition is to have a "quantified" reflexive transitive closure which takes in a natural as one more argument.

[Yaël Dillies]

inductive quantified_refl_trans_gen (r : α → α → Prop) (a : α) : α → ℕ → Prop
| refl : refl_trans_gen a 0
| tail {n b c} : refl_trans_gen b n → r b c → refl_trans_gen c (n + 1)

def no_infinite_reduction_path (r : α → α → Prop) : Prop :=
∀ a b, refl_trans_gen r a b → ∃ N, ∀ n, quantified_refl_trans_gen r a b n → n ≤ N

[Yaël Dillies]

This natural is concretely measuring the length of the path so far.

[Mario Carneiro]

@Yaël Dillies Your relation is satisfied by the b = a + 1 relation on nat, so it's not right. I mean exactly what I said above:

inductive strongly_normalizing (r : α → α → Prop) : α → Prop
| mk (a) : (∀ b, r a b → strongly_normalizing b) → strongly_normalizing a

The term "strongly normalizing" is usually used to mean there are no infinite reduction paths starting at this element. It's basically the same as acc (flip r) as you can see, and the definition you have (with no element, just talking about the relation as a whole) is equivalent to well_founded (flip r).

[Yaël Dillies]

Oh yeah, what's acc actually?

[Mario Carneiro]

it stands for "accessible", and it's literally the definition I wrote with r flipped

[Mario Carneiro]

docs#acc

[Mario Carneiro]

it's the basic building block for defining well foundedness

[Mario Carneiro]

in maths we would read acc (<) a as "there is no infinite sequence a > a1 > a2 > ..."

[Mario Carneiro]

see docs#rel_embedding.well_founded_iff_no_descending_seq for the proof of equivalence of these two statements

[Yaël Dillies]

Ahah! So relation.church_rosser is the proof that semi-confluent implies the Church Rosser property.

[Yaël Dillies]

Wait, no. It's not semi-confluence... The refl_gen refl_trans_gen is on the wrong side of the implication.