Hostname: page-component-7c8c6479df-24hb2 Total loading time: 0 Render date: 2024-03-18T14:46:08.691Z Has data issue: false hasContentIssue false

A syntactic method for finding least fixed points of higher-order functions over finite domains

Published online by Cambridge University Press:  01 July 1997

TYNG-RUEY CHUANG
Affiliation:
Institute of Information Science, Academia Sinica, Nankang, Taipei 11529, Taiwan
BENJAMIN GOLDBERG
Affiliation:
Department of Computer Science, Courant Institute of Mathematical Sciences, New York University, 251 Mercer Street, New York, NY 10012, USA
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.

This paper describes a method for finding the least fixed points of higher-order functions over finite domains using symbolic manipulation. Fixed point finding is an essential component in the calculation of abstract semantics of functional programs, providing the foundation for program analyses based on abstract interpretation. Previous methods for fixed point finding have primarily used semantic approaches, which often must traverse large portions of the semantic domain even for simple programs. This paper provides the theoretical framework for a syntax-based analysis that is potentially very fast. The proposed syntactic method is based on an augmented simply typed lambda calculus where the symbolic representation of each function produced in the fixed point iteration is transformed to a syntactic normal form. Normal forms resulting from successive iterations are then compared syntactically to determine their ordering in the semantic domain, and to decide whether a fixed point has been reached. We show the method to be sound, complete and compositional. Examples are presented to show how this method can be used to perform strictness analysis for higher-order functions over non-flat domains. Our method is compositional in the sense that the strictness property of an expression can be easily calculated from those of its sub-expressions. This is contrary to most strictness analysers, where the strictness property of an expression has to be computed anew whenever one of its subexpressions changes. We also compare our approach with recent developments in strictness analysis.

Type
Research Article
Copyright
© 1997 Cambridge University Press

Footnotes

A preliminary version of this paper was presented at the 1992 ACM Conference on Lisp and Functional Programming, June 1992, San Francisco, CA, USA, under the title ‘A syntactic approach to fixed point computation on finite domains’. This research has been supported, in part, by the National Science Foundation (CCR–8909634) and DARPA (DARPA/ONR N00014–91–J1472). A part of this work was performed while Tyng–Ruey Chuang was at Department of Computer Science, New York University.
Submit a response

Discussions

No Discussions have been published for this article.