Lambda substitution algebras
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.
KeywordsEnvironment Model Unary Operation Countable Family Completeness Theorem Algebraic Logic
Unable to display preview. Download preview PDF.
- [B81]Barendregt,H.P. The Lambda Calculus: its Syntax and Semantics. Studies in Logic, 103, N-Holland, 1982.Google Scholar
- [C88]Cïrulis,J. An Algebraization of First-order Logic with Terms. In “Algebraic logic (Proc. Conf. in Budapest, 1988)”, ed. H.Andréka,J.D.Monk,I.Németi, N-Holland,1991, pp.125–146Google Scholar
- [D91]Diskin,Z.B. Lambda Term Systems. Submitted to Z.Math.Logik und Grundl.Math.Google Scholar
- [F82]Feldman,N. Axiomatization of Polynomial Substitution Algebras. J.Symbolic Logic,47,3(1982), 481–492.Google Scholar
- [M82]Meyer,A.R. What is a Model of the Lambda Calculus? Information and Control,52,1(1982), 87–122.Google Scholar
- [OW82]Obtułowicz,A. and Wiweger,A., Categorical, Functional and Algebraic Aspects of the Type-free Lambda Calculus. in: “Universal algebra and Applications”, Banach Center Publications, 9(1982), 399–422.Google Scholar
- [PS92]Pigozzi,D. and Salibra,A. Polyadic Algebras over Nonclassical Logics. Manuscript.Google Scholar