A few days ago, I thought that I had understood pi calculus in terms of category theory, and I did, in a way.
calculus
model in Set
type
set of values
term
function
(deterministic outcome)
rewrite rule
identity functional
calculus
model in Set
process
set of states
reduction rule
state update rule
(deterministic outcome)
To make lambda calculus into a category, we mod out by the rewrite rules and consider equivalence classes [...]
We can write any expression like as a full binary tree where the nodes denote evaluation of the left child at the right, and the leaves are values:
Figure 1:
[In the caption of figure 1, the expression is slightly different; when using trees, it's more convenient to curry all the functions---that is, replace every [...]
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 [...]
They’re the same thing! Why doesn’t anyone ever say so?
Assume A and B are types; the continuation passing transform takes a function (here I’m using C++ notation)
B f(A a);
and produces a function
<X> CPT_f(<X> (*k)(B), A a) {
return k(f(a));
}
where X is any type. In CPT_f, instead of returning the value f(a) directly, [...]
