Conference
Lambda substitution algebras
Abstract
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.
Authors
Diskin Z; Beylin I
Series
Lecture Notes in Computer Science
Volume
711
Pagination
pp. 423-432
Publisher
Springer Nature
Publication Date
1993
DOI
10.1007/3-540-57182-5_34
Conference proceedings
Lecture Notes in Computer Science
ISSN
0302-9743