Abstract
We show how to transform a set of regular type definitions into a finite pre-interpretation for a logic program. The derived pre-interpretation forms the basis for an abstract interpretation. The core of the transformation is a determinization procedure for non-deterministic finite tree automata. This approach provides a flexible and practical way of building program-specific analysis domains. We argue that the constructed domains are condensing: thus goal-independent analysis over the constructed domains loses no precision compared to goal-dependent analysis. We also show how instantiation modes such as ground, variable and non-variable can be expressed as regular types and hence integrated with other regular types. We highlight applications in binding time analysis for offline partial evaluation and infinite-state model checking. Experimental results and a discussion of complexity are included.
Work supported in part by European Framework 5 Project ASAP (IST-2001-38059), and the IT-University of Copenhagen.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Frühwirth, T., Shapiro, E., Vardi, M., Yardeni, E.: Logic programs as types for logic programs. In: Proceedings of the IEEE Symposium on Logic in Computer Science, Amsterdam (1991)
Mishra, P.: Towards a theory of types in Prolog. In: Proceedings of the IEEE International Symposium on Logic Programming (1984)
Yardeni, E., Shapiro, E.: A type system for logic programs. Journal of Logic Programming 10(2), 125–154 (1990)
Comon, H., Dauchet, M., Gilleron, R., Jacquemard, F., Lugiez, D., Tison, S., Tommasi, M.: Tree Automata Techniques and Applications (1999), http://www.grappa.univlille3.fr/tata
Boulanger, D., Bruynooghe, M., Denecker, M.: Abstracting s-semantics using a model-theoretic approach. In: Penjam, J. (ed.) PLILP 1994. LNCS, vol. 844, pp. 432–446. Springer, Heidelberg (1994)
Boulanger, D., Bruynooghe, M.: A systematic construction of abstract domains. In: LeCharlier, B. (ed.) SAS 1994. LNCS, vol. 864, pp. 61–77. Springer, Heidelberg (1994)
Gallagher, J., Boulanger, D., Sağlam, H.: Practical model-based static analysis for definite logic programs. In: Lloyd, J.W. (ed.) Proc. of International Logic Programming Symposium, pp. 351–365. MIT Press, Cambridge (1995)
Lloyd, J.: Foundations of Logic Programming, 2nd edn. Springer, Heidelberg (1987)
Clark, K.: Predicate logic as a computational formalism. Technical Report DOC 79/59, Imperial College, London, Department of Computing (1979)
Marriott, K., Søndergaard, H.: Bottom-up abstract interpretation of logic programs. In: Proceedings of the Fifth International Conference and Symposium on Logic Programming, Washington (1988)
Leuschel, M., Jørgensen, J.: Efficient specialisation in Prolog using the handwritten compiler generator LOGEN. Elec. Notes Theor. Comp. Sci, vol. 30(2) (1999)
Codish, M., Demoen, B.: Analysing logic programs using “Prop”-ositional logic programs and a magic wand. In: Miller, D. (ed.) Proceedings of the 1993 International Symposium on Logic Programming, Vancouver, MIT Press, Cambridge (1993)
Roychoudhury, A., Kumar, K.N., Ramakrishnan, C.R., Ramakrishnan, I.V., Smolka, S.A.: Verification of parameterized systems using logic program transformations. In: Schwartzbach, M.I., Graf, S. (eds.) TACAS 2000. LNCS, vol. 1785, pp. 172–187. Springer, Heidelberg (2000)
Charatonik, W.: Directional type checking for logic programs: Beyond discriminative types. In: Smolka, G. (ed.) ESOP 2000. LNCS, vol. 1782, pp. 72–87. Springer, Heidelberg (2000)
Debray, S., Warren, D.: Automatic mode inference for logic programs. Journal of Logic Programming 5(3), 207–229 (1988)
Tarjan, R.: Depth-first search and linear graph algorithms. SIAM Journal of Computing 1(2), 146–160 (1972)
Ullman, J.: Implementation of Logical Query Languages for Databases. ACM Transactions on Database Systems 10(3) (1985)
Schachte, P.: Precise and Efficient Static Analysis of Logic Programs. PhD thesis, Dept. of Computer Science, The University of Melbourne, Australia (1999)
Howe, J.M., King, A.: Positive Boolean Functions as Multiheaded Clauses. In: Codognet, P. (ed.) ICLP 2001. LNCS, vol. 2237, pp. 120–134. Springer, Heidelberg (2001)
Bruynooghe, M., Janssens, G.: An instance of abstract interpretation integrating type and mode inferencing. In: Kowalski, R., Bowen, K. (eds.) Proceedings of ICLP/SLP, pp. 669–683. MIT Press, Cambridge (1988)
Horiuchi, K., Kanamori, T.: Polymorphic type inference in prolog by abstract interpretation. In: Furukawa, K., Fujisaki, T., Tanaka, H. (eds.) Logic Programming 1987. LNCS, vol. 315, pp. 195–214. Springer, Heidelberg (1988)
Codish, M., Demoen, B.: Deriving type dependencies for logic programs using multiple incarnations of Prop. In: LeCharlier, B. (ed.) SAS 1994. LNCS, vol. 864, pp. 281–296. Springer, Heidelberg (1994)
Codish, M., Lagoon, V.: Type dependencies for logic programs using ACIunification. Theoretical Computer Science 238(1-2), 131–159 (2000)
Marriott, K., Søndergaard, H.: Precise and efficient groundness analysis for logic programs. LOPLAS 2(1-4), 181–196 (1993)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2004 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Gallagher, J.P., Henriksen, K.S. (2004). Abstract Domains Based on Regular Types. In: Demoen, B., Lifschitz, V. (eds) Logic Programming. ICLP 2004. Lecture Notes in Computer Science, vol 3132. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-27775-0_3
Download citation
DOI: https://doi.org/10.1007/978-3-540-27775-0_3
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-22671-0
Online ISBN: 978-3-540-27775-0
eBook Packages: Springer Book Archive