Unify the rules in the implementation and in the paper

[eyihluyc]

Rewrite rules

• [ ] NF condition in R_DOT and R_COPY
  • https://github.com/objectionary/normalizer/pull/449
  • https://github.com/yegor256/phi-paper/pull/45
• [ ] https://github.com/objectionary/normalizer/issues/448
  • [ ] https://github.com/yegor256/phi-paper/pull/46
  • [ ] https://github.com/objectionary/normalizer/pull/468
• [x] ξ-dispatch
• [x] R_COPY
• [X] R_COPY_EMPTY
• [X] R_φ
• [X] R_OVER
• [X] R_MISS
• [X] R_STOP
• [X] R_DD
• [X] R_DC

Dataization

• [ ] 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? ?
• [ ] https://github.com/yegor256/phi-paper/issues/43 – termination issues caused by Φ-dispatch and R_COPY.
  • [ ] https://github.com/yegor256/phi-paper/pull/47 – what to consider nf in dataization
  • [ ] https://github.com/yegor256/phi-paper/pull/48 – morph lambda before normalization

Other issues

• [ ] address the failing tests (?)
• [ ] Other ideas where to look for problems:
  • [ ] 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