Tags:Backus FP, Cartesian Monoids, Confluence and Standardization and Simulation of Turing Machines
Abstract:
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." 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. Indeed we shall show that FP can simulate the behavior of an arbitrary Turing machine. Our method for doing this is the following. We first observe that the equational theory of Cartesian monoids is a fragment of FP. 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. This theory, together with fixed points for all Cartesian monoid polynomials, is contained in FP. Now Cartesian monoids with fixed points can be studied using rewrite techniques, learned from lambda calculus, including confluence and standarization. Turing machines can then be simulated; transitions corresponding to fixed points and computations corresponding to standard reductions to normal form.