Basic properties of rewrite relations

We define the basic properties of rewrite relations (commutation, confluence, normalization, as well as various variants of these). Additionally, we prove various theorems that relate these properties to one another.

@[reducible, inline]

abbrev Thesis.weakly_commutes {α : Type u_1} (r s : Rel α α) : Prop

Two relations r and s commute weakly if any one-step reducts b (via r) and c (via s) of a have a common reduct d.

Equations

• Thesis.weakly_commutes r s = ∀ ⦃a b c : α⦄, r a b ∧ s a c → ∃ (d : α), s∗ b d ∧ r∗ c d

@[reducible, inline]

abbrev Thesis.commutes {α : Type u_1} (r s : Rel α α) : Prop

Two relations r and s commute if any reducts b (via r) and c (via s) of a have a common reduct d.

Equations

• Thesis.commutes r s = ∀ ⦃a b c : α⦄, r∗ a b ∧ s∗ a c → ∃ (d : α), s∗ b d ∧ r∗ c d

@[reducible, inline]

abbrev Thesis.subcommutative {α : Type u_1} (r : Rel α α) : Prop

A relation r is subcommutative if any one-step reducts b and c of a have a common reduct d, which may be equal to b or c.

Equations

• Thesis.subcommutative r = ∀ ⦃a b c : α⦄, r a b ∧ r a c → ∃ (d : α), r⁼ b d ∧ r⁼ c d

@[reducible, inline]

abbrev Thesis.confluent {α : Type u_1} (r : Rel α α) : Prop

A relation r is confluent if any reducts b and c of a have a common reduct d.

Equations

• Thesis.confluent r = ∀ ⦃a b c : α⦄, r∗ a b ∧ r∗ a c → ∃ (d : α), r∗ b d ∧ r∗ c d

@[reducible, inline]

abbrev Thesis.confluent' {α : Type u_1} (r : Rel α α) (a : α) : Prop

Confluence for a specific element a: α (see confluent).

Equations

• Thesis.confluent' r a = ∀ ⦃b c : α⦄, r∗ a b ∧ r∗ a c → ∃ (d : α), r∗ b d ∧ r∗ c d

@[reducible, inline]

abbrev Thesis.weakly_confluent {α : Type u_1} (r : Rel α α) : Prop

A relation r is weakly confluent (or locally confluent) if any one-step reducts b and c of a have a common reduct d.

Equations

• Thesis.weakly_confluent r = ∀ ⦃a b c : α⦄, r a b ∧ r a c → ∃ (d : α), r∗ b d ∧ r∗ c d

@[reducible, inline]

abbrev Thesis.diamond_property {α : Type u_1} (r : Rel α α) : Prop

The diamond property holds if any one-step reducts b and c of a have a common one-step reduct d.

Equations

• Thesis.diamond_property r = ∀ ⦃a b c : α⦄, r a b ∧ r a c → ∃ (d : α), r b d ∧ r c d

@[reducible, inline]

abbrev Thesis.triangle_property {α : Type u_1} (r : Rel α α) : Prop

The triangle property holds if every element a has a two-step reduct a' which can be reached via all one-step reducts b.

Equations

• Thesis.triangle_property r = ∀ (a : α), ∃ (a' : α), ∀ (b : α), r a b → r b a'

theorem Thesis.confluent_iff_star_weakly_confluent {α : Type u_1} (r : Rel α α) : Thesis.confluent r ↔ Thesis.weakly_confluent r∗

theorem Thesis.confluent_iff_star_self_commutes {α : Type u_1} (r : Rel α α) : Thesis.confluent r ↔ Thesis.commutes r∗ r∗

theorem Thesis.confluent_iff_star_dp {α : Type u_1} (r : Rel α α) : Thesis.confluent r ↔ Thesis.diamond_property r∗

def Thesis.semi_confluent {α : Type u_1} (r : Rel α α) : Prop

A relation r is semi-confluent if r∗ a b and r a c imply the existence of a d such that r∗ b d and r∗ c d. This differs from confluence in that c must be a one-step reduct of a.

semi_confluent is equivalent to confluent (see semi_confluent_iff_confluent) but is sometimes easier to prove as you can simply use induction on the length of r∗ a b.

Equations

• Thesis.semi_confluent r = ∀ ⦃a b c : α⦄, r∗ a b ∧ r a c → ∃ (d : α), r∗ b d ∧ r∗ c d

theorem Thesis.semi_confluent_iff_confluent {α : Type u_1} {r : Rel α α} : Thesis.semi_confluent r ↔ Thesis.confluent r

Semi-confluence is equivalent to confluence.

def Thesis.conv_confluent {α : Type u_1} (r : Rel α α) : Prop

A relation is conversion confluent if r≡ a b implies the existence of a c such that r∗ a c and r∗ b c. It is equivalent to confluence (see conv_confluent_iff_confluent).

This is also called the Church-Rosser property -- since Terese identifies confluence and the Church-Rosser property, we use the novel name conversion confluence here.

Equations

• Thesis.conv_confluent r = ∀ ⦃a b : α⦄, r≡ a b → ∃ (c : α), r∗ a c ∧ r∗ b c

theorem Thesis.conv_confluent_iff_confluent {α : Type u_1} {r : Rel α α} : Thesis.conv_confluent r ↔ Thesis.confluent r

Conversion confluence is equivalent to confluence.

theorem Thesis.confluent_of_diamond_property {α : Type u_1} (r : Rel α α) : Thesis.diamond_property r → Thesis.confluent r

The diamond property implies confluence.

def Thesis.strongly_confluent {α : Type u_1} (r : Rel α α) : Prop

Strong confluence, as defined by Huet (1980).

Strong confluence implies confluence, see confluent_of_strongly_confluent.

Equations

• Thesis.strongly_confluent r = ∀ ⦃a b c : α⦄, r a b ∧ r a c → ∃ (d : α), r⁼ b d ∧ r∗ c d

theorem Thesis.confluent_of_strongly_confluent {α : Type u_1} (r : Rel α α) : Thesis.strongly_confluent r → Thesis.confluent r

Any relation that is strongly confluent is confluent.

@[reducible, inline]

abbrev Thesis.normal_form {α : Type u_1} (r : Rel α α) (a : α) : Prop

An element a is a normal form in r if there are no b s.t. r a b.

Equations

• Thesis.normal_form r a = ¬∃ (b : α), r a b

@[reducible, inline]

abbrev Thesis.weakly_normalizing' {α : Type u_1} (r : Rel α α) (a : α) : Prop

Equations

• Thesis.weakly_normalizing' r a = ∃ (b : α), Thesis.normal_form r b ∧ r∗ a b

@[reducible, inline]

abbrev Thesis.weakly_normalizing {α : Type u_1} (r : Rel α α) : Prop

A relation is weakly normalizing if all elements can reduce to a normal form.

Equations

• Thesis.weakly_normalizing r = ∀ (a : α), ∃ (b : α), Thesis.normal_form r b ∧ r∗ a b

@[reducible, inline]

abbrev Thesis.strongly_normalizing' {α : Type u_1} (r : Rel α α) (a : α) : Prop

Equations

• Thesis.strongly_normalizing' r a = ¬∃ (f : ℕ → α), f 0 = a ∧ Thesis.reduction_seq r ⊤ f

@[reducible, inline]

abbrev Thesis.strongly_normalizing {α : Type u_1} (r : Rel α α) : Prop

A relation is strongly normalizing if it admits no infinite reduction sequences.

Equations

• Thesis.strongly_normalizing r = ¬∃ (f : ℕ → α), Thesis.reduction_seq r ⊤ f

def Thesis.normal_form_property {α : Type u_1} (r : Rel α α) : Prop

A relation has the normal form property if a reduces to b if b is a normal form and a ≡ b.

Equations

• Thesis.normal_form_property r = ∀ (a b : α), Thesis.normal_form r b → r≡ a b → r∗ a b

def Thesis.unique_normal_form_property {α : Type u_1} (r : Rel α α) : Prop

A relation has the unique normal form property if all equivalent normal forms a and b are equal.

Equations

• Thesis.unique_normal_form_property r = ∀ (a b : α), Thesis.normal_form r a ∧ Thesis.normal_form r b → r≡ a b → a = b

def Thesis.unique_nf_prop_r {α : Type u_1} (r : Rel α α) : Prop

A relation has the unique normal form property with respect to reduction if all normal forms with a common expansion are equal.

Equations

• Thesis.unique_nf_prop_r r = ∀ (a b c : α), Thesis.normal_form r a ∧ Thesis.normal_form r b → r∗ c a ∧ r∗ c b → a = b

def Thesis.complete {α : Type u_1} (r : Rel α α) : Prop

A relation is complete if it is confluent and strongly normalizing.

Equations

• Thesis.complete r = (Thesis.confluent r ∧ Thesis.strongly_normalizing r)

def Thesis.semi_complete {α : Type u_1} (r : Rel α α) : Prop

A relation is semi-complete if it has the unique normal form property and it is weakly normalizing.

Equations

• Thesis.semi_complete r = (Thesis.unique_normal_form_property r ∧ Thesis.weakly_normalizing r)

def Thesis.rel_inductive {α : Type u_1} (r : Rel α α) : Prop

A relation is inductive if, for every reduction sequence, there exists an element a that is a reduct of every element in the sequence.

Since inductive is a Lean keyword, we use the name rel_inductive.

Equations

• Thesis.rel_inductive r = ∀ {N : ℕ∞} {f : ℕ → α} (hseq : Thesis.reduction_seq r N f), ∃ (a : α), ∀ b ∈ hseq.elems, r∗ b a

def Thesis.increasing {α : Type u_1} (r : Rel α α) : Prop

A relation is increasing if there exists a mapping f: α → ℕ which increases with a reduction step.

Equations

• Thesis.increasing r = ∃ (f : α → ℕ), ∀ {a b : α}, r a b → f a < f b

theorem Thesis.increasing_trans_of_increasing {α : Type u_1} {r : Rel α α} : Thesis.increasing r → Thesis.increasing r⁺

If r is increasing, so is its transitive closure r⁺.

def Thesis.finitely_branching {α : Type u_1} (r : Rel α α) : Prop

A relation is finitely branching if every element has only finitely many one-step reducts.

Equations

• Thesis.finitely_branching r = ∀ (a : α), ∃ (s : Finset α), ∀ (b : α), r a b → b ∈ s

def Thesis.acyclic {α : Type u_1} (r : Rel α α) : Prop

A relation is acyclic if no element a is a reduct of itself.

Equations

• Thesis.acyclic r = ∀ (a b : α), r⁺ a b → a ≠ b

theorem Thesis.sn_of_wf_inv {α : Type u_1} (r : Rel α α) : WellFounded r.inv → Thesis.strongly_normalizing r

If r⁻¹ is well-founded, then r is strongly normalizing.

theorem Thesis.wf_inv_of_sn {α : Type u_1} (r : Rel α α) : Thesis.strongly_normalizing r → WellFounded r.inv

If r is strongly normalizing, then r⁻¹ is well-founded.

Take the contrapositive, i.e. ¬WF → ¬SN. Assume r is not well-founded. Then it has an inaccessible element. Any inaccessible element must have a descendent which is inaccessible. This leads to an infinite sequence of inaccessible elements. Hence, r cannot be strongly normalizing.

theorem Thesis.sn_iff_wf_inv {α : Type u_1} (r : Rel α α) : WellFounded r.inv ↔ Thesis.strongly_normalizing r

If a relation is strongly normalizing, its inverse is well-founded, and vice versa.

theorem Thesis.wn_of_sn {α : Type u_1} {r : Rel α α} : Thesis.strongly_normalizing r → Thesis.weakly_normalizing r

Strong normalization implies weak normalization.

theorem Thesis.rel_inductive_of_semi_complete {α : Type u_1} (r : Rel α α) : Thesis.semi_complete r → Thesis.rel_inductive r

Any semi-complete relation r is inductive.

theorem Thesis.nf_of_confluent {α : Type u_1} (r : Rel α α) : Thesis.confluent r → Thesis.normal_form_property r

Any confluent relation r has the normal form property.

theorem Thesis.unf_of_nf {α : Type u_1} (r : Rel α α) : Thesis.normal_form_property r → Thesis.unique_normal_form_property r

Any relation with the normal form property has the unique normal form property.

theorem Thesis.confluent_of_semi_complete {α : Type u_1} (r : Rel α α) : Thesis.semi_complete r → Thesis.confluent r

Any semi-complete relation is confluent.

theorem Thesis.strongly_normalizing_of_inductive_of_increasing {α : Type u_1} (r : Rel α α) : Thesis.rel_inductive r → Thesis.increasing r → Thesis.strongly_normalizing r

Any inductive and increasing relation is strongly normalizing.

theorem Thesis.confluent_of_subcommutative {α : Type u_1} (r : Rel α α) : Thesis.subcommutative r → Thesis.confluent r

Any subcommutative relation is confluent.

theorem Thesis.strongly_normalizing_of_normal_form {α : Type u_1} (r : Rel α α) {a : α} (hnf : Thesis.normal_form r a) : Thesis.strongly_normalizing' r a

A normal form is always strongly normalizing.