Lambda substitution algebras

  • Zinovy Diskin
  • Ilya Beylin
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 711)


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.


Environment Model Unary Operation Countable Family Completeness Theorem Algebraic Logic 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. [B81]
    Barendregt,H.P. The Lambda Calculus: its Syntax and Semantics. Studies in Logic, 103, N-Holland, 1982.Google Scholar
  2. [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
  3. [D91]
    Diskin,Z.B. Lambda Term Systems. Submitted to Z.Math.Logik und Grundl.Math.Google Scholar
  4. [F82]
    Feldman,N. Axiomatization of Polynomial Substitution Algebras. J.Symbolic Logic,47,3(1982), 481–492.Google Scholar
  5. [M82]
    Meyer,A.R. What is a Model of the Lambda Calculus? Information and Control,52,1(1982), 87–122.Google Scholar
  6. [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
  7. [PS92]
    Pigozzi,D. and Salibra,A. Polyadic Algebras over Nonclassical Logics. Manuscript.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1993

Authors and Affiliations

  • Zinovy Diskin
    • 1
  • Ilya Beylin
    • 2
  1. 1.Frame Inform SystemsRigaLatvia
  2. 2.University of LatviaRigaLatvia

Personalised recommendations