What Sequential Games , the Tychonoff Theorem and the Double-Negation Shift have in Common

• Published in 2010
• Added on 2010-08-04

This is a tutorial for mathematically inclined functional programmers, based on previously published, peered reviewed theoretical work. We discuss a higher-type functional, written here in the functional programming language Haskell, which (1) optimally plays sequential games, (2) implements a computational version of the Tychonoff Theorem from topology, and (3) realizes the Double Negation Shift from logic and proof theory. The functional makes sense for finite and infinite (lazy) lists, and in the binary case it amounts to an operation that is available in any (strong) monad. In fact, once we define this monad in Haskell, it turns out that this amazingly versatile functional is already available in Haskell, in the standard prelude, called sequence, which iterates this binary operation. Therefore Haskell proves that this functional is even more versatile than anticipated, as the function sequence was introduced for other purposes by the language designers, in particular the iteration of a list of monadic effects (but effects are not what we discuss here)

Links

• http://www.cs.bham.ac.uk/~mhe/papers/msfp2010/Escardo-Oliva-MSFP2010.pdf

Other information

BibTeX entry

@article{Oliva2010,
	key = {Oliva2010},
	type = {article},
	title = {What Sequential Games , the Tychonoff Theorem and the Double-Negation Shift have in Common},
	author = {Oliva, Paulo and Escardo, Martin},
	abstract = {This is a tutorial for mathematically inclined functional programmers, based on previously published, peered reviewed theoretical work. We discuss a higher-type functional, written here in the functional programming language Haskell, which (1) optimally plays sequential games, (2) implements a computational version of the Tychonoff Theorem from topology, and (3) realizes the Double Negation Shift from logic and proof theory. The functional makes sense for finite and infinite (lazy) lists, and in the binary case it amounts to an operation that is available in any (strong) monad. In fact, once we define this monad in Haskell, it turns out that this amazingly versatile functional is already available in Haskell, in the standard prelude, called sequence, which iterates this binary operation.
Therefore Haskell proves that this functional is even more versatile than anticipated, as the function sequence was introduced for other purposes by the language designers, in particular the iteration of a list of monadic effects (but effects are not what we discuss here)},
	comment = {},
	date_added = {2010-08-04},
	date_published = {2010-04-10},
	urls = {http://www.cs.bham.ac.uk/{\~{}}mhe/papers/msfp2010/Escardo-Oliva-MSFP2010.pdf},
	collections = {Basically computer science,Protocols and strategies,Games to play with friends},
	url = {http://www.cs.bham.ac.uk/{\~{}}mhe/papers/msfp2010/Escardo-Oliva-MSFP2010.pdf},
	urldate = {2010-08-04},
	journal = {Topology},
	keywords = {agda,axiom of choice,dependent type,exhaustible set,foundations,functional programming,game theory,haskell,infinite data,logic,monad,optimal strategy,search,topology},
	year = 2010
}