Confluent, Church-Rosser, diamond, etc. for relations

Stream: Is there code for X?

[Iván Renison]

Hi, I wanted to ask if there are definitions for when a relation is confluent, Church-Rosser, has the diamond property, and similar properties of relations?
I have seen that some theorems, for example Relation.church_rosser, use this concepts, but they have inline the definition, so I guess that maybe they are not defined anywhere

[Snir Broshi]

Might be useful:

• Diamond in CSLib
• CSLib proof of Church-Rosser for SKI calculus
• https://github.com/Danelnov/Lambda-Calculus-Formalization

[Iván Renison]

Ah, so it is in CSLib, that's why I didn't find it

[Iván Renison]

Thank you

[Iván Renison]

Do you know why is this in CSLib instead of Mathlib? Considering that some lemmas in Mathlib (like Relation.church_rosser) are essentially using them, it is surprising for me that it is not in Mathlib

[Chris Henson]

I initially added those (IIRC very early before it was even part of CSLib), simply because Mathlib didn't have them. If people agree they belong upstream, I'm happy to make a PR.

[Kevin Buzzard]

Iván Renison said:

Do you know why is this in CSLib instead of Mathlib?

Because this stuff is not really taught in mathematics departments but is bread and butter in theoretical computer science?

[Snir Broshi]

Iván Renison said:

Do you know why is this in CSLib instead of Mathlib? Considering that some lemmas in Mathlib (like Relation.church_rosser) are essentially using them, it is surprising for me that it is not in Mathlib

I think you should be asking the opposite question; why is Relation.church_rosser in Mathlib and not CSLib? CSLib didn't exist 7 years ago. Though docs#FreeGroup.Red.church_rosser makes the cs/math boundary here a bit blurry

[Kevin Buzzard]

Yes, this kind of stuff feels more on the boundary (because whilst mathematicians tend not to talk about SKI stuff they certainly talk about free groups).

[Chris Henson]

Yes, there are grey areas. Sometimes we prove small lemmas in CSLib that we then upstream to Mathlib. Others things like automata exist already in Mathlib, but are being extended further in CSLib. There have been discussions previously on this, but the library is new and there is no rush to move things. If maintainers feel anything should move up/downstream, please always feel free to reach out!

[Iván Renison]

Okay, I understand

[Iván Renison]

I have another question: Are there definitions for normal forms and normalizing relations? (for an arbitrary relation)

[Chris Henson]

I don't believe so, and this would be a welcome contribution to CSLib. Any particular reference you're working from?

[Snir Broshi]

(FWIW I really like this reference - https://www.youtube.com/playlist?list=PLNwzBl6BGLwOKBFVbvp-GFjAA_ESZ--q4)

[Chris Henson]

Snir Broshi said:

(FWIW I really like this reference - https://www.youtube.com/playlist?list=PLNwzBl6BGLwOKBFVbvp-GFjAA_ESZ--q4)

This seems to be particular to lambda calculi?

[Iván Renison]

Chris Henson said:

Any particular reference you're working from?

With my professor @Miguel Pagano we are exploring if it is feasible to formalize an alternative proof of the Fundamental Theorem of Arithmetic.
The idea is for each n ∈ ℕ to represent it as an infinite list with finte support, f : ℕ →₀ ℕ, where f represents ∑ i ∈ f.support, i ^ (f i). Over that representation the idea is to define a relation that reduces the representation to a representation where the support is only prime numbers, and show that this relation is confluent and the normal forms are the prime factorizations.
This is what I have so far (I only started today, so I'm figuring out things):

import Mathlib
import Cslib

structure NatRep where
  f : ℕ →₀ ℕ
  h₀ : f 0 = 0
  h₁ : f 1 = 0

def NatRep.toNat (r : NatRep) : ℕ :=
  ∑ i ∈ r.f.support, i ^ (r.f i)

def NatRep.Red (a b : NatRep) : Prop :=
  ∃ i j k : ℕ,
    i = j * k ∧
    a.f i > 0 ∧
    b.f j = a.f j + 1 ∧
    b.f k = a.f k + 1 ∧
    b.f i = a.f i - 1 ∧
    ∀l : ℕ, l ≠ i → l ≠ j → l ≠ k → a.f l = b.f l

def NatRep.RedStar : NatRep → NatRep → Prop :=
  Relation.ReflTransGen NatRep.Red

lemma NatRep.RedStar.Confluence : Cslib.Confluence NatRep.RedStar := sorry

[Snir Broshi]

Chris Henson said:

This seems to be particular to lambda calculi?

Yes but they define {confluence, normal forms, weakly normalizing, strongly normalizing} in general

[Snir Broshi]

Iván Renison said:

This is what I have so far (I only started today, so I'm figuring out things):

Cool idea! You might want to create a CoeFun instance to avoid typing .f everywhere:

instance : CoeFun (NatRep) (fun _ ↦ ℕ → ℕ) := ⟨Finsupp.toFun ∘ NatRep.f⟩

Isn't toNat supposed to be multiplication rather than a sum? i.e.

def NatRep.toNat (r : NatRep) : ℕ :=
  r.f.prod (· ^ ·)

Also wdyt about this Red/RedStar alternative?

def NatRep.Red (a b : NatRep) : Prop :=
  a.toNat = b.toNat ∧ a.f.sum (fun _ ↦ id) ≤ b.f.sum (fun _ ↦ id)

[Chris Henson]

@Iván Renison One thing we do have is Cslib.ReductionSystem which is meant to represent reductions generally. If you see the example in the docs at the bottom of that page it shows how to get the notation we use for reductions. Past that, there's not much API yet.

I am not sure about your specific application, but if along the way you prove any general lemmas about normalizing relations, that could be a good location for them.

[Iván Renison]

Yes, it is prod instead of sum :man_facepalming:

[Iván Renison]

Thank you for the ideas

[Iván Renison]

Cslib.ReductionSystem seems to also be useful, thank you

[Iván Renison]

If I probe some useful lemma I will pull request it

[Iván Renison]

Something that is happening to me with Cslib.ReductionSystem is that I want to use things that are defined for relations with it. I could redefine them for Cslib.ReductionSystem, but I don't think that is a nice solution. Do you have some suggestion of what to do?

[Chris Henson]

Maybe defining a coercion to relations is sufficient? If initially working with Cslib.ReductionSystem is painful, you could start by just working with relations and handle that part later.

[Iván Renison]

The idea is to eventually duplicate things from relations to ReductionSystem or to always work mostly with relations?

[Iván Renison]

Currently ReductionSystem.MRed is already a duplication of Relation.ReflTransGen

[Chris Henson]

Usually the intent of defining a one-field structure like this is to prevent you from directly using the type it contains, and you do end up duplicating some definitions.