Lics

IEEE Symposium on Logic in Computer Science

LICS Home - LICS Awards - LICS Newsletters - LICS Archive - LICS Organization - Logic-Related Conferences - Links

Fifteenth Annual IEEE Symposium on

Logic in Computer Science (LICS 2000)

Paper: Complete Axioms for Categorical Fixed-Point Operators (at LICS 2000)

Authors: Alex K. Simpson Gordon D. Plotkin

Abstract

We give an axiomatic treatment of fixed-point operators in categories. A notion of iteration operator is defined, embodying the equational properties of iteration theories. We prove a general completeness theorem for iteration operators, relying on a new, purely syntactic characterization of the free iteration theory.We then show how iteration operators arise in axiomatic domain theory. One result derives them from the existence of sufficiently many bifree algebras (exploiting the universal property Freyd introduced in his notion of algebraic compactness). Another result shows that, in the presence of a parameterized natural numbers object and an equational lifting monad, any uniform fixed-point operator is necessarily an iteration operator.

BibTeX

  @InProceedings{SimpsonPlotkin-CompleteAxiomsforCa,
    author = 	 {Alex K. Simpson and Gordon D. Plotkin},
    title = 	 {Complete Axioms for Categorical Fixed-Point Operators},
    booktitle =  {Proceedings of the Fifteenth Annual IEEE Symposium on Logic in Computer Science (LICS 2000)},
    year =	 {2000},
    month =	 {June}, 
    pages =      {30--41},
    location =   {Santa Barbara, CA, USA}, 
    publisher =	 {IEEE Computer Society Press}
  }
   

Last modified: 2017-04-0512:37
Andrzej Murawski