2020-05-20: Fixed-point operators from recursive types I rak
================================================================
I was reading Marcelo Fiore's PhD thesis this afternoon [0] and
came across the following remark:
"In the sequel recursion at the level of programs is not
considered primitive, instead our viewpoint is that it
arises from recursion at the level of types."
I've heard many times over the years that you can do this, but I
never sat down and worked out how to encode fixed point
operators using recursive types. So here it goes.
----------------
- The language -
----------------
Assume we have a language containing the following rule defining
a fixed-point operator:
G, x : t |- e : t
-------------------- (fix)
G |- fix(x.e) : t
where operationally,
---------------------------------- .
fix(x.e) ~~> [fix(x.e) / x] e
Also suppose that our language has isorecursive types [1] given
by:
G |- e : pa.t
---------------------------- (unfold)
G |- unfold e : [pa.t/a]t
G |- e : [pa.t/a]t
---------------------------- (fold)
G |- fold e : pa.t
with dynamics
---------------- ,
fold(v) value
------------------------ ,
unfold(fold(e)) ~~> e
and
e ~~> e'
--------------------------- .
unfold(e) ~~> unfold(e')
We also assume abstraction / application:
G, x : t |- e : t'
---------------------- (abs)
G |- \x.e : t -> t'
G |- e : t -> t' G |- e' : t
------------------------------------- (app)
G |- ee' : t'
with a call-by-value (or CBN if you want) dynamics:
------------- ,
\x.e value
v value
--------------------- ,
(\x.e)v ~~> [v/x]e
v value e ~~> f
---------------------- ,
ve ~~> vf
e ~~> f
------------ .
eg ~~> fg
----------------
- The encoding -
----------------
We can encode fix(x.e) as
f(fold(f))
where
f = \y.[(unfold(y))y/x]e.
First, this is well-typed:
------------------------------- (var)
y : pa.a -> t |- y : pa.a -> t
--------------------------------------------- (unfold) ------------------------------ (var)
y : pa.a -> t |- unfold(y) : (pa.a -> t) -> t y : pa.a -> t |- y : pa.a -> t
-------------------------------------------------------------------------------------- (app)
y : pa.a -> t |- (unfold(y))y : t
so using substitution / cut we get
G, x : t |- e : t
-------------------------------------------- (subst)
G, y : pa.a -> t |- [(unfold(y))y/x]e : t
----------------------------------------------- (abs)
G |- \y.[(unfold(y))y/x]e : (pa.a -> t) -> t
where we recognize the term in the bottom as f. Call the above
derivation D1. We also get
D1
D1 -------------------------- (fold)
G |- f : (pa.a -> t) -> t G |- fold(f) : pa.a -> t
-------------------------------------------------------- (app)
G |- f(fold(f)) : t
So we see that our encoding at least has the right type.
Next we check that it has the right operational behaviour:
fix(x.e)
=== f(fold(f))
~~> [(unfold(fold(f))fold(f)/x] e
??? [f(fold(f))/x] e
=== [fix(x.e)/x] e
The question is, how do I show the step labelled '???'? To be
continued...
[0] Fiore, Marcelo P., "Axiomatic Domain Theory in Categories of
Partial Maps", PhD thesis, The University of Edinburgh
Department of Computer Science, October 1994, v+282 pp.
[1] I'm punning on the visual resemblence between 'p' and the
non-ASCII greek letter rho, which is my preferred binder for
recursive types.
