Abstract:An axiomatization of equality of regular expressions was given by Arto Salomaa in 1966, using Janusz Brzozowski's "derivatives" in 1964. Volodimir Redko also showed in 1964 that a finite set of axioms is insufficient, so Salomaa used an algorithmic side condition in his system. John Horton Conway formulated an algebraic approach in 1971. Albert Meyer and Larry Stockmeyer showed in 1972 that the problem requires polynomial space. Dexter Kozen developed a new "inequational" axiomatization using Conway's algebraic ideas in 1994 (requiring no algorithmic side conditions). Jan Rutten suggested using "coalgebraic" ideas in 1999 and Clemens Grabmayer came up with an axiomatization in 2005. This talk surveys these ideas and points out challenges remaining after 50 years of work in this area.
