Tarski's fixpoint theorem and static analysis -- reference?
John Fiskio-Lasseter
regarding the existence of least/greatest fixpoints of monotonic
functions on a complete lattice ("A Lattice Theoretical Fixpoint
Theorem and its Applications", Pacific J. of Math. 5, 285-309, 1955) as
the basis for termination of the standard dataflow analysis algorithms.
None of the "classical" data flow works I've read (Killdall '73, Kam &
Ullman '76, Kam & Ullman '77, Hecht '77) cite this paper, nor any of
the compilers textbooks Ive seen (the dragon book, Fischer & LeBlanc,
Muchnick's _Advanced Compiler Design_).
It is, however, given an appendix' worth of summary in the recent
_Principles of Program Analysis_ textbook by Nielson, Nielson, &
Hankin, suggesting to me that his relevance was identified by the
abstract interpretation community. Indeed, the earliest citation of
Tarski's paper that I've seen (within the static analysis community) is
the Cousots' original abstract interpretation paper from POPL 77, and
they later published a constructive proof of Tarksi's theorem, also in
the Pacific Journal of Mathematics [82(1), 1979].
Were they the first ones to observe the relevance of Tarski's theorem
to static analysis, or is there an earlier paper that cites him?
Thanks,
John
----------------------------------------------------------------------
John Fiskio-Lasseter
* Phd. Student, CIS Dept., University of Oregon
* Deschutes 234 x6-1385 joh...@cs.uoregon.edu
Jens Kilian
> Were they the first ones to observe the relevance of Tarski's theorem
> to static analysis, or is there an earlier paper that cites him?
IIRC, fixpoint analysis was used to define the semantics of Prolog; I have no
idea if this predates the abstract interpretation paper.
...clickety click...
This might be relevant:
van Emden, M., and Kowalski, R. The semantics of predicate logic as
a programming language. Journal of the Assoc. for Comp. Mach. 23 (1976),
733742
HTH,
Jens.
--
mailto:j...@acm.org phone:+49-7031-464-7698 (TELNET 778-7698)
http://www.bawue.de/~jjk/ fax:+49-7031-464-7351
PGP: 06 04 1C 35 7B DC 1F 26 As the air to a bird, or the sea to a fish,
0x555DA8B5 BB A2 F0 66 77 75 E1 08 so is contempt to the contemptible. [Blake]
David Chase
> I'm curious to know the earliest paper that identifies Tarski's theorem
> regarding the existence of least/greatest fixpoints of monotonic
> functions on a complete lattice ("A Lattice Theoretical Fixpoint
> Theorem and its Applications", Pacific J. of Math. 5, 285-309, 1955) as
> the basis for termination of the standard dataflow analysis algorithms.
Note sure if I can help, but Huet cited a paper by Newman, and he
might include other pointers in the same direction. It wouldn't
surprise me if Cousot & C were the first.
@article{Newman:TCDE,
AUTHOR="M. H. A. Newman",
TITLE="On theories with a combinatorial definition of ``equivalence''",
JOURNAL="Annals of Mathematics",VOLUME=43, NUMBER=2, YEAR=1942,MONTH=apr,
PAGES={223--243},
NOTE="Cited in \cite{Huet:CR}"
}
@article{Huet:CR,
AUTHOR="{G\'{e}rard} Huet",
TITLE="Confluent Reductions: {A}bstract properties and
applications to term rewriting systems",
JOURNAL=jacm,
VOLUME=27, NUMBER=4,YEAR=1980,MONTH=oct,PAGES={797--821}
}
I don't recall the exact meaning, but Newman's Lemma was something
along the lines of "locally confluent and finite implies Church-Rosser".
David Chase
Jamie Andrews
>> Were [the Cousots] the first ones to observe the relevance of Tarski's theorem
>> to static analysis, or is there an earlier paper that cites him?
Jens Kilian <Jens_...@agilent.com> wrote:
>IIRC, fixpoint analysis was used to define the semantics of Prolog; I have no
>idea if this predates the abstract interpretation paper.
>This might be relevant:
> van Emden, M., and Kowalski, R. The semantics of predicate logic as
> a programming language. Journal of the Assoc. for Comp. Mach. 23 (1976),
> 733742
Van Emden and Kowalski were applying ideas that were
already well-known from semantics of other programming
languages. Van Emden had read about fixpoint semantics of other
languages, and wanted to see if he and Kowalski could apply them
to Prolog.
Intrigued by the history question, I looked in my copy of
Stoy (1977) for the earliest papers on programming language
semantics as we now know it. It pointed to a 1966 paper (from
a 1964 workshop) by Strachey in:
Formal Language Description Languages for Computer Programming
ed. T. B. Steel
North-Holland 1966
I looked up that volume (it was in our library!), and found
the following curious situation:
- Tarski's crucial 1955 paper is in the bibliography (ref. 316).
- However, there is one bibliography for the whole book,
not separate ones for each paper.
- Strachey's paper does not seem to cite Tarski's paper.
- Landin has a key paper in the same volume that doesn't seem
to cite it either.
- In fact, I couldn't find *any* citation of Tarski's paper in
my brief (15 min) scan of the whole book, except for a
citation by Elgot about Turing machines which is probably
supposed to be a citation of a Turing paper (ref. 319).
I invite others to give it a closer look. Perhaps a citation
is even hidden in Strachey's paper somewhere where I didn't
notice it. But I doubt it because of the below.
In Scott's Foreward to Stoy's book, he quotes Strachey
talking about his (Scott's) work: "The relevant theorems about
fixed points, due to Knaster and Tarski, had little impact on
computing [as distinct from recursive function theory] until the
work of David Park and Scott. Landin in his 1964 paper made use
of the 'paradoxical combinator', Y.... After Scott had completed
his theory of reflexive domains [in 1969], Park showed that this
operator could be identified with the [lattice-theoretic minimal
fixed-point function of Stoy's book]."
So, this indicates that the relevance of Knaster-Tarski to
*programming language semantics* was not known until 1969-1970
or so.
To return to the original poster's point:
> None of the "classical" data flow works I've read (Killdall '73, Kam &
> Ullman '76, Kam & Ullman '77, Hecht '77) cite this paper, nor any of
> the compilers textbooks Ive seen (the dragon book, Fischer & LeBlanc,
> Muchnick's _Advanced Compiler Design_).
It might be that the notion had not yet broken out of the
semantics area by that time, so the Cousots' 1977 paper may well
be the first. Indeed, it may well be that a Cousot or two read
Stoy's book (copyright date 1977, thus available possibly in
1976), and understood the importance of Tarski's theorem to
dataflow analysis then. I don't have the Cousots' paper -- does
it cite Stoy as well as Tarski?
(p.s. I'm a tyro at this... I'm sure there are any number of
people in the UK that could give a clearer answer.)
--Jamie. (nel mezzo del cammin di nostra vita)
John Fiskio-Lasseter
> It might be that the notion had not yet broken out of the
> semantics area by that time, so the Cousots' 1977 paper may well
> be the first. Indeed, it may well be that a Cousot or two read
> Stoy's book (copyright date 1977, thus available possibly in
> 1976), and understood the importance of Tarski's theorem to
> dataflow analysis then. I don't have the Cousots' paper -- does
> it cite Stoy as well as Tarski?
Unfortunately, my copy's in my office right now, so I can't check from
home. I'm almost positive, though, that Scott's "Data Types as
Lattices" paper is included in the bibliography of the first POPL
paper on abstract interpretation -- not sure about Stoy. That's
certainly consistent with your suggestion about the chain of
influence, which also fits well with the more general story of
abstract interpretation and its use in establishing a link between
program analysis and semantics.
-- John