This is mostly for my own benefit.
We start with some term-generating functor parametric in a set of ground terms and a set of names .
Now specialize to a single ground term:
Now mod out by structural equivalence:
Let be a set of names and let M be the set of name-equivalence classes (where is yet to be defined—it’s part of the theory of names in which we’re still parametric).
Prequoting and predereference are an algebra and coalgebra of , respectively:
Real quoting and dereference have to use , defined below.
Define . Does ? I think so; assuming it does, define
so name equivalence is structural equivalence; equivalence of prequoted predereferences is automatic by the definition above.
The fixed point gives us an isomorphism
We can define , because undecidability doesn’t come into play until we add operational semantics. It’s decidable whether two terms are structurally equivalent. Thus
is the identity, satisfying the condition, and
is the identity, which we get for free.
When we mod out by operational semantics (following the traditional approach rather than the 2-categorical one needed for pi calculus):
we have the quotient map
and a map
that picks a representative from the equivalence class.
It’s undecidable whether two terms are in the same operational equivalence class, so may not halt. However, it’s true by construction that
is the identity.
We can extend prequoting and predereference to quoting and dereference on by
which is what we want for quoting and dereference. The other way around involves undecidability.