[ ] Unify dataization.
The implementation and the description of the dataization in the paper are quite different in the structure, but they behave in a same way. I wonder how can I prove that? ?
[ ] Can I do .ρ but there's no ρ and there is φ, and then R_φ is applied and we get something unexpected
[ ] About morphing lambda whenever it's possible. What if we start normalization when it's not possible to morph lambda, then do something and lambda appears and after that normalization doesn't terminate
Rewrite rules
R_DOT
andR_COPY
ξ-dispatch
R_COPY
R_COPY_EMPTY
R_φ
R_OVER
R_MISS
R_STOP
R_DD
R_DC
Dataization
Φ-dispatch
andR_COPY
.Other issues
.ρ
but there's noρ
and there isφ
, and thenR_φ
is applied and we get something unexpected