# Zulip Chat Archive

## Stream: general

### Topic: relation.church_rosser

#### Yaël Dillies (Aug 17 2021 at 07:24):

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 (Aug 17 2021 at 07:29):

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 (Aug 17 2021 at 07:50):

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

#### Yaël Dillies (Aug 17 2021 at 07:51):

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

#### Mario Carneiro (Aug 17 2021 at 07:52):

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

#### Yaël Dillies (Aug 17 2021 at 07:53):

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 (Aug 17 2021 at 07:55):

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 (Aug 17 2021 at 07:57):

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 (Aug 17 2021 at 07:58):

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 (Aug 17 2021 at 08:02):

```
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 (Aug 17 2021 at 08:03):

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

#### Mario Carneiro (Aug 17 2021 at 16:29):

@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 (Aug 17 2021 at 16:30):

Oh yeah, what's `acc`

actually?

#### Mario Carneiro (Aug 17 2021 at 16:31):

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

#### Mario Carneiro (Aug 17 2021 at 16:31):

#### Mario Carneiro (Aug 17 2021 at 16:32):

it's the basic building block for defining well foundedness

#### Mario Carneiro (Aug 17 2021 at 16:32):

in maths we would read `acc (<) a`

as "there is no infinite sequence `a > a1 > a2 > ...`

"

#### Mario Carneiro (Aug 17 2021 at 16:35):

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

#### Yaël Dillies (Aug 20 2021 at 09:19):

Ahah! So `relation.church_rosser`

is the proof that semi-confluent implies the Church Rosser property.

#### Yaël Dillies (Aug 20 2021 at 09:28):

Wait, no. It's not semi-confluence... The `refl_gen`

`refl_trans_gen`

is on the wrong side of the implication.

Last updated: Dec 20 2023 at 11:08 UTC