14 Mar 2003 11:25:51 -0500

Related articles |
---|

Tarski's fixpoint theorem and static analysis -- reference? johnfl@cs.uoregon.edu (John Fiskio-Lasseter) (2003-02-24) |

Re: Tarski's fixpoint theorem and static analysis -- reference? Jens_Kilian@agilent.com (Jens Kilian) (2003-03-09) |

Re: Tarski's fixpoint theorem and static analysis -- reference? chase@theworld.com (David Chase) (2003-03-09) |

Re: Tarski's fixpoint theorem and static analysis -- reference? andrews@csd.uwo.ca (2003-03-14) |

Re: Tarski's fixpoint theorem and static analysis -- reference? johnfl@cs.uoregon.edu (John Fiskio-Lasseter) (2003-03-17) |

Re: Tarski's fixpoint theorem and static analysis -- reference? steck@stecksoft.com (Paul A. Steckler) (2003-03-23) |

From: | andrews@csd.uwo.ca (Jamie Andrews) |

Newsgroups: | comp.theory,comp.compilers |

Date: | 14 Mar 2003 11:25:51 -0500 |

Organization: | Department of Computer Science, University of Western Ontario |

References: | 03-02-151 03-03-013 |

Keywords: | analysis |

Posted-Date: | 14 Mar 2003 11:25:51 EST |

Originator: | andrews@csd.uwo.ca |

*>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),*

*> 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)

Post a followup to this message

Return to the
comp.compilers page.

Search the
comp.compilers archives again.