UCalgary Peripatetic Seminar: Robin Cockett

Moses Schonfinkel invented “combinatory logic” — aka combinatory algebra (CA ) — in 1920. It consisted of a binary operation and two constants S and K (called combinators by Haskell Curry who further investigated CAs in the 1950s) which satisfy just two identities. That such a simple gadget can generate all computable functions is — well — amazing. 

However, that was not the end of the story. 

In 1975 Solomon Feferman introduced the notion of a partial combinatory algebra (PCA) and showed that it too could generate all computable functions … but furthermore had as a prime example the usual notion of computability which the average CS student meets in theory courses via Turing machines. Again, this is an amazingly simple structure which can express all computation: it consists of a partial binary operation and combinators S and K which satisfy just four identities. 

In 2008 Pieter Hofstra and I introduced Turing Categories: we argued that this notion subsumed all the previous notions of computability. Furthermore, it turned out that the initial Turing category was generated by a generic PCA … and, thus, this gadget was, therefore, the grandad of all computation.

Now CAs are well known to have a confluent rewriting system, which this is very important as it is the rewriting system which generates computation. By analogy to a CA, this generic PCA should have a nice rewriting system. However, it is still has not been proven that PCAs do have a confluent rewriting system!

The talk is aimed to introduce Turing categories, PCAs, and a suggestion for what the rewriting system should be.