9 Mar 2003 17:26:11 -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: | 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.