Sequential Games, the Tychonoff Theorem and the Double-Negation Shift (original) (raw)

• The tutorial paper: What Sequential Games, the Tychonoff Theorem and the Double-Negation Shift have in Common.
  We would have liked to include more material and more remarks of an expository nature, and more references to other people's related work, but we had a hard limit of 12 pages.
• Haskell programs.
• Agda programs/proofs.
  Set your browser to use UTF-8 encoding to be able to properly see the mathematical symbols.
• Zip file with the Haskell and Agda programs.
• A Haskell program showing that non-empty exhaustible sets are searchable.
  (This was mentioned in the paper but omitted for lack of space.)
• See also the related posts Seemingly impossible functional programs. andA Haskell monad for infinite search in finite timeat Andrej Bauer's blogMathematics and Computation.
  Functional programmers with less mathematical background should probably start from those posts.
• Errata, last updated 12 August 2010 3:38pm BST.
  The Corrected version of the paper as documented in the errata.