LAMBDA-ABSTRACTION ALGEBRAS - REPRESENTATION THEOREMS

Lambda abstraction algebras (LAAs) are designed to algebraize the unty ped lambda calculus in the same way cylindric and polyadic algebras al gebraize the first-order predicate logic. Like combinatory algebras th ey can be defined by true identities and thus form a variety in the se nse of universal algebra, but they differ from combinatory algebras in several important respects. The most natural LAAs are obtained by coo rdinatizing environment models of the lambda calculus. This gives rise to two classes of LAAs of functions of finite arity: functional LAAs (FLA) and point-relativized functional LAAs (RFA). It is shown that RF A is a variety and is the smallest variety including FLA. Dimension-co mplemented LAAs constitute the widest class of LAAs that can be repres ented as an algebra of functions and are known to have a natural intri nsic characterization. We prove that every dimension-complemented LAA is isomorphic to RFA. This is the crucial step in showing that RFA is a variety.