I do like the [currently] last comment, which puts this in perspective for non-gurus like moi:

“Let’s put a fine point on this: Decidability and soundness are two distinct properties when talking about type systems. It is perfectly valid to have undecidable type checking/synthesis but still have a system that is sound. […] Type Inference in System F is also undecidable (don’t confuse this with type checking, which is decidable), but variants of that system form the basis of Haskell and many many flavors of ML.”

A nice demonstration of using algebraic structures in programming. The post is extremely clear, and I like the technique of “Here’s a situation. Here’s some maths that models the situation. Here are the consequences of the maths.”

In case anyone else saw the “semi-group with an undecidable problem” and immediately tried to figure out what it is and why it is undecidable: it is apparently known as the “Tzeitin semigroup” or “the Tzeitin semigroup S7” in the literature searches I’ve done. I’ve yet to find the original proof, but it’s ~20 pages of Russian so I’d likely struggle to make much of it if I did find it.

Either way, this seems like a fairly well known example of a semigroup for which the word problem is undecidable.

For those interested, a proof is in Theorem 2.2 of Adian, Durnev, Decision problems for groups and semigroups, Russian Mathematical Surveys, Volume 55 (2002), Number 2, 207–296.

I was also unable to find an online copy of Tseitin’s 1956 original, it looks like the archive of Doklady Akademii Nauk is only available starting from 1957.

I do like the [currently] last comment, which puts this in perspective for non-gurus like moi:

A nice demonstration of using algebraic structures in programming. The post is extremely clear, and I like the technique of “Here’s a situation. Here’s some maths that models the situation. Here are the consequences of the maths.”

In case anyone else saw the “semi-group with an undecidable problem” and immediately tried to figure out what it is and why it is undecidable: it is apparently known as the “Tzeitin semigroup” or “the Tzeitin semigroup S7” in the literature searches I’ve done. I’ve yet to find the original proof, but it’s ~20 pages of Russian so I’d likely struggle to make much of it if I did find it.

Either way, this seems like a fairly well known example of a semigroup for which the word problem is undecidable.

For those interested, a proof is in Theorem 2.2 of Adian, Durnev,

Decision problems for groups and semigroups, Russian Mathematical Surveys, Volume55(2002), Number2, 207–296.I was also unable to find an online copy of Tseitin’s 1956 original, it looks like the archive of Doklady Akademii Nauk is only available starting from 1957.