Beyond Beta-Reduction in Church's lambda Yield

摘要

In the paper, the authors observed that if they change slightly the classicallambda-notation, then they can make more redexes visible. This is useful and is in line with current research on the needed redexes (for normal forms). The authors have shown further that, using item notation (which makes more redexes visible), one is able to stick to the old beta-reduction and just do a simple reshuffling so that these newly visible redexes can be contracted before other redexes. The authors have shown that this reshuffling (which is very simple and can only be enabled in the authors' notation), is correct. In fact, reshuffling does really make all redexes subject to immediate contraction and preserves typing. So, if t has type rho then the reshuffled version of t also has type rho.