Mathematical logic seminar – March 29 2016

Time: 12:30 – 13:30

Room: Wean Hall 8220

Speaker: Rick Statman

Department of Mathematical Sciences

CMU

Title: Algebraic Structures Intrinsic to Functional Programming

Abstract:

Lambda Calculus is the starting point of all functional programming. Since Church noticed the undecidability of the word problem for semigroups ([1]), it has been understood that certain algebraic strutures are embedded in lambda calculus. These include the B,I monoid ([2],[4]), the free Cartesian monoid which includes the positive part of the Freyd,Heller, Thompson group ([5],[6]), the profinite group of hereditary permutations ([3]), and the near semirings and b.a.d. algebras of [7].

In this talk we shall first survey the backgound results. Next we outline the theorem that that every semigroup with a recursively enumerable word problem is pointwise embeddable in the combinator semigroup. Finally we discuss an number of related results concerning embedding congruences and r.e. subsets of free semigroups. In particular, we show that the free monoid generated by an arbitrary r.e. subset of combinators can be represented as the monoid of all terms which fix a finite set of points.

1) Church, Alonzo A Note on the Entscheidungsproblem J. of Symbolic Logic, vol. 1 1936

2) Curry, Haskell B., Feys, Robert Combinatory Logic. Vol. I North Holland 1958

3) Dazani-Ciancaglini, Mariangiola Characterization of normal forms … T.C.S. 2, 1976

4) Statman, Rick Combinators and the theory of partitions, CMU Research Report No. 88-31 1988

5) Statman, Rick On Cartesian Monoids CSL ’97 LNCS 1258

6) Statman, Rick Cartesian Monoids MFPS 2010 ENTCS Vol 65 Sept 6 2010

7) Statman, Rick Near semirings and lambda calculus TLCA 2014 LNCS 8560