Abstract
We develop the elementary theory of higher-order universal algebra using the non-standard approach to finite type theory introduced by Henkin. Basic results include: existence theorems for free and initial higher type algebras, a complete higher type equational calculus, and characterisation theorems for higher type equational and Horn classes.
(Extended Abstract)
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
J. Barwise and S. Feferman (eds), Model-Theoretic Logics, (Springer Verlag, Berlin, 1985).
G. Birkhoff, On the structure of abstract algebras, Proc. Cambridge Phil. Soc. 31 (1935) 433–454.
M. Broy, Equational specification of partial higher-order algebras, in: M. Broy (ed) Logic of programming and calculi of discrete design, (Springer Verlag, Berlin, 1987).
R. Burstall, D. MacQueen and D. Sanella, Hope: an experimental applicative language, in: Proceedings, First LISP Conference, Stanford University, 1980, 136–143.
C.C. Chang and H.J. Keisler, Model Theory, third edition, (North Holland, Amsterdam, 1990).
P.M. Cohn, Universal Algebra, (Harper and Row, New York, 1965).
J.A. Goguen and J. Meseguer, Completeness of many-sorted equational logic, Association for Computing Machinery SIGPLAN Notices 17 (1982) 9–17.
M. Gordon, Why higher-order logic is a good formalism for specifying and verifying hardware, in: G. Milne and P.A. Subrahmanyam, (eds) Formal aspects of VLSI design, (North Holland, Amsterdam, 1986).
R. Harper, D. MacQueen and R. Milner, Standard ML, Technical Report ECS-LFCS-86-2, Department of Computer Science, University of Edinburgh, 1986.
L. Henkin, Completeness in the theory of types, J. Symbolic Logic 2 (1950) 81–91.
T. Jech, Set theory, (Academic Press, New York, 1978).
G. Kreisel and J.L. Krivine, Elements of mathematical logic: model theory, (North Holland, Amsterdam, 1967).
T.S.E. Maibaum and C.J. Lucena, Higher-order data types, International Journal of Computer and Information Sciences 9, (1980) 31–53.
A.I. Malcev, Algebraic Systems, (Springer Verlag, Berlin, 1973).
W.G. Malcolm, Application of higher-order ultraproducts to the theory of local properties in universal algebras and relational systems, Proc. London Math. Soc. 3 (1973) 617–637.
K. Meinke, Universal algebra in higher types, to appear in: Theoretical Computer Science, 1991.
K. Meinke, Subdirect representation of higher type algebras, Report CSR 14–90, Department of Mathematics and Computer Science, University College of Swansea, 1990.
K. Meinke and J.V. Tucker, The scope and limits of synchronous concurrent computation, in: F. H. Vogt, (ed) Concurrency '88, Lecture Notes in Computer Science 335 (Springer Verlag, Berlin, 1988) 163–180.
K. Meinke and J.V. Tucker, Universal algebra, to appear in: S. Abramsky, D. Gabbay and T.S.E. Maibaum, (eds) Handbook of Logic in Computer Science, (Oxford University Press, Oxford, 1991).
D.A. Miller and G. Nadathur, Higher-order logic programming, Departmental Report MS-CIS-86-17, University of Pennsylvania, Department of Computer and Information Science, 1986.
B. Möller, Algebraic specifications with higher-order operators, in: L.G.L.T. Meertens (ed) Program specification and transformation, (North Holland, Amsterdam, 1987a).
B. Möller, Higher-order algebraic specifications, Facultät für Mathematik und Informatik, Technische Universität München, Habilitationsschrift, 1987b.
B. Möller, A. Tarlecki and M. Wirsing, Algebraic specifications of reachable higher-order algebras, in: D. Sannella and A. Tarlecki (eds), Recent Trends in Data Type Specification, Lecture Notes in Computer Science 332, (Springer Verlag, Berlin, 1988) 154–169.
K. Parsaye-Ghomi, Higher-order abstract data types, Department of Computer Science, University of California at Los Angeles, PhD thesis, (1981).
A. Poigné, On specifications, theories and models with higher types, Information and Control 68, (1986) 1–46.
J.E. Stoy, Denotational semantics: the Scott-Strachey approach to programming language theory (MIT Press, Cambridge, Massachusetts, 1977).
D. Turner, Miranda: a non-strict functional language with polymorphic types, in: J-P. Jouannaud (ed) Functional programming languages and computer architectures, Lecture Notes in Computer Science 201, (Springer Verlag, Berlin, 1985).
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1991 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Meinke, K. (1991). Universal algebra in higher types. In: Ehrig, H., Jantke, K.P., Orejas, F., Reichel, H. (eds) Recent Trends in Data Type Specification. ADT 1990. Lecture Notes in Computer Science, vol 534. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-54496-8_10
Download citation
DOI: https://doi.org/10.1007/3-540-54496-8_10
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-54496-8
Online ISBN: 978-3-540-38416-8
eBook Packages: Springer Book Archive