This is part of the Tutorial:Graphic lambda calculus.
Here are described the moves related to the univalent termination gate. There are local and global pruning moves.
- LOCAL PRUNING. The local moves which eliminate “dead edges” or “dead nodes” are the following:
These moves go in one direction, compared with the graphic beta move, which is allowed in both directions. In arXiv:1207.0332v1 [cs.LO], paragraph 2.6, where this moves were introduced, they are allowed in both directions. However, I intend to modify this and to introduce generation moves instead, like CREA and GARB, as explained in Ancient Turing machines posts here and here.
- GLOBAL PRUNING. Like the GLOBAL FAN-OUT move, this is a global move. A local version of it, in the spirit of the LOCAL FAN-OUT move, may be introduced. For any graph in , if is connected ONLY to a termination gate, then we may remove it.
Return to Tutorial:Graphic lambda calculus