Notes on "A CUCH-Machine: The Automatic Treatment of Bound Variables ''1
Mariangiola Dezani · 1973
The method described in ReL 1 does not always correctly establish the bonds between the variables. In fact, during the reduction to normal form of the h-formula ((ty)(~yy)) and of all those in which the same variable that is free in the left subformula of an application occurs bound in the right subformula, this variable is wrongly considered as bound. To prevent this, it is necessary to modify the levels assigned to the formulas in the fi-generation. We therefore give the correct fi-generation statements and the correct algorithm of the fi-generation.