Abstract
The syntax and semantics of a new kind of a type system are described and type unification is discussed. Special algebraic structures are used for the semantics. The universe of such a structure consists of ground data terms (for the representation of the ground objects) and of ground type terms (for the representation of the types). A binary function ”:” is used to determine the elements belonging to a type. This function is defined by special rewrite rules called type rules. The main aim of this approach is computing with types. The elements of a type can be generated by using the type rules. The type unification can generate the elements belonging to the intersection of two types.
Preview
Unable to display preview. Download preview PDF.
References
Ait-Kaci,H., and R.Nasr: LOGIN: A Logic Programming Language with Built-In Inheritance. J. Logic Programming 3 (1986), 185–215.
Beierle,C.: Types, Modules and Databases in the Logic Programming Language PROTOS-L. In [3], 73–110.
Bläsius,K.H., U.Hedtstück, and C.-R. Rollinger (Eds.): Sorts and Types in Artificial Intelligence. LNAI 418, Springer-Verlag, 1990.
DeGroot,D., and G.Lindstrom (eds.): Logic Programming. Functions, Relations and Equations. Prentice-Hall, Englewood Cliffs (New Jersey) 1986.
Furbach,U., and S.Hölldobler: Equations, Order-Sortedness and Inheritance in Logic Programming. Technical Report, FKI-110-89, TU München 1989.
Furbach,U.: Logische und Funktionale Programmierung. Grundlagen einer Kombination. Vieweg Verlag, Braunschweig 1991.
Genesereth,M.R., and N.J.Nilsson: Logical Foundations of Artificial Intelligence. Morgan Kaufmann Publ., Los Altos 1987.
Goltz,H.-J.: Functional Data Term Models and Semantic Unification. In: [12], 158–167.
Goltz,H.-J., and H.Herre: Grundlagen der logischen Programmierung. Akademie Verlag, Berlin 1990.
Goltz,H.-J.: Functional Extension of Logic Programming. In: U.Geske and D.Koch: Contributions to Artificial Intelligence. Research in Informatics vol. 1, Akademie Verlag, Berlin 1991, 55–73.
Goltz,H.-J.: Ein praktischer Algorithmus für die E-Unifikation. IWBS-Report 166, IBM Stuttgart 1991.
Grabowski,J., P.Lescanne, and W.Wechler (eds.): Algebraic and Logic Programming. Akademie-Verlag Berlin 1988 (also Lecture Notes in Computer Sciences 343, Springer-Verlag, Berlin, Heidelberg, New York, Tokyo 1988).
Hanus,M.: Parametric Order-Sorted Types in Logic Programming. In: Proceedings of the TAPSOFT'91, LNCS 494, Springer-Verlag, 1991, 181–200.
Hanus,M.: Logic Programming with Type Specifications. To appear in: F.Pfenning (ed.), Types in Logic Programming, MIT Press, 1992.
Hölldobler,S.: Foundations in Equational Logic Programming. LNCS 353, Springer-Verlag, 1989.
Huet,G., and D.Oppen: Equations and Rewrite Rules: A Survey. In: R.Book (ed.), Formal Language Theory: Perspectives and Open Problems, Academic Press, New York, London 1980, 349–405.
Jouannaud,J.-P., C.Kirchner, H.Kirchner, and A.Megrelis: OBJ: Programming with Equalities, Subsorts, Overloading and Parameterization. In:[12], 41–52.
Lakshman,T.K. and U.S.Reddy: Typed Prolog: A Semantic Reconstruction of the Mycroft-O'Keefe Type System. In: V.Saraswat, K.Ueda (eds.), Logic Programming, Proc. Int. Symposium 1991, MIT Press, 1991, 201–217.
Lloyd,J.W.: Foundations of Logic Programming. 2.Ed., Springer-Verlag, Berlin, Heidelberg, New York, Tokyo 1987.
Martelli,A., and U.Montanari: An Efficient Unification Algorithm. ACM Transactions on Programming Languages and Systems 4 (1982), 258–282.
Montini,G.: Efficiency Considarations on Built-in Taxonomic Reasoning in Prolog. In: Proc. Int. Joint Conf. Artificial Intelligence 1987, 68–75.
Mycroft,A., and R.A.O'Keefe: A Polymorphic Type System for Prolog. Artificial Intelligence 23 (1984), 295–307.
Shin,D.W., J.H.Nang, S.R.Maeng, and J.W.Cho: A Typed Functional Extension of Logic Programming. Journal New Generation Computing 10 (1992), 197–221.
Smolka,S., W.Nutt, J.A.Goguen, and J.Meseguer: Order-Sorted Equational Computation. SEKI-Report SR-87-14, FB Informatik, Universität Kaiserslautern, 1987.
Smolka,G.: Logic Programming with Polymorphicaly Order-Sorted Types. In:[12], 53–70.
Walther,C.: A Many-sorted Calculus Based on Resolution and Paramodulation. Research Notes in Artificial Intelligence, Pitman and Morgan Kaufman Publ., London; Morgan Kaufmann Publ., Los Altos (Calif.) 1987.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1992 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Goltz, HJ. (1992). A constructive type system based on data terms. In: Pearce, D., Wagner, G. (eds) Logics in AI. JELIA 1992. Lecture Notes in Computer Science, vol 633. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0023434
Download citation
DOI: https://doi.org/10.1007/BFb0023434
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-55887-3
Online ISBN: 978-3-540-47304-6
eBook Packages: Springer Book Archive