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

David Chase <chase@theworld.com>
9 Mar 2003 17:26:11 -0500

          From comp.compilers

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)
| List of all articles for this month |

From: David Chase <chase@theworld.com>
Newsgroups: comp.theory,comp.compilers
Date: 9 Mar 2003 17:26:11 -0500
Organization: Little or none
References: 03-02-151
Keywords: analysis
Posted-Date: 09 Mar 2003 17:26:11 EST

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


Post a followup to this message

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