JAIST Logic@JAIST

Digit Spaces - Topological Foundations

  • Dieter Spreen
  • University of Siegen
  • This seminar is held as a part of JSPS Core-to-Core Program, A. Advanced Research Networks, and EU FP7 Marie Curie Actions IRSES project COMPUTAL (http://computal.uni-trier.de/).
Date: 2015/05/07 (Thu) 13:30 to 15:00
Place: JAIST, Collaboration room 6 (I-57g)
Group: Logic Unit
Digit spaces have been introduced by Ulrich Berger as a framework for extracting programs that deal with continuous data from formal proofs.The essential idea was to represent objects as streams of unary contractions on a complete metric space and to use coinduction on the logical side. In recent joint work on an extension of this approach to hyperspaces like the space of nonempty compact subsets of a digit space, it turned out that compact cannot be represented by such streams in general: instead one has to deal with infinite trees the nodes of which are labeled by contraction similar to the stream case. It was realized, however, that one will obtain a uniform theory, if the contractions, also called digits, are allowed to be multi-ary.
Contact Hajime ISHIHARA