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

John Fiskio-Lasseter wrote:


> 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

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