Lambda abstraction algebras: representation theorems. (English) Zbl 0874.68188
Summary: Lambda abstraction algebras (LAAs) are designed to algebraize the untyped lambda calculus in the same way cylindric and polyadic algebras algebraize the first-order predicate logic. Like combinatory algebras they can be defined by true identities and thus form a variety in the sense of universal algebra, but they differ from combinatory algebras in several important respects. The most natural LAAs are obtained by coordinatizing environment models of the lambda calculus. This gives rise to two classes of LAAs of functions of finite arity: functional LAAs (FLA) and point-relativized functional LAAs (RFA). It is shown that RFA is a variety and is the smallest variety including FLA. Dimension-complemented LAAs constitute the widest class of LAAs that can be represented as an algebra of functions and are known to have a natural intrinsic characterization. We prove that every dimension-complemented LAA is isomorphic to RFA. This is the crucial step in showing that RFA is a variety.
MSC:
| 68Q55 | Semantics in the theory of computing |
References:
| [1] | Abadi, M.; Cardelli, L.; Curien, P. L.; Lévy, J. J., Explicit substitutions, (Proc. 17th Conf. POPL. Proc. 17th Conf. POPL, San Francisco (1990)) · Zbl 0941.68542 |
| [2] | Adachi, T., A categorical characterization of lambda calculus models, (Research Report No. C-49 (1983), Dept. of Information Sciences, Tokio Institute of Technology) |
| [3] | Barendregt, H. P., The Lambda Calculus. Its Syntax and Semantics, (Studies in Logic and the Foundations of Mathematics, Vol. 103 (1985), North-Holland: North-Holland Amsterdam) · Zbl 0467.03010 |
| [4] | Barendregt, H. P., Functional programming and lambda calculus, (van Leeuwen, Jan, Handbook of Theoretical Computer Science, Vol. B (Formal Models and Semantics) (1990), Elsevier: Elsevier Amsterdam), 321-363 · Zbl 0900.68110 |
| [5] | Barendregt, H. P.; Koymans, K., Comparing some classes of lambda calculus models, (Hindley, J. R.; Seldin, J. P., To H.B. Curry: Essays on Combinatory Logic, Lambda-Calculus and Formalism (1980), Academic Press: Academic Press New York), 287-302 |
| [6] | Church, A., A set of postulates for the foundation of logic, Ann. Math., 2, 346-366 (1933) · JFM 58.0997.06 |
| [7] | Church, A., The Calculi of Lambda Conversion (1941), Princeton University Press: Princeton University Press Princeton · JFM 67.0041.01 |
| [8] | Curien, P. L., Categorial Combinators, Sequential Algorithms and Functional Programming (1986), Pitman: Pitman London · Zbl 0643.68004 |
| [9] | Curry, H. B.; Feys, R., (Combinatory Logic, Vol I (1958), North-Holland: North-Holland Amsterdam) · Zbl 0175.27601 |
| [10] | Z.B. Diskin, Lambda term systems, manuscript.; Z.B. Diskin, Lambda term systems, manuscript. |
| [11] | Diskin, Z. B.; Beylin, I., Lambda substitution algebras, (Borzyskowski, A. M.; Sokolowski, S., Proc. 18th Internat. Symp. on Mathematical Foundations of Computer Science. Proc. 18th Internat. Symp. on Mathematical Foundations of Computer Science, Lecture Notes in Computer Science, Vol. 711 (1993), Springer: Springer Berlin), 423-432 · Zbl 0925.03091 |
| [12] | Feldman, N., Axiomatization of polynomial substitution algebras, J. Symbolic Logic, 47, 481-492 (1982) · Zbl 0494.03047 |
| [13] | Feldman, N., Representation of substitution algebras, J. Symbolic Logic, 49, 677-678 (1984), abstract |
| [14] | Grätzer, G., Universal Algebra (1979), Springer: Springer New York · Zbl 0182.34201 |
| [15] | Halmos, P., Homogeneous locally finite polyadic Boolean algebras of infinite degree, Fund. Math., 43, 255-325 (1956) |
| [16] | Halmos, P., Algebras Logic (1962), Chelsea, New York · Zbl 0101.01101 |
| [17] | Henkin, L.; Monk, J. D.; Tarski, A., Cylindric Algebras (1971), North-Holland: North-Holland Amsterdam, Parts I and II · Zbl 0214.01302 |
| [18] | Henkin, L.; Monk, J. D.; Tarski, A.; Andréka, H.; Németi, I., Cylindric Set Algebras, (Lecture Notes in Mathematics, Vol. 833 (1981), Springer: Springer Berlin) · Zbl 0497.03025 |
| [19] | Hindley, R.; Longo, G., Lambda-calculus models and extensionality, Zeit. f. Math. Logik u Grund. der Math., 26, 289-310 (1980) · Zbl 0453.03015 |
| [20] | Krivine, J. L., Lambda-Calcul, Types and Models (1990), Masson: Masson Paris · Zbl 0697.03004 |
| [21] | LeBlanc, L., Transformation algebras, Canad. J. Math., 13, 602-613 (1961) · Zbl 0263.02027 |
| [22] | Meyer, A. R., What is a model of the lambda calculus?, Inform. and Control, 52, 87-122 (1982) · Zbl 0507.03002 |
| [23] | Németi, I., Algebraizations of quantifier logics. An introductory overview, Studia Logica, 50, 485-569 (1991) · Zbl 0772.03033 |
| [24] | Obtułowicz, A.; Wiweger, A., Categorical, functorial, and algebraic aspects of the type-free lambda calculus, (Traczyk, T., Universal Algebra and Applications, Banach Center Publications, Vol. 9 (1982), PWD-Polish Scientific Pub: PWD-Polish Scientific Pub Warsaw) · Zbl 0514.03010 |
| [25] | Pigozzi, D.; Salibra, A., An introduction to lambda abstraction algebras, (Abad, M., Proc. IX Latin American Symp. on Mathematical Logic. Proc. IX Latin American Symp. on Mathematical Logic, Bahia Blanca, Argentina, 1992. Proc. IX Latin American Symp. on Mathematical Logic. Proc. IX Latin American Symp. on Mathematical Logic, Bahia Blanca, Argentina, 1992, Nortas de Logica Matematica, Vol. 38 (1994), Instituto de Matematica, Universidad Nacional del Sur: Instituto de Matematica, Universidad Nacional del Sur Bahia Blanca, Argentina), 93-112 · Zbl 0820.03039 |
| [26] | Pigozzi, D.; Salibra, A., Dimension-complemented lambda abstraction algebras, (Nivat, M.; Rattray, C.; Rus, T.; Scollo, G., Algebraic Methodology and Software Technology (AMAST’93) Proc. 3rd Internat. Conf. on Algebraic Methodology and Software Technology, University of Twente. Algebraic Methodology and Software Technology (AMAST’93) Proc. 3rd Internat. Conf. on Algebraic Methodology and Software Technology, University of Twente, The Netherlands, 21-25, June, 1993. Algebraic Methodology and Software Technology (AMAST’93) Proc. 3rd Internat. Conf. on Algebraic Methodology and Software Technology, University of Twente. Algebraic Methodology and Software Technology (AMAST’93) Proc. 3rd Internat. Conf. on Algebraic Methodology and Software Technology, University of Twente, The Netherlands, 21-25, June, 1993, Workshops in Computing (1993), Springer: Springer London), 131-138 |
| [27] | Pigozzi, D.; Salibra, A., A representation theorem for lambda abstraction algebras, (Borzyszkowski, A. M.; Sokolowski, S., Proc 18th Internat. Symp. on Mathematical Foundations of Computer Science. Proc 18th Internat. Symp. on Mathematical Foundations of Computer Science, Lecture Notes in Computer Science, Vol. 711 (1993), Springer: Springer Berlin), 629-639 · Zbl 0925.03087 |
| [28] | Pigozzi, D.; Salibra, A., Lambda abstraction algebras. Coordinatization of models of lambda calculus (1993), preprint |
| [29] | D. Pigozzi and A. Salibra, The abstract variable-binding calculus, preprint.; D. Pigozzi and A. Salibra, The abstract variable-binding calculus, preprint. · Zbl 0836.03038 |
| [30] | Pinter, C., Cylindric algebras and algebras of substitution, Trans. Amer. Math. Soc., 175, 167-179 (1973) · Zbl 0266.02036 |
| [31] | Salibra, A., A general theory of algebras with quantifiers, (Andréka, H.; Monk, J. D.; Németi, I., Algebraic Logic, Proc. Conf.. Algebraic Logic, Proc. Conf., Budapest 1988. Algebraic Logic, Proc. Conf.. Algebraic Logic, Proc. Conf., Budapest 1988, Colloq. Mat. Soc. J. Bolyai, Vol. 54 (1991), North-Holland: North-Holland Amsterdam), 573-620 · Zbl 0746.03056 |
| [32] | Scott, D. S., Data types as lattices, SIAM J. Comput., 5, 522-587 (1976) · Zbl 0337.02018 |
| [33] | Scott, D. S., Lambda calculus: some models, some philosophy, (Barwise, J.; Keisler, H. J.; Kunen, K., The Kleene Symposium, Studies in Logic, Vol. 101 (1980), North-Holland: North-Holland Amsterdam) · Zbl 0515.03004 |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
