The Lambda Calculus is Algebraic

this paper, we point out that the failure of the -rule, and the subsequent need for a non-equational class of models, is not due to the lambda calculus itself, but to the way free variables are usually interpreted in these models. An equation M = N between open terms is usually said to be satisfied in a lambda algebra A if it holds for all substitutions of elements of A for the free variables. We call this the local interpretation, and define M = N to hol