Mathematical logic seminar – Feb 28 2017

Time: 3:30pm – 4:30 pm

Room: Wean Hall 8220

Speaker: Rick Statman

Department of Mathematical Sciences

CMU

Title: Backus FP is Turing complete

Abstract:

Cartesian monoids are rather simple algebraic structures of which you know many examples. They also travel under many assumed names such as Cantor algebras, Jonsson-Tarski algebras, and Freyd-Heller monoids. John Backus’s FP is just the theory of Cartesian monoids together with fixed points for all Cartesian monoid polynomials.

In his 1977 Turing Award address, John Backus introduced the model of functional programming called “FP”. FP is a descendant of the Herbrand-Godel notion of recursive definablity and the ancestor of the programming language Haskell. One reason that FP is attractive is that it provides “an algebra of functional programs”. However, Backus did not believe that basic FP was powerful enough;

“FP systems have a number of limitations….. If the set of primitive functions and functional forms is weak, it may not be able to express every computable function”. John Backus, 1977 ACM Turing award lecture.

and he moved on to stronger systems. It turns out that, in this respect, Backus was mistaken. Here we shall show that FP can compute every partial recursive function.