6533b861fe1ef96bd12c421c
RESEARCH PRODUCT
Lambda substitution algebras
Ilya BeylinZinovy Diskinsubject
AlgebraDiscrete mathematicsUnary operationBinary operationComputer Science::Logic in Computer ScienceCompleteness (logic)Substitution (algebra)Countable setGödel's completeness theoremEquational logicAlgebraic logicMathematicsdescription
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.
| year | journal | country | edition | language |
|---|---|---|---|---|
| 1993-01-01 |