1. 39
  1. 8

    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.”

    1. 6

      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.”

      1. 5

        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.

        1. 4

          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.