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

Tyng Ruey Chuang, Benjamin Goldberg

Research output: Contribution to journalArticle

Abstract

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.

Original languageEnglish (US)
Pages (from-to)357-394
Number of pages38
JournalJournal of Functional Programming
Volume7
Issue number4
StatePublished - Jul 1997

Fingerprint

Syntactics
Semantics
Acoustic waves

ASJC Scopus subject areas

  • Computer Graphics and Computer-Aided Design
  • Software

Cite this

A syntactic method for finding least fixed points of higher-order functions over finite domains. / Chuang, Tyng Ruey; Goldberg, Benjamin.

In: Journal of Functional Programming, Vol. 7, No. 4, 07.1997, p. 357-394.

Research output: Contribution to journalArticle

@article{0ff02227bac84589abfe64463e0bb620,
title = "A syntactic method for finding least fixed points of higher-order functions over finite domains",
abstract = "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.",
author = "Chuang, {Tyng Ruey} and Benjamin Goldberg",
year = "1997",
month = "7",
language = "English (US)",
volume = "7",
pages = "357--394",
journal = "Journal of Functional Programming",
issn = "0956-7968",
publisher = "Cambridge University Press",
number = "4",

}

TY - JOUR

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

AU - Chuang, Tyng Ruey

AU - Goldberg, Benjamin

PY - 1997/7

Y1 - 1997/7

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=0031525364&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=0031525364&partnerID=8YFLogxK

M3 - Article

AN - SCOPUS:0031525364

VL - 7

SP - 357

EP - 394

JO - Journal of Functional Programming

JF - Journal of Functional Programming

SN - 0956-7968

IS - 4

ER -