Partial Commutative Monoids

Stream: Is there code for X?

[Vladimir Gladstein]

Does anyone know of any formalizations of partial commutative monoids theory? I need them for my current project in Lean.
There are some attempts in Coq, I don't know of any in Lean4

[Johan Commelin]

What is a partial commutative monoid?

[Vladimir Gladstein]

Johan Commelin said:

What is a partial commutative monoid?

This is like a monoid, but an operation might be partial. I am interested in it, because pcms are commonly used in computer science to formalize program logics.

[Johan Commelin]

Aha. Is it ok to totalize the operation and study Option M instead? Because then there might be some theory in mathlib...

[Johan Commelin]

It sounds quite related to docs#CommMonoidWithZero

[Johan Commelin]

Where you would treat 0 as NaN

[Vladimir Gladstein]

Yes, I guess, In theory I could derive a pcm instance from ComMonoid (Option M) and vice versa. But I was hoping that some has already done that
Thanks!

[Johan Commelin]

Are you also interested in homomorphisms between pcms? Are those always total, or also partial?

[Vladimir Gladstein]

Johan Commelin said:

Are you also interested in homomorphisms between pcms? Are those always total, or also partial?

I know that pcm homomorphisms are applicable in computer science for program logic, but I do not think I will need those in my project.
According to Coq pcm formalization those morphisms can be partial.

[Johan Commelin]

Ok, in that case, I think the category of CommMonoidWithZero objects and MonoidHom morphisms is equivalent to the category of pcms with partial homs.

[Johan Commelin]

So I hope you can apply the theory that we have about CommMonoidWithZero in your project.

[Kevin Buzzard]

The only definition we've seen here is "like a monoid, but an operation may be partial". It would be a good exercise to either prove or disprove that pcm structures on a type correspond to monoid with zero structures on the corresponding option type sending none to 0. This may or may not work out, depending on what the actual definition of pcm is.

[Ira Fesefeldt]

I gave the coq formalization only a quick look. But I believe, usually these PCMs (and also that coq formaliazation) are defined in ITPs by defining a predicate valid that captures exactly these elements which are considered defined. Thus usually PCMs have not only one undefined element, but multiple.

This formalization of PCMs may make it more complicated to proof the equivalence to CommMonoidWithZero.

Personally, I prefer the Option M variant in my projects, but I don't require exotic PCMs, for which I believe the other PCM definition is more convient.

[Matthew Ballard]

There is also docs#Part

[Adam Topaz]

I think the right mathematical abstraction is to develop something like "algebra relative to a monad". Partial operations would correspond to the Option monad. Hyperoperations would correspond to the Set monad, etc. Essentially you work in the Kleisli category.