Re: Tarski's fixpoint theorem and static analysis -- reference?

>John Fiskio-Lasseter <johnfl@cs.uoregon.edu> writes:
>> 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_Kilian@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),
> 733­742


          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)

Return to the comp.compilers page.
Search the comp.compilers archives again.