Iowa Type Theory Commute

I talk about my efforts to formalize lambda-calculus with named variables and explicit alpha-equivalence, as originally proposed by Church.  One reason to do that, besides just a love of being ornery, is to be able to state and prove theorems about alpha-equivalence.  One example class of such theorems concern when alpha-equivalence can be avoided, in the sense that beta-reduction can proceed without any variable capture, while not requiring renaming variables.  I have a companion blog post that talks about this, with a link to the repo with my Agda code so far.

A system of word equations is called quadratic if no variable occurs more than twice in it.  There is an interesting simple algorithm to solve quadratic systems of word equations, which I talk through in this episode.  My source is Chapter 12 of "Algebraic Combinatorics on Words" by Lothaire.

The problem of word equations is a rather storied one, including frustrated connections to Hilbert's Tenth problem.  Word equations relate expressions consisting of concatenations of variables and constant symbols.  An example is a X = X a, where X is a variable and a is a constant.  A solution maps variables to strings of constant symbols making the two sides identical.  In this episode, I discuss the problem a little, and what I learned so far about how it is solved.

In this episode, I give further arguments in favor of coercive subtyping from a software-engineering perspective.  I also explain the critical concept of coherence.

I explain the story from last episode.