Abstract
Languages that distinguish between types and structures use explicit components for the carrier type(s) in structures. Examples are the functional language Standard ML and most algebraic specification systems. Hence, they have to use general sum types or signatures to give types to structures and to be able to build, for instance, the algebraic hierarchy.
Furthermore, in most languages the modelling of properties that the elements of a signature — the structures — should fulfill is not possible or computationally not relevant. This is a major drawback, especially in a computer algebra environment.
This paper presents a calculus for building signatures with explicit type components which are needed for modelling many-sorted structures and structures of the same signature with identical carriers. Additionally, we provide the possibility of using propositions as components needed for modelling the properties of structures. Propositions, which are distinguished from booleans, are inhabited by their proofs and hence, they are types themselves. This idea stems from the “propositions as types” principle known from constructive logic and results in a coherent treatment of carrier types, operations and their properties. It allows us to express theories (specifications) while staying within the framework of signatures.
The framework is used for the construction of function spaces between types with equality and the building of some parts of the algebraic hierarchy.
Research supported by the Swiss National Science Foundation.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
K. Abdali, G. Cherry, and N. Soiffer. An Object Oriented Approach to Algebra System Design. In Symposium on symbolic and algebraic manipulation, pages 24–30. ACM, 1986.
R.M. Burstall and B. Lampson. A Kernel Language for Abstract Data Types and Modules. In Semantics of Data Types, volume 173 of Lecture Notes in Computer Science, pages 1–50. Springer Verlag, 1988.
J. Calmet and I. Tjandra. A Unified-Algebra-based Specification Language for Symbolic Computing. In Design and Implementation of Symbolic Computation Systems (Proceedings of DISCO '93), volume 722 of Lecture Notes in Computer Science, pages 122–133. Springer Verlag, 1993.
L. Cardelli. A Polymorphic λ-calculus with Type:Type. Technical Report 10, DEC Systems Research Center, 1986.
L. Cardelli. Typeful Programming. Technical Report 45, DEC Systems Research Center, 1989.
L. Cardelli and J.C. Mitchell. Operations on Records. Mathematical Structures in Computer Science, 1(1):3–48, 1991.
R.L. Constable et al. Implementing mathematics with the Nuprl proof development system. Prentice-Hall, 1986.
T. Coquand et al. The Calculus of Constructions. Technical report, INRIA, 1989.
S. Dalmas. A polymorphic functional language applied to symbolic computation. In ISSAC, 1992.
W.M. Farmer, J.D. Guttman, and F.J. Thayer. IMPS User's Manual. The MITRE Corporation, September 1993.
Joseph A. Goguen. Types as theories. In Topology and category theory in computer science, pages 357–390. Oxford science publications, 1991.
Joseph A. Goguen et al. Introducing OBJ. Technical report, SRI International, March 1992.
W.A. Howard. The formulae-as-types notion of constructions. In to H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism. Academic Press, 1980.
P.R. Hudak et al. Report on the programming language Haskell, a non-strict purely functional language, Version 1.2. ACM SIGPLAN Notices, 1992.
Richard D. Jenks and Robert S. Sutor. Axiom: The Scientific Computation System. Springer, 1992.
Serge Lang. Algebra. Addison-Wesley, 2nd edition, 1984.
Robin Milner, Mads Thorpe, and Robert Harper. The Definition of Standard ML. The MIT Press, 1990.
Stephan A. Missura. Combining Forgetful Functors with Coercions. Unpublished Manuscript, 1993.
Stephan A. Missura. Extending AlgBench with a type system. In Design and Implementation of Symbolic Computation Systems (Proceedings of DISCO '93), volume 722 of Lecture Notes in Computer Science. Springer Verlag, 1993.
J. Mitchell and R. Harper. The Essence of ML. In Conference Record of ACM Symposium on Principles of Programming Languages, pages 28–46, 1988.
John Mitchell, Sigurd Meldal, and Neel Madhav. An extension of Standard ML modules with subtyping and inheritance. In Conference Record of the ACM Sym-posium on Principles of Programming Languages, pages 270–278, 1991.
M.J. Beeson. Foundations of Constructive Mathematics. Springer-Verlag, 1985.
Bengt Nordström, Kent Petersson, and Jan M. Smith. Programming in Martin-Löf's Type Theory. Oxford Science Publications, 1990.
Lawrence C. Paulson. Introduction to Isabelle. Technical report, Computer Laboratory, University of Cambridge, 1993.
D. Sannella. Formal program development in Extended ML for the working programmer. Technical report, Laboratory for Foundations of Computer Science, University of Edinburgh, December 1989.
R. Turner. Constructive Foundations for Functional Languages. McGraw-Hill, 1991.
Jan van Leeuwen, editor. Formal Models and Semantics, volume B of Handbook of Theoretical Computer Science. Elsevier, 1990.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1995 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Missura, S.A. (1995). Theories = signatures + propositions used as types. In: Calmet, J., Campbell, J.A. (eds) Integrating Symbolic Mathematical Computation and Artificial Intelligence. AISMC 1994. Lecture Notes in Computer Science, vol 958. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-60156-2_11
Download citation
DOI: https://doi.org/10.1007/3-540-60156-2_11
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-60156-2
Online ISBN: 978-3-540-49533-8
eBook Packages: Springer Book Archive