Normal forms for relations

This file develops basic normal form notions for abstract reduction relations.

We represent finite reduction sequences by Relation.ReflTransGen r. The assumption WellFounded (flip r) expresses termination of forward reductions.

The main results are:

• existence of normal forms for terminating relations;
• Newman's lemma: for a terminating relation, local confluence implies confluence;
• for terminating relations, confluence is equivalent to uniqueness of normal forms.

def Relation.IsNormalForm {α : Type u_1} (r : α → α → Prop) (a : α) : Prop

An element is in normal form if it admits no one-step reduction.

Equations

• Relation.IsNormalForm r a = ∀ (b : α), ¬r a b

def Relation.IsNormalFormOf {α : Type u_1} (r : α → α → Prop) (a b : α) : Prop

An element b is a normal form of a with respect to r.

Equations

• Relation.IsNormalFormOf r a b = (Relation.ReflTransGen r a b ∧ Relation.IsNormalForm r b)

def Relation.UniqueNormalForms {α : Type u_1} (r : α → α → Prop) : Prop

A relation has unique normal forms if any two normal forms reachable from the same element by finite reductions are equal.

Equations

• Relation.UniqueNormalForms r = ∀ {a b c : α}, Relation.ReflTransGen r a b → Relation.ReflTransGen r a c → Relation.IsNormalForm r b → Relation.IsNormalForm r c → b = c

def Relation.LocallyConfluent {α : Type u_1} (r : α → α → Prop) : Prop

A relation is locally confluent if any two one-step reductions starting from the same element can be joined by finite reductions.

Equations

• Relation.LocallyConfluent r = ∀ {a b c : α}, r a b → r a c → Relation.Join (Relation.ReflTransGen r) b c

theorem Relation.exists_normalFormOf_of_wellFounded_flip {α : Type u_1} {r : α → α → Prop} (hrwf : WellFounded (flip r)) (a : α) : ∃ (b : α), IsNormalFormOf r a b

If forward reductions are terminating, then every element has at least one normal form.

theorem Relation.ReflTransGen.eq_of_isNormalForm {α : Type u_1} {r : α → α → Prop} {a b : α} (hnf : IsNormalForm r a) (h : ReflTransGen r a b) : b = a

If a is in normal form and a reduces finitely to b, then b = a.

theorem Relation.Confluent.locallyConfluent {α : Type u_1} {r : α → α → Prop} (hc : Confluent r) : LocallyConfluent r

Confluence implies local confluence.

theorem Relation.locallyConfluent_of_confluent {α : Type u_1} {r : α → α → Prop} (hc : Confluent r) : LocallyConfluent r

Confluence implies local confluence.

theorem Relation.ChurchRosser.locallyConfluent {α : Type u_1} {r : α → α → Prop} (hcr : ChurchRosser r) : LocallyConfluent r

The Church-Rosser property implies local confluence.

theorem Relation.confluent_of_wellFounded_flip_of_locallyConfluent {α : Type u_1} {r : α → α → Prop} (hwf : WellFounded (flip r)) (hlc : LocallyConfluent r) : Confluent r

Newman's lemma, main direction. If flip r is well-founded and r is locally confluent, then r is confluent.

theorem Relation.Confluent.uniqueNormalForms {α : Type u_1} {r : α → α → Prop} (hc : Confluent r) : UniqueNormalForms r

Confluence implies unique normal forms.

theorem Relation.uniqueNormalForms_of_confluent {α : Type u_1} {r : α → α → Prop} (hc : Confluent r) : UniqueNormalForms r

Confluence implies unique normal forms.

theorem Relation.confluent_of_wellFounded_flip_of_uniqueNormalForms {α : Type u_1} {r : α → α → Prop} (hwf : WellFounded (flip r)) (hunf : UniqueNormalForms r) : Confluent r

Under well-foundedness of flip r, unique normal forms imply confluence.