When beta reducing, "capture avoiding substitution" is not taken place.
For example, the term (\x. \y. x y) y
should be reduced to \z. y z
by renaming y
to z
in (\x. \y. x y)
, but in the interpreter, this term is reduced to \y. y y
, which is ill typed lambda term.
By exploiting this, the input
f1 = (\f:I->I. \g:A->A. g)
f2 = (\x:(I->I)->(A->A)->A->A. \f1:A->A. x dec) f1 (\d:A. d)