A list of equivalent definition of regular langage

Monadic Second order on finite sequence

Consider a logic containing n relation of arity 1, and a single sucessor function. From a finite word w over a alphabet of size n, we'll create a model:

• The universe is the set of position of lettre (ie, {1,2,...,|w|} )
• The sucessor function of i gives i+1 unless it's the last character of the word
• Rf R is the i-th relation symbol, R(j) is true iff the j-th letter of w is i

Then regular langage are exacly langeges for which there exists a MSO formula (meaning you can also quantify over relation of arity 1, i.e. sets of positions). A star-free langage is exacly language for which there exists a first-order formulas.
woua😱!

Simply typed Lambda Calculus

Consider the usual encoding of binary list in simply typed lambda calculus String[A] := (A -> A) -> (A -> A) -> A -> A (correspond to type list = | A of list | B of list | empty in ocaml), and the boolean type Bool[A] := A -> A -> A (correspond to type bool = | A | B in ocaml).
Then, if you consider a function of String[A] -> Bool[B] for some A and B, the accepted value are exacly regular languages!
See more on Tito's thesis that I didn't read that you can found here.