## Reflective calculi

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:

such that

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

and then

which is what we want for quoting and dereference. The other way around involves undecidability.

leave a comment