Dear Scalarazzi,
i noticed that you can use the derivative of data types to build a bridge between nominal and positional access. i've written about it
here. The kernel of the idea can be illustrated in two simple equations.
T[N] = N + [N => T[N]] + T[N] x T[N]
N = ∂T[N]
The first equation is a domain equation for the data type of lambda terms. The second equation says that names (aka variables) must be contexts in lambda terms. This leads to a whole host of interesting new questions. Further, the technique is quite general and applies to a wide range of situations, not just nominal presentations of computational calculi.
Best wishes,
--greg
--
L.G. Meredith
Managing Partner
Biosimilarity LLC
1219 NW 83rd St
Seattle, WA 98117
+1 206.650.3740
http://biosimilarity.blogspot.com
