Directional Type Checking for Logic Programs: Beyond Discriminative Types

  • Witold Charatonik
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1782)


Directional types form a type system for logic programs which is based on the view of a predicate as a directional procedure which, when applied to a tuple of input terms, generates a tuple of output terms. It is known that directional-type checking wrt. arbitrary types is undecidable; several authors proved decidability of the problem wrt. discriminative regular types. In this paper, using techniques based on tree automata, we show that directional-type checking for logic programs wrt. general regular types is Dexptime-complete and fixed-parameter linear. The latter result shows that despite the exponential lower bound, the type system might be usable in practice.


types in logic programming directional types regular types tree automata 


  1. 1.
    A. Aiken and T. K. Lakshman. Directional type checking of logic programs. In B. L. Charlier, editor, 1st International Symposium on Static Analysis, volume 864 of Lecture Notes in Computer Science, pages 43–60, Namur, Belgium, Sept. 1994. Springer Verlag.Google Scholar
  2. 2.
    K. R. Apt. Declarative programming in Prolog. In D. Miller, editor, Logic Programming-Proceedings of the 1993 International Symposium, pages 12–35, Vancouver, Canada, 1993. The MIT Press.Google Scholar
  3. 3.
    K. R. Apt. Program verification and Prolog. In E. Börger, editor, Specification and Validation methods for Programming languages and systems, pages 55–95. Oxford University Press, 1995.Google Scholar
  4. 4.
    K. R. Apt and S. Etalle. On the unification free Prolog programs. In A. M. Borzyszkowski and S. Sokolowski, editors, Mathematical Foundations of Computer Science 1993, 18th International Symposium, volume 711 of LNCS, pages 1–19, Gdansk, Poland, 30 Aug.–3 Sept. 1993. Springer.Google Scholar
  5. 5.
    J. Boye. Directional Types in Logic Programming. PhD thesis, Department of Computer and Information Science, Linköping University, 1996.Google Scholar
  6. 6.
    J. Boye and J. Maluszynski. Two aspects of directional types. In L. Sterling, editor, Proceedings of the 12th International Conference on Logic Programming, pages 747–764, Cambridge, June 13–18 1995. MIT Press.Google Scholar
  7. 7.
    J. Boye and J. Maluszynski. Directional types and the annotation method. Journal of Logic Programming, 33(3):179–220, Dec. 1997.zbMATHCrossRefMathSciNetGoogle Scholar
  8. 8.
    F. Bronsard, T. K. Lakshman, and U. S. Reddy. A framework of directionality for proving termination of logic programs. In K. Apt, editor, Proceedings of the Joint International Conference and Symposium on Logic Programming, pages 321–335, Washington, USA, 1992. The MIT Press.Google Scholar
  9. 9.
    A. Caron, J. Coquidé, and M. Dauchet. Encompassment properties and automata with constraints. In C. Kirchner, editor, 5th international conference on Rewriting Techniques and Applications, LNCS 690, pages 328–342, Montréal, 1993.Google Scholar
  10. 10.
    W. Charatonik. Automata on DAG representations of finite trees. Technical Report MPI-I-1999-2-001, Max-Planck-Institut für Informatik, Mar. 1999. Scholar
  11. 11.
    W. Charatonik, F. Jacquemard, and A. Podelski. Directional type checking for logic programs is decidable, 1998. Unpublished note.Google Scholar
  12. 12.
    W. Charatonik and A. Podelski. Directional type inference for logic programs. In G. Levi, editor, Proceedings of the Fifth International Static Analysis Symposium (SAS), LNCS 1503, pages 278–294, Pisa, Italy, 1998. Springer-Verlag.Google Scholar
  13. 13.
    W. Charatonik and A. Podelski. Set-based analysis of reactive infinite-state systems. In B. Steffen, editor, Fourth International Conference on Tools and Algorithms for the Construction and Analysis of Systems, LNCS 1384, pages 358–375, Lisbon, Portugal, March–April 1998. Springer-Verlag.CrossRefGoogle Scholar
  14. 14.
    W. Charatonik, A. Podelski, and J.-M. Talbot. Paths vs. trees in set-based program analysis. In 27th Annual ACM Symposium on Principles of Programming Languages, Jan. 2000.Google Scholar
  15. 15.
    H. Comon, M. Dauchet, R. Gilleron, F. Jacquemard, D. Lugiez, S. Tison, and M. Tommasi. Tree automata techniques and applications. Scholar
  16. 16.
    P. Dart and J. Zobel. A regular type language for logic programs. In F. Pfenning, editor, Types in Logic Programming, pages 157–189. MIT Press, 1992.Google Scholar
  17. 17.
    P. Devienne, J.-M. Talbot, and S. Tison. Set-based analysis for logic programming and tree automata. In Proceedings of the Static Analysis Symposium, SAS’97, volume 1302 of LNCS, pages 127–140. Springer-Verlag, 1997.Google Scholar
  18. 18.
    R. G. Downey and M. Fellows. Parameterized complexity. Monographs in computer science. Springer, New York, 1999.Google Scholar
  19. 19.
    T. Frühwirth, E. Shapiro, M. Vardi, and E. Yardeni. Logic programs as types for logic programs. In Sixth Annual IEEE Symposium on Logic in Computer Science, pages 300–309, July 1991.Google Scholar
  20. 20.
    J. Gallagher and D. A. de Waal. Regular approximations of logic programs and their uses. Technical Report CSTR-92-06, Department of Computer Science, University of Bristol, 1992.Google Scholar
  21. 21.
    J. Gallagher and D. A. de Waal. Fast and precise regular approximations of logic programs. In P. V. Hentenryck, editor, Proceedings of the Eleventh International Conference on Logic Programming, pages 599–613, Santa Margherita Ligure, Italy, 1994. The MIT Press.Google Scholar
  22. 22.
    F. Gécseg and M. Steinby. Tree Automata. Akademiai Kiado, 1984.Google Scholar
  23. 23.
    G. Gottlob, E. Grädel, and H. Veith. Datalog LITE: Temporal versus deductive reasoning in verification. Technical Report DBAI-TR-98-22, Institut für Informationssysteme, Technische Universität Wien, December 1998.Google Scholar
  24. 24.
    N. Heintze. Set based program analysis. PhD thesis, School of Computer Science, Carnegie Mellon University, 1992.Google Scholar
  25. 25.
    N. Heintze and J. Jaffar. A finite presentation theorem for approximating logic programs. In Seventeenth Annual ACM Symposium on Principles of Programming Languages, pages 197–209, January 1990.Google Scholar
  26. 26.
    N. Heintze and J. Jaffar. Semantic types for logic programs. In F. Pfenning, editor, Types in Logic Programming, pages 141–156. MIT Press, 1992.Google Scholar
  27. 27.
    F. Henglein. Type inference with polymorphic recursion. Transactions on Programming Languages and Systems, 15(2):253–289, 1993.CrossRefGoogle Scholar
  28. 28.
    P. V. Hentenryck, A. Cortesi, and B. L. Charlier. Type analysis of Prolog using type graphs. Journal of Logic Programming, 22(3):179–209, Mar. 1995.zbMATHCrossRefGoogle Scholar
  29. 29.
    G. Janssens and M. Bruynooghe. Deriving descriptions of possible values of program variables by means of abstract interpretation. Journal of Logic Programming, 13(2–3):205–258, July 1992.zbMATHCrossRefMathSciNetGoogle Scholar
  30. 30.
    P. Mishra. Towards a theory of types in Prolog. In IEEE International Symposium on Logic Programming, pages 289–298, 1984.Google Scholar
  31. 31.
    A. Mycroft and R. A. O’Keefe. A polymorphic type system for Prolog. Artificial Intelligence, 23:295–307, 1984.zbMATHCrossRefMathSciNetGoogle Scholar
  32. 32.
    L. Naish. A declarative view of modes. In Proceedings of the 1996 Joint International Conference and Symposium on Logic Programming, pages 185–199. MIT Press, September 1996.Google Scholar
  33. 33.
    F. Pfenning, editor. Types in Logic Programming. MIT Press, 1992.Google Scholar
  34. 34.
    Y. Ramakrishna, C. Ramakrishnan, I. Ramakrishnan, S. Smolka, T. Swift, and D. Warren. Efficient model checking using tabled resolution. In Computer Aided Verification (CAV’97), LNCS 1254. Springer-Verlag, June 1997.Google Scholar
  35. 35.
    Y. Rouzaud and L. Nguyen-Phuong. Integrating modes and subtypes into a Prolog type-checker. In K. Apt, editor, Proceedings of the Joint International Conference and Symposium on Logic Programming, pages 85–97, Washington, USA, 1992. The MIT Press.Google Scholar
  36. 36.
    P. Rychlikowski and T. Truderung. Polymorphic directional types for logic programming., 2000.
  37. 37.
    H. Seidl. Haskell overloading is DEXPTIME-complete. Information Processing Letters, 52:57–60, 1994.zbMATHCrossRefMathSciNetGoogle Scholar
  38. 38.
    W. Thomas. Handbook of Theoretical Computer Science, volume B, chapter Automata on Infinite Objects, pages 134–191. Elsevier, 1990.Google Scholar
  39. 39.
    E. Yardeni and E. Shapiro. A type system for logic programs. Journal of Logic Programming, 10:125–153, 1991.CrossRefzbMATHMathSciNetGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2000

Authors and Affiliations

  • Witold Charatonik
    • 1
    • 2
  1. 1.Max-Planck-Institut für InformatikSaarbrückenGermany
  2. 2.University of WrocławPoland

Personalised recommendations