Hostname: page-component-586b7cd67f-tf8b9 Total loading time: 0 Render date: 2024-11-24T22:02:36.110Z Has data issue: false hasContentIssue false
  • English
  • Français

Fixed points and frontiers: a new perspective

Published online by Cambridge University Press:  07 November 2008

Sebastian Hunt  and
Chris Hankin
Sebastian Hunt
Affiliation:
Department of Computing, Imperial College, London
Chris Hankin
Affiliation:
Department of Computing, Imperial College, London
Rights & Permissions [Opens in a new window]

Abstract

Core share and HTML view are not available for this content. However, as you have access to this content, a full PDF is available via the ‘Save PDF’ action button.

Abstract interpretation is the collective name for a family of semantics-based techniques for compile-time analysis of programs. One of the most costly operations in automating such analyses is the computation of fixed points. The frontiers algorithm is an elegant method, invented by Chris Clack and Simon Peyton Jones, which addresses this issue.

In this article we present a new approach to the frontiers algorithm based on the insight that frontiers represent upper and lower subsets of a function's argument domain. This insight leads to a new formulation of the frontiers algorithm for higher-order functions, which is considerably more concise than previous versions.

We go on to argue that for many functions, especially in the higher-order case, finding fixed points is an intractable problem unless the sizes of the abstract domains are reduced. We show how the semantic machinery of abstract interpretation allows us to place upper and lower bounds on the values of fixed points in large lattices by working within smaller ones.

Type
Article
Information
Journal of Functional Programming , Volume 1 , Issue 1 , January 1991 , pp. 91 - 120
Copyright
Copyright © Cambridge University Press 1991

References

Abramsky, Samson. 1986. Strictness analysis and polymorphic invariance. In Ganzinger, H. and Jones, N. D. (editors), Programs as Data Objects, Lecture Notes in Computer Science 217. Springer-Verlag.Google Scholar
Abramsky, Samson and Hankin, Chris (editors). 1987. Abstract Interpretation of Declarative Languages. Ellis Horwood.Google Scholar
Burn, G. L., Hankin, Chris and Abramsky, Samson. 1986. The theory of strictness analysis for higher-order functions. In Ganzinger, H. and Jones, N. D. (editors), Programs as Data Objects, Lecture Notes in Computer Science 217, pp. 42–62, Springer-Verlag.Google Scholar
Burn, G. L. 1987. Abstract Interpretation and the Parallel Evaluation of Functional Languages. PhD thesis, Department of Computing, Imperial College of Science and Technology, University of London.Google Scholar
Clack, Chris and Jones, Peyton, Simon, . 1985. Strictness analysis – a practical approach. In Jouannaud, J.-P. (editor), Functional Programming Languages and Computer Architecture, Lecture Notes in Computer Science 201, pp. 35–49. Springer-Verlag.Google Scholar
Gierz, G., Hofmann, K. H., Keimel, K., Lawson, J. D., Mislove, M. and Scott, D. S., 1980. A Compendium of Continuous Lattices. Springer-Verlag.CrossRefGoogle Scholar
Goldberg, B. and Park, Y. G. 1990. Higher-order escape analysis: optimising stack allocation in functional program implementations. In Jones, N. D. (editor), ESOP '90, 3rd European Symposium on Programming,Copenhagen, Denmark.May 1990. Lecture Notes in Computer Science 432. Springer-Verlag.CrossRefGoogle Scholar
Hughes, John. 1988. Abstract interpretation of first-order polymorphic functions. In Glasgow Workshop on Functional Programming, University of Glasgow, Department of Computing Science (August 1988). Research Report 89/R4.Google Scholar
Hunt, Sebastian. 1989. Frontiers and open sets in abstract interpretation. In MacQueen, D. (editor), Functional Programming Languages and Computer Architecture, pp. 1–11. ACM Publications (09 1989).Google Scholar
Jones, Peyton, Simon, and Clack, Chris. 1987. Finding fixpoints in abstract interpretation. In Abramsky, Samson, and Hankin, Chris (editors), Abstract Interpretation of Declarative Languages, chapter 11. Ellis Horwood.Google Scholar
Jones, N. D., Sestoft, P. and Søndergaard, H. 1985. An experiment in partial evaluation: the generation of a compiler generator. In Jouannaud, J.-P. (editor), Rewriting Techniques and Applications, Lecture Notes in Computer Science 202, pp. 124–140. Springer-Verlag.CrossRefGoogle Scholar
Martin, Chris. 1989. Algorithms for Finding Fixpoints in Abstract Interpretation. PhD thesis, Department of Computing, Imperial College of Science, Technology and Medicine, University of London.Google Scholar
Martin, Chris and Hankin, Chris. 1987. Finding fixed points in finite lattices. In Kahn, G. (editor), Functional Programming Languages and Computer Architecture, Lecture Notes in Computer Science 274, pp. 426–45. Springer-Verlag (09 1987).Google Scholar
Mycroft, A. 1989. Abstract Interpretation and Optimising Transformations for Applicative Programs. PhD thesis, University of Edinburgh.Google Scholar
Vickers, S. J. 1989. Topology via Logic. Cambridge University Press.Google Scholar
Wadler, P. 1987. Strictness analysis on non-flat domains (by abstract interpretation over finite domains). In Abramsky, Samson and Hankin, Chris (editors) Abstract Interpretation of Declarative Languages, chapter 12. Ellis Horwood.Google Scholar
Submit a response

Discussions

No Discussions have been published for this article.