Analysing innocent interaction

We analyse the PAM via game semantics. We formalize the role of the
PAM as that of a "referee" mediating between the interacting
terms/strategies. In this way, we see that we can equivalently compute
the "execution trace" (a run of the PAM) as a sequence of moves or in
desequentialized form as a kind of tree. If we restrict our attention
to innocent strategies satisfying a stronger visibility condition than
usual, we can simplify the PAM by eliminating the referee. The
resulting machine (the CPAM or cellular PAM) correctly computes
interaction between these constrained innocent strategies.

We then show that the CPAM essentially behaves as an abstract machine
for cellular lambda-terms (and lambda-mu-terms), hence its
name. Cellular lambda-terms [Padovani, Loader] serve as canonical
representatives for contextual equivalence classes in unary PCF: any
term of unary PCF can be "cellularized" to find such a
representative. This observation leads to the listing algorithm which
establishes the effective presentability of the (simple,
set-theoretic) model of unary PCF and, as a consequence, that
contextual equivalence is decidable.

This "syntactic cellularization" has a semantic counterpart: given an
innocent strategy, we can "cellularize" it. However, unlike in the
syntactic case, we can cellularize *any* innocent strategy; this
doesn't contradict the undecidability of, say, boolean PCF since the
semantic cellularization doesn't preserve the bracketing
condition. So, any run of the PAM can be simulated by a (typically
much longer) run of the CPAM operating on the cellularized strategies.