Normalized subset of Pi+

vikraman / 2DTypes

Collaborative work on reversible computing

17 stars 1 forks source link

Closed inexxt closed 3 years ago

inexxt commented 3 years ago

To do:

[x] Define normalized types (1 + (1 + ... + (1 + 0))) and normalized 1-combinators
[x] Show that for any type, there is 1-combinator between it and its normalized version
[ ] Show that for any two types t1 and t2 and a 1-combinator c between them, there exists a normalized 1-combinator nc and a 2-combinator nnc such that the (obvious) diagram commutes up to nnc.

inexxt commented 3 years ago

No longer relevant. Created separate issues for the remaining parts.