The Pattern-of-Calls Expansion Is the Canonical Fixpoint for Recursive Definitions

Abstract

In partially-addittve semantics, a program ts interpreted as a “sum” of the paths taken during execuuon. Partial-addltion ts motivated here by looking at partml functions, the general notion ofpartmllyadditive monold is axiomaUzed, and examples are discussed The pattern-of-calls expansion is an “infinite sum” decomposition wbach provides a new expression for the interpretive semantics of a recurslvely defined program This expansmn is defined, associated rules are provided for proofs of correctness, and program transformation is demonstrated by algebraic manipulaaon. The general notion of a canomcal fixpoint is then introduced for a family of recursive defmauons as an assignment of a fuxpomt to each deflmtlon m a fashion preserved by a given class of homomorphisms. As a corollary of the “canonical futpomt theorem” it is shown that the least fuxpomt is the umque canonical fixpoint for order semantics. A general axmmatlc treatment of the pattern-of-calls expansion for abstract recursion schemes is offered, and it is shown that the present pattern-of-calls expansion is the umque canonical fixpomt for abstract recursion schemes. Finally, a comparison of order semantics and partially-addiuve semantics is made, showing that in the usual recursive calls defined over partial functions, the least fixpoirtt and the patternof-calls expansion return the same mterpretatton (but vta different formulas). © 1982, ACM. All rights reserved.