Defining soft sortedness by abstract interpretation
Sorted languages can improve the expressiveness and efficiency of reasoning. A conventional sorted language typically includes well-sortedness rules amongst the rules for well-formedness. A major disadvantage of this approach is that many intuitively meaningful expressions are ill-sorted and hence not part of the language.
To overcome this limitation, soft sorting regards as well-formed, all first-order expressions of the corresponding unsorted language, and lets the semantics be the basis for defining the significance of the sort syntax. In this paper we show how soft sortedness can be defined by abstract interpretations which characterise semantic properties of softly sorted expressions.
KeywordsLogic Program Abstract Interpretation Predicate Symbol Domain Universe Soft Typing
Unable to display preview. Download preview PDF.
- 1.Abramsky, S. and Hankin, C. (eds.), Abstract Interpretation of Declarative Languages, Ellis Horwood, 1987.Google Scholar
- 2.Cartwright, R. and M. Fagan, “Soft Typing”, in Proceedings of the ACM SIG-PLAN'91 Conference on Programming Language Design and Implementation, pages 278–292, 1991.Google Scholar
- 3.Chen, J., “Soft Sorting: Integrating Static and Dynamic Sort Checking”, PhD thesis, Department of Computer Science, The University of Queensland, Australia, 1992.Google Scholar
- 4.Chen, J. and J. Staples, “Soft Sorting in Logic Programming”, in Proceedings of ALPUK'92, Springer-Verlag, pages 79–96, 1992.Google Scholar
- 5.Cohn, A. G., “A More Expressive Formulation of Many Sorted Logic”, JAR 3(1987) 113–200.Google Scholar
- 6.Comon, H., “Disunification: A Survey”, in Computational Logic: Essays in Honor of Alan Robinson, Lassez, J.-L. and Plotkin, G. (eds.), The MIT Press, 1991, 322–359.Google Scholar
- 7.Enderton, H. B., A Mathematical Introduction to Logic, Academic Press, 1972.Google Scholar
- 8.Henglein, F., “Dynamic Typing”, in Proceedings of the 4th European Symposium on Programming (ESOP '92), pages 233–253, LNCS 582, Springer-Verlag, 1992.Google Scholar
- 9.Hill, P. M. and R. W. Topor, “A Semantics for Typed Logic Programs”, in Pfenning, F., (ed.), Types in Logic Programming, The MIT Press, pages 1–62, 1992.Google Scholar
- 10.Kifer, M. and J. Wu, “A First-Order Theory of Typed and Polymorphism in Logic Programming”, in Proceedings of LICS '91, pages 310–321, 1991.Google Scholar
- 11.Lassez, J.-L., M. J. Maher and K. Marriott, “Unification Revisited”, in Foundations of Deductive Databases and Logic Programming, Minker, J. (ed.), Morgan Kaufmann Publishers, pages 587–625, 1988.Google Scholar
- 12.Lloyd, J. W., Foundations of Logic Programming, Springer-Verlag, 1987.Google Scholar
- 13.Mycroft, A. and R. A. O'Keefe, “A Polymorphic Type System for Prolog”, Artificial Intelligence 23, 295–307, 1984.Google Scholar