Abstract
I have described a syntactic calculus of partially ordered structures and its application to computation. A syntax of record-like terms and a "type subsumption" ordering were defined and shown to form a lattice structure. A simple "type-as-set" interpretation of these term structures extends this lattice to a distributive one, and in the case of finitary terms, to a complete Brouwerian lattice. As a result, a method for solving systems of type equations by iterated rewriting of type symbols was proposed which defines an operational semantics for KBL — a Knowledge Base Language. It was shown that a KBL program can be seen as a system of equations. Thanks to the lattice properties of finite structures, a system of equations admits a least fixed-point solution. The particular order of computation of KBL, the "fan-out computation order", which rewrites symbols closer to the root first was formally defined and shown to be maximal. Unfortunately, the complete "correctness" of KBL is not yet established. That is, it is not known at this point whether the normal form of a term is equal to the fixed-point solution. However, as steps in this direction, two technical lemmas were conjectured to which a proof of the correctness is corollary.
Research described in this paper was done while the author was at the University of Pennsylvania, Philadelphia.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
Ait-Kaci, H. A Lattice Theoretic Approach to Computation Based on a Calculus of Partially Ordered Type Structures. PhD thesis, Computer and Information Science, University of Pennsylvania, 1984.
Berry, G., and Levy, J.J. Minimal and Optimal Computations of Recursive Programs. Journal of the ACM 26:148–75, 1979.
Birkhoff, G. Colloquium Publications. Volume 25: Lattice Theory. American Mathematical Society, Providence, RI, 1940. Third (revised) edition, 1979.
Borkin, S.A. Series in Computer Science. Volume 4: Data Models: A Semantic Approach for Database Systems. The M.I.T. Press, Cambridge, MA, 1980.
Brachman, R.J. A New Paradigm for Representing Knowledge. BBN Report 3605, Bolt Beranek and Newman, Cambridge, MA, 1978.
Brachman, R.J. What IS-A Is and Isn't: An Analysis of Taxonomic Links in Semantic Networks. Computer 16(10):30–35, October 1983.
Brouwer, L.E.J. On Order in the Continuum, and the Relation of Truth to Non-Contradictority. In Proceedings of the Section of Sciences 54, pages 357–358. Koninklijke Nederlandse Akademie Van Wetenschappen, 1951. Series A, Mathematical Sciences.
Courcelle, B. Fundamental Properties of Infinite Trees. Theoretical Computer Science 25:95–169, 1983.
Courcelle, B., and Nivat, M. The Algebraic Semantics of Recursive Program Schemes. In J. Winkowski (editor), Mathematical Foundations of Computer Science Proceedings, pages 16–30. Springer-Verlag, Berlin, W.Germany, 1978. Lecture Notes in Computer Science 64.
Dummett, M. Elements of Intuitionism. Oxford University Press, Oxford, UK, 1977.
Goguen, J.A., and Tardo, J.J. An Introduction to OBJ: a Language for Writing and Testing Formal Algebraic Program Specifications. In Proceedings of the IEEE Conference on Specifications of Reliable Software, pages 170–189. Cambridge, MA, 1979.
Gorn, S. Explicit Definitions and Linguistic Dominoes. In J.F. Hart and S. Takasu (editors), Systems and Computer Science, pages 77–105. University of Toronto Press, Toronto, Ontario, 1965.
Gorn, S. Data Representation and Lexical Calculi. Information Processing & Management 20(1–2):151–174, 1984. Also available as technical report MS-CIS-82-39, Department of Computer and Information Science, University of Pennsylvania, Philadelphia, PA.
Guessarian, I. Lecture Notes in Computer Science. Volume 99: Algebraic Semantics. Springer-Verlag, Berlin, W.Germany, 1981.
Huet, G. Resolution d'Equations dans des Langages d'Ordre 1, 2, ..., ω. PhD thesis, Universite de Paris VII, France, September, 1976.
Nivat, M. On the Interpretation of Recursive Polyadic Program Schemes. In Symposia Mathematica, pages 225–81. Istituto Nazionale di Alta Mathematica, Rome, Italy, 1975.
Plotkin, G.D. A Powerdomain Construction. SIAM Journal on Computing 5, 1976.
Plotkin, G.D. Lattice Theoretic Properties of Subsumption. Memorandum MIP-R-77, Department of Machine Intelligence and Perception, University of Edinburgh, June, 1977.
Reynolds, J.C. Transformational Systems and the Algebraic Structure of Atomic Formulas. In D. Michie (editor), Machine Intelligence 5, chapter 7. Edinburgh University Press, 1970.
Robinson, J.A. A Machine-Oriented Logic Based on the Resolution Principle. Journal of the ACM 12(1):23–41, 1965.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1985 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Ait-Kaci, H. (1985). Solving type equations by graph rewriting. In: Jouannaud, JP. (eds) Rewriting Techniques and Applications. RTA 1985. Lecture Notes in Computer Science, vol 202. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-15976-2_8
Download citation
DOI: https://doi.org/10.1007/3-540-15976-2_8
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-15976-6
Online ISBN: 978-3-540-39679-6
eBook Packages: Springer Book Archive