A piece of the Rosetta stone
| category | lambda calculus | pi calculus | Turing machine |
| objects | types | structural congruence classes of processes |  where  is the natural numbers and  is all binary sequences with finitely many ones. |
| a morphism | an equivalence class of terms | a specific reduction from one process state to the next | a specific transition from one state and position of the machine to the next |
| dinatural transformation from the constant functor (mapping to the terminal set and its identity) to a functor generated by hom, products, projections, and exponentials (if they’re there) | combinator | reduction rule (covers all reductions of a particular form) | tape-head update rule (covers all transitions with the current cell and state in common) |
| products | product types | parallel processes | multiple tapes |
| internal hom | exponential types | all types are exponentials? | ? |
| Model of the category in Set | A set of values for each data type and a function for each morphism between them | A set of states for each process and a single evolution function out of each set. | ? |
This won’t be appearing in our Rosetta stone paper, but I wanted to write it down. What flavor of logic corresponds to the pi calculus? To the Turing machine?
[...] piece of the stone A few days ago, I thought that I had understood pi calculus in terms of category theory, and I did, in a [...]