Lambda substitution algebras

1993

In the paper an algebraic metatheory of type-free λ-calculus is developed. Our version is based on lambda substitution algebras (λSAs), which are just SAs introduced by Feldman (for algebraizing equational logic) enriched with a countable family of unary operations of λ-abstraction and a binary operation of application. Two representation theorems, syntactical and semantic, are proved, what directly provides completeness theorems.