Logic in Computer Science (LICS 1997)

Paper: Induction and recursion on the partial real line via biquotients of bifree algebras (at LICS 1997)

Authors: Martin Hotzel Escardo Thomas Streicher

Abstract

The partial real line is the continuous domain of compact real intervals ordered by reverse inclusion. The idea is that singleton intervals represent total real numbers, and that the remaining intervals represent (properly) partial real numbers. This is justified by the fact that the singleton map is a topological embedding of the Euclidean real line into the partial real line endowed with its Scott topology. The partial real line has been used to model exact real number computation in the framework of the programming language Real PCF, including computation of integrals. We introduce induction principles and recursion schemes for the partial unit interval (the domain of closed subintervals of the unit interval [0,1]), which allow us to verify that Real PCF programs meet their specification. In domain theory one usually derives induction principles and recursion schemes from canonical solutions of domain equations. Since the partial real line is not algebraic, it is not the canonical solution of any domain equation involving usual functors. We establish new results about inductive retractions, which generalize canonical solutions of domain equations by means of ideas similar to those of Freyd. In particular, we introduce the notion of a biquotient of a bifree algebra, and we show that the inductive retractions are the biquotients of the bifree algebras. These results are applied to the partial real line.

BibTeX

  @InProceedings{EscardoStreicher-Inductionandrecursi,
    author = 	 {Martin Hotzel Escardo and Thomas Streicher},
    title = 	 {Induction and recursion on the partial real line via biquotients of bifree algebras},
    booktitle =  {Proceedings of the Twelfth Annual IEEE Symp. on Logic in Computer Science, {LICS} 1997},
    year =	 1997,
    editor =	 {Glynn Winskel},
    month =	 {June}, 
    pages =      {376--386},
    location =   {Warsaw, Poland}, 
    publisher =	 {IEEE Computer Society Press}
  }