More Web Proxy on the site http://driver.im/

Article

Free access

A precise type analysis of logic programs

Author:

Lunjin LuAuthors Info & Claims

PPDP '00: Proceedings of the 2nd ACM SIGPLAN international conference on Principles and practice of declarative programming

Pages 214 - 225

https://doi.org/10.1145/351268.351293

Published: 01 September 2000 Publication History

Abstract

This paper presents a new type analysis for logic programs. The type information in a set of substitutions is described by a disjunction of variable typings each of which maps a variable to a non-deterministic regular type. The use of non-deterministic regular types, set union and intersection operators, and disjunctions of variable typings makes the new type analysis more precise than those found in the literature. Experimental results on the performance of the new analysis are given together with comparable results from an existing type analysis. The fundamental problem of checking the emptiness of non-deterministic regular types is more complex in the new analysis. The experimental results, however, show that careful use of tabling reduces the effect to an average of 15% of execution time on a set of benchmarks.

References

[1]

R. Barbuti and R. Giacobazzi. A bottom-up polymorphic type inference in logic programming. Science ofcomputer programming, 19(3):133{181, 1992.

Digital Library

[2]

M. Bruynooghe. A practical framework for the abstract interpretation of logic progams. Journal of Logic Programming, 10(2):91{124, 1991.

Digital Library

[3]

M. Bruynooghe, G. Janssens, A. Callebaut, and B. Demoen. Abstract interpretation: towards the global optimisation of Prolog programs. In Proceedings of the 1987 Symposium on Logic Programming, pages 192{204. The IEEE Computer Society Press, 1987.

[4]

M. Codish and B. Demoen. Deriving polymorphic type dependencies for logic programs using multiple incarnations of Prop. Lecture Notes in Computer Science, 864:281{297, 1994.

[5]

M. Codish and V. Lagoon. Type dependencies for logic programs using ACI-uni~cation. In Proceedings of the 1996 Israeli Symposium on Theory of Computing and Systems, pages 136{145. IEEE Press, June 1996.

[6]

M.M. Corsini and K. Musumbu. Type inference: a new approach. Journal of Theoretical Computer Science, 119(1):23{38, 1993.

Digital Library

[7]

A. Cortesi, B. Le Charlier, and P. van Hentenryck. Type analysis of Prolog using type graphs. Journal of Logic Programming, 22(3):179{208, 1995.

[8]

P. Cousot and R. Cousot. Abstract interpretation: a uni~ed framework for static analysis of programs by construction or approximation of ~xpoints. In Proceedings of the fourth annual ACM symposium on Principles of programming languages, pages 238{252. The ACM Press, 1977.

Digital Library

[9]

P.W. Dart and J. Zobel. E~cient run-time type checking of typed logic programs. Journal of Logic Programming, 14(1-2):31{69, 1992.

Digital Library

[10]

P.W. Dart and J. Zobel. A regular type language for logic programs. In F. Pfenning, editor, Types in Logic Programming, pages 157{189. The MIT Press, 1992.

[11]

T. Fruhwirth, E. Shapiro, M.Y. Vardi, and E. Yardeni. Logic programs as types for logic programs. In Proceedings of Sixth Annual IEEE Symposium on Logic in Computer Science, pages 300{309. The IEEE Computer Society Press, 1991.

[12]

J.P. Gallagher and D.A. de Waal. Fast and precise regular approximations of logic programs. In M. Bruynooghe, editor, Proceedings of the Eleventh International Conference onLogic Programming, pages 599{613. The MIT Press, 1994.

Digital Library

[13]

F. G~ecseg and M. Steinby. Tree Automata. Akad~emiai Kiad~o, 1984.

[14]

M. Hanus. Horn clause programs with polymorphic types: semantics and resolution. Journal of Theoretical Computer Science, 89(1):63{106, 1991.

Digital Library

[15]

N. Heintze and J. Ja~ar. A ~nite presentation theorem for approximating logic programs. In Proceedings of the seventh Annual ACM Symposium on Principles of Programming Languages, pages 197{209. The ACM Press, 1990.

Digital Library

[16]

N. Heintze and J. Ja~ar. Semantic types for logic programs. In F. Pfenning, editor, Types in Logic Programming, pages 141{155. The MIT Press, 1992.

[17]

M. Hermenegildo, R. Warren, and S.K. Debray. Global ow analysis as a practical compilation tool. Journal of Logic Programming, 13(1, 2, 3 and 4):349{366, 1992.

Digital Library

[18]

K. Horiuchi and T. Kanamori. Polymorphic type inference in Prolog by abstract interpretation. In K. Furukawa, H. Tanaka,and T. Fujisaki, editors, Proceedings of the Sixth Conference onLogic Programming, pages 195{214, Tokyo, June 1987.

Digital Library

[19]

G. Janssens and M. Bruynooghe. Deriving descriptions of possible values of program variables by means of abstract interpretation. Journal of Logic Programming, 13(1, 2, 3 and 4):205{258, 1992.

Digital Library

[20]

T. Kanamori. Abstract interpretation based on Alexander Templates. Journal of Logic Programming, 15(1 & 2):31{54, 1993.

Digital Library

[21]

T. Kanamori and K. Horiuchi. Type inference in Prolog and its application. In Proceedings of the ninth International Joint Conference onArti~cial Intelligence, pages 704{707, 1985.

[22]

T. Kanamori and T. Kawamura. Abstract interpretation based on OLDT resolution. Journal of Logic Programming, 15(1 & 2):1{30, January 1993.

Digital Library

[23]

G. Levi and F. Spoto. An experiment in domain re~nement: type domains and type representations for logic programs. Lecture Notes in Computer Science, 1490:152{169, 1998.

Digital Library

[24]

J.W. Lloyd. Foundations of Logic Programming. Springer-Verlag, 1987.

Digital Library

[25]

L. Lu. Abstract interpretation, bug detection and bug diagnosis in normal logic programs. PhD thesis, University of Birmingham, 1994.

[26]

L. Lu. Type analysis of logic programs in the presence of type de~nitions. In Proceedings of the 1995 ACM SIGPLAN Symposium on Partial Evaluation and Semantics-Based program manipulation, pages 241{252. The ACM Press, 1995.

Digital Library

[27]

L. Lu. A polymorphic type analysis in logic programs by abstract interpretation. Journal of Logic Programming, 36(1):1{54, 1998.

[28]

L. Lu and J. Cleary. An emptiness algorithm for regular types with set operators. Technical report, Department of Computer Science, The University of Waikato, November 1998. http://xxx.lanl.gov/ps.LO/cs/9811015.

[29]

K. Marriott and H. S?ndergaard. Semantics-based data ow analysis of logic programs. In G. Ritter, editor, Information Processing'89. North-Holland, 1989.

[30]

K. Marriott, H. S?ndergaard, and N.D. Jones. Denotational abstract interpretation of logic programs. ACM Transactions on Programming Languages and Systems, 16(3):607{648, 1994.

Digital Library

[31]

P. Mishra. Towardsa theoryof types in Prolog. In Proceedings of the IEEE international Symposium on Logic Programming, pages 289{298. The IEEE Computer Society Press, 1984.

[32]

K. Muthukumar and M. Hermenegildo. Compile-time derivation of variable dependency using abstract interpretation. Journal of Logic Programming, 13(1, 2, 3 and 4):315{347, 1992.

Digital Library

[33]

A. Mycroft and R.A. O'Keefe. A polymorphic type system for Prolog. Arti~cial Intelligence, 23:295{307, 1984.

Digital Library

[34]

U. Nilsson. Towards a framework for the abstract interpretation of logic programs. In Proceedings of the International Workshop on Programming Language Implementation and Logic Programming, pages 68{82. Springer-Verlag, 1988.

Digital Library

[35]

F. Pfenning, editor. Types in logic programming. The MIT Press, Cambridge, Massachusetts, 1992.

Digital Library

[36]

U.S. Reddy. Types for logic programs. In Proceedings of the 1990 North American Conference onLogic Programming, pages 836{40. The MIT Press, 1990.

Digital Library

[37]

H. Saglam and J.P. Gallagher. Approximating constraint logic programs using polymorphic types and regular descriptions. Technical Report CSTR-95-017, Department of Computer Science, University of Bristol, July 1995.

Digital Library

[38]

D. S. Warren. Memoing for logic programs. Communications of the ACM, 35(3):93{111, 1992.

Digital Library

[39]

E. Yardeni, T. Fruehwirth, and E. Shapiro. Polymorphically typed logic programs. In K. Furukawa, editor, Logic Programming. Proceedings of the Eighth International Conference, pages 379{93. The MIT Press, 1991.

[40]

E. Yardeni and E. Shapiro. A type system for logic programs. Journal of Logic Programming, 10(2):125{153, 1991.

Digital Library

[41]

J. Zobel. Derivation of polymorphic types for Prolog programs. In J.-L. Lassez, editor, Logic Programming: Proceedings of the fourth international conference, pages 817{838. The MIT Press, 1987.

Cited By

Lu L(2019)Path Dependent Analysis of Logic ProgramsHigher-Order and Symbolic Computation10.1023/A:102582490368316:4(341-377)Online publication date: 1-Jun-2019
https://dl.acm.org/doi/10.1023/A%3A1025824903683
Schneider-Kamp PGiesl JSerebrenik AThiemann R(2009)Automated termination proofs for logic programs by term rewritingACM Transactions on Computational Logic (TOCL)10.1145/1614431.161443311:1(1-52)Online publication date: 6-Nov-2009
https://dl.acm.org/doi/10.1145/1614431.1614433
Lu L(2002)Path dependent analysis of logic programsACM SIGPLAN Notices10.1145/509799.50303837:3(63-74)Online publication date: 14-Jan-2002
https://dl.acm.org/doi/10.1145/509799.503038
Show More Cited By

Index Terms

A precise type analysis of logic programs
1. Computing methodologies
  1. Artificial intelligence
    1. Knowledge representation and reasoning
  2. Symbolic and algebraic manipulation
    1. Symbolic and algebraic algorithms
      1. Theorem proving algorithms
2. Theory of computation
  1. Logic
  2. Models of computation

Recommendations

Inferring precise polymorphic type dependencies in logic programs
PPDP '08: Proceedings of the 10th international ACM SIGPLAN conference on Principles and practice of declarative programming

We present a new analysis that infers polymorphic type dependencies in logic programs. The analysis infers more precise information than previous type dependency inference analyses. The improvement in precision is achieved by making use of set union as ...
Principal Type Schemes for Gradual Programs
POPL '15: Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages

Gradual typing is a discipline for integrating dynamic checking into a static type system. Since its introduction in functional languages, it has been adapted to a variety of type systems, including object-oriented, security, and substructural. This ...
A Polymorphic Type Dependency Analysis for Logic Programs
Abstract
An analysis is presented that infers polymorphic type dependencies in logic programs. Using set union as a type constructor and non-deterministic type definitions, the analysis infers more precise information than previous type dependency ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

PPDP '00: Proceedings of the 2nd ACM SIGPLAN international conference on Principles and practice of declarative programming

September 2000

301 pages

ISBN:1581132654

DOI:10.1145/351268

Chairman:
Maurizio Gabbrielli
Univ. of Udine, Italy
,
Editor:
Frank Pfenning
Carnegie Mellon Univ., Pittsburgh, PA

Copyright © 2000 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Sponsors

SIGPLAN: ACM Special Interest Group on Programming Languages

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 01 September 2000

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Qualifiers

Article

Conference

PPDP00

Sponsor:

SIGPLAN

PPDP00: International Conference on Principles and Practice of Declarative Programming

September 20 - 23, 2000

Quebec, Montreal, Canada

Acceptance Rates

PPDP '00 Paper Acceptance Rate 26 of 65 submissions, 40%;

Overall Acceptance Rate 230 of 486 submissions, 47%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

5
Total Citations
View Citations
1,451
Total Downloads

Downloads (Last 12 months)17
Downloads (Last 6 weeks)1

Reflects downloads up to 11 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

Lu L(2019)Path Dependent Analysis of Logic ProgramsHigher-Order and Symbolic Computation10.1023/A:102582490368316:4(341-377)Online publication date: 1-Jun-2019
https://dl.acm.org/doi/10.1023/A%3A1025824903683
Schneider-Kamp PGiesl JSerebrenik AThiemann R(2009)Automated termination proofs for logic programs by term rewritingACM Transactions on Computational Logic (TOCL)10.1145/1614431.161443311:1(1-52)Online publication date: 6-Nov-2009
https://dl.acm.org/doi/10.1145/1614431.1614433
Lu L(2002)Path dependent analysis of logic programsACM SIGPLAN Notices10.1145/509799.50303837:3(63-74)Online publication date: 14-Jan-2002
https://dl.acm.org/doi/10.1145/509799.503038
Lu LThiemann P(2002)Path dependent analysis of logic programsProceedings of the 2002 ACM SIGPLAN workshop on Partial evaluation and semantics-based program manipulation10.1145/503032.503038(63-74)Online publication date: 14-Jan-2002
https://dl.acm.org/doi/10.1145/503032.503038
Lu LKing A(2002)Backward Type Inference Generalises Type CheckingStatic Analysis10.1007/3-540-45789-5_9(85-101)Online publication date: 5-Sep-2002
https://doi.org/10.1007/3-540-45789-5_9

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

Media

Figures

Other

Tables

View Table of Contents