Data Type Inference for Logic Programming | SpringerLink
Skip to main content
Springer Nature Link
Log in

Data Type Inference for Logic Programming

  • Conference paper
  • First Online:
Logic-Based Program Synthesis and Transformation (LOPSTR 2021)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 13290))

Abstract

In this paper we present a new static data type inference algorithm for logic programming. Without the need for declaring types for predicates, our algorithm is able to automatically assign types to predicates which, in most cases, correspond to the data types processed by their intended meaning. The algorithm is also able to infer types given data type definitions similar to data definitions in Haskell and, in this case, the inferred types are more informative, in general. We present the type inference algorithm, prove it is decidable and sound with respect to a type system, and, finally, we evaluate our approach on example programs that deal with different data structures.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Subscribe and save

Springer+ Basic
¥17,985 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Chapter
JPY 3498
Price includes VAT (Japan)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
JPY 6291
Price includes VAT (Japan)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
JPY 7864
Price includes VAT (Japan)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Similar content being viewed by others

Notes

  1. 1.

    This work is partially funded by the portuguese Fundação para a Ciência e a Tecnologia and by LIACC (FCT/UID/CEC/0027/2020).

  2. 2.

    Accordingly to a notion of intended meaning first presented in [Nai92].

  3. 3.

    Implementation at https://github.com/JoaoLBarbosa/TypeInferenceAlgorithm.

  4. 4.

    Type definitions will use the user friendly Prolog notation for lists instead of the list constructor.

References

  1. Barbosa, J., Florido, M., Costa, V.S.: A three-valued semantics for typed logic programming. In: Proceedings 35th International Conference on Logic Programming (Technical Communications), ICLP 2019 Technical Communications, Las Cruces, NM, USA, 20–25 September 2019. EPTCS, vol. 306, pp. 36–51 (2019)

    Google Scholar 

  2. Barbosa, J., Florido, M., Costa, V.S.: Closed types for logic programming. In: 25th International Workshop on Functional and Logic Programming (WFLP 2017) (2017)

    Google Scholar 

  3. Barbuti, R., Giacobazzi, R.: A bottom-up polymorphic type inference in logic programming. Sci. Comput. Program. 19(3), 281–313 (1992)

    Article  MathSciNet  Google Scholar 

  4. Bruynooghe, M., Janssens, G.: An instance of abstract interpretation integrating type and mode inferencing. In: 1988 Fifth International Conference and Symposium, Washington, pp. 669–683 (1988)

    Google Scholar 

  5. Charatonik, W., Podelski, A.: Directional type inference for logic programs. In: Levi, G. (ed.) SAS 1998. LNCS, vol. 1503, pp. 278–294. Springer, Heidelberg (1998). https://doi.org/10.1007/3-540-49727-7_17

    Chapter  Google Scholar 

  6. Damas, L.: Type assignment in programming languages. Ph.D. thesis, University of Edinburgh, UK (1984)

    Google Scholar 

  7. Drabent, W., Małuszyński, J., Pietrzak, P.: Locating type errors in untyped CLP programs. In: Deransart, P., Hermenegildo, M.V., Małuszynski, J. (eds.) Analysis and Visualization Tools for Constraint Programming. LNCS, vol. 1870, pp. 121–150. Springer, Heidelberg (2000). https://doi.org/10.1007/10722311_5

    Chapter  Google Scholar 

  8. Drabent, W., Małuszyński, J., Pietrzak, P.: Using parametric set constraints for locating errors in CLP programs. Theory Pract. Logic Program. 2(4–5), 549–610 (2002)

    Article  MathSciNet  Google Scholar 

  9. Dart, P.W., Zobel, J.: A regular type language for logic programs. In: Pfenning, F. (ed.) Types in Logic Programming, pp. 157–187. The MIT Press (1992)

    Google Scholar 

  10. Florido, M., Damas, L.: Types as theories. In: Proceedings of post-conference workshop on Proofs and Types, Joint International Conference and Symposium on Logic Programming (1992)

    Google Scholar 

  11. Frühwirth, T.W., Shapiro, E.Y., Vardi, M.Y., Yardeni, E.: Logic programs as types for logic programs. In: 1991 Proceedings of the Sixth Annual Symposium on Logic in Computer Science (LICS 1991), Netherlands, pp. 300–309 (1991)

    Google Scholar 

  12. Gallagher, J.P., de Waal, D.A.: Fast and precise regular approximations of logic programs. In: 1994 Logic Programming, International Conference on Logic Programming, Italy, pp. 599–613 (1994)

    Google Scholar 

  13. Hanus, M.: Polymorphic high-order programming in prolog. In: Levi, G., Martelli, M. (eds.) Logic Programming, Proceedings of the Sixth International Conference, Lisbon, Portugal, 19–23 June 1989, pp. 382–397. MIT Press (1989)

    Google Scholar 

  14. Hanus, M.: Functional logic programming: from theory to curry. In: Voronkov, A., Weidenbach, C. (eds.) Programming Logics. LNCS, vol. 7797, pp. 123–168. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-37651-1_6

    Chapter  MATH  Google Scholar 

  15. Henglein, F.: Type inference with polymorphic recursion. ACM Trans. Program. Lang. Syst. 15(2), 253–289 (1993)

    Article  Google Scholar 

  16. Heintze, N., Jaffar, J.: Semantic types for logic programs. In: Pfenning, F. (ed.) Types in Logic Programming, pp. 141–155. The MIT Press (1992)

    Google Scholar 

  17. Hill, P.M., Lloyd, J.W.: The Gödel Programming Language. MIT Press, Cambridge (1994)

    MATH  Google Scholar 

  18. Lakshman, T.L., Reddy, U.S.: Typed Prolog: a semantic reconstruction of the Mycroft-O’Keefe type system. In Logic Programming, Proceedings of the 1991 International Symposium, San Diego, California, USA (1991)

    Google Scholar 

  19. Lunjin, L.: On Dart-Zobel algorithm for testing regular type inclusion. SIGPLAN Not. 36(9), 81–85 (2001)

    Article  Google Scholar 

  20. Maher, M.: Complete axiomatizations of the algebras of finite, rational and infinite trees. In: Proceedings Third Annual Symposium on Logic in Computer Science, Los Alamitos, CA, USA, pp. 348–357. IEEE Computer Society, July 1988

    Google Scholar 

  21. Mishra, P.: Towards a theory of types in Prolog. In: Proceedings of the 1984 International Symposium on Logic Programming, Atlantic City, New Jersey, USA, 6–9 February 1984, pp. 289–298. IEEE-CS (1984)

    Google Scholar 

  22. Mycroft, A., O’Keefe, R.A.: A polymorphic type system for Prolog. Artif. Intell. 23(3), 295–307 (1984)

    Article  MathSciNet  Google Scholar 

  23. Naish, L.: Types and the intended meaning of logic programs. In: Pfenning, F. (ed.) Types in Logic Programming, pp. 189–216. The MIT Press (1992)

    Google Scholar 

  24. Pietrzak, P., Correas, J., Puebla, G., Hermenegildo, M.V.: A practical type analysis for verification of modular Prolog programs. In: Proceedings of the ACM SIGPLAN Symposium on Partial Evaluation and Semantics-Based Program Manipulation, pp. 61–70, January 2008

    Google Scholar 

  25. Pyo, C., Reddy, U.S.: Inference of polymorphic types for logic programs. In: 1989 Proceedings of the North American Conference on Logic Programming, USA, 2 Volumes, pp. 1115–1132 (1989)

    Google Scholar 

  26. Schrijvers, T., Bruynooghe, M., Gallagher, J.P.: From monomorphic to polymorphic well-typings and beyond. In: Hanus, M. (ed.) LOPSTR 2008. LNCS, vol. 5438, pp. 152–167. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-00515-2_11

    Chapter  MATH  Google Scholar 

  27. Schrijvers, T., Santos Costa, V., Wielemaker, J., Demoen, B.: Towards typed Prolog. In: Garcia de la Banda, M., Pontelli, E. (eds.) ICLP 2008. LNCS, vol. 5366, pp. 693–697. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-89982-2_59

    Chapter  Google Scholar 

  28. Sağlam, H., Gallagher, J.P.: Approximating constraint logic programs using polymorphic types and regular descriptions. In: Hermenegildo, M., Swierstra, S.D. (eds.) Programming Languages: Implementations, Logics and Programs, pp. 461–462. Springer, Heidelberg (1995)

    Chapter  Google Scholar 

  29. Somogyi, Z., Henderson, F., Conway, T.C.: The execution algorithm of Mercury, an efficient purely declarative logic programming language. J. Log. Program. 29(1–3), 17–64 (1996)

    Article  Google Scholar 

  30. Talbot, J.M., Tison, S., Devienne, P.: Set-based analysis for logic programming and tree automata. In: Van Hentenryck, P. (ed.) SAS 1997. LNCS, vol. 1302, pp. 127–140. Springer, Heidelberg (1997). https://doi.org/10.1007/BFb0032738

    Chapter  Google Scholar 

  31. Ullman, J.D.: Principles of Database and Knowledge-Base Systems, Computer Science Press Inc. (1988)

    Google Scholar 

  32. Vaucheret, C., Bueno, F.: More precise yet efficient type inference for logic programs. In: Hermenegildo, M.V., Puebla, G. (eds.) SAS 2002. LNCS, vol. 2477, pp. 102–116. Springer, Heidelberg (2002). https://doi.org/10.1007/3-540-45789-5_10

    Chapter  Google Scholar 

  33. Van Roy, P.L.: Can logic programming execute as fast as imperative programming? Ph.D. thesis, EECS Department, University of California, Berkeley, November 1990

    Google Scholar 

  34. Yardeni, E., Frühwirth, T.W., Shapiro, E.: Polymorphically typed logic programs. In: Pfenning, F. (ed.) Types in Logic Programming, pp. 63–90. The MIT Press (1992)

    Google Scholar 

  35. Zobel, J.: Derivation of polymorphic types for Prolog programs. In: 1987 Proceedings of the Fourth International Conference on Logic Programming, Melbourne (1987)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Faculdade de Ciências, Universidade do Porto, Porto, Portugal

    João Barbosa, Mário Florido & Vítor Santos Costa

Authors
  1. João Barbosa
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Mário Florido
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Vítor Santos Costa
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to João Barbosa .

Editor information

Editors and Affiliations

  1. IASI-CNR, Rome, Italy

    Emanuele De Angelis

  2. University of Namur, Namur, Belgium

    Wim Vanhoof

Rights and permissions

Reprints and permissions

Copyright information

© 2022 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Barbosa, J., Florido, M., Costa, V.S. (2022). Data Type Inference for Logic Programming. In: De Angelis, E., Vanhoof, W. (eds) Logic-Based Program Synthesis and Transformation. LOPSTR 2021. Lecture Notes in Computer Science, vol 13290. Springer, Cham. https://doi.org/10.1007/978-3-030-98869-2_2

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-98869-2_2

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-98868-5

  • Online ISBN: 978-3-030-98869-2

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics