Midlands Graduate School in the Foundations of Computing Science
Christmas Seminars
Thursday 17 December 2015,
14:00-17:45
The University of Birmingham
Room UG10, Murray Learning Centre
Programme
14:00-15:00
On pirates, treasures and monads
Paulo Oliva (Queen Mary, University of London)
The University of Oxford has recently released a couple of their interview questions. One of the computer science questions relates to a group of pirates that have to share a number of gold coins. The problem can be modelled as a strategic game where all players are trying to maximise their share. The solution can be reached at by backward induction. In this talk we will show how the problem can be modelled using the selection monad [1,2], and a solution computed via a simple Haskell implementation.[1] Martin Escardo and Paulo Oliva. Sequential games and optimal strategies. Proceedings of the Royal Society A, 467:1519-1545, 2011
[2] Martin Escardo and Paulo Oliva. Selection functions, bar recursion and backward induction. Mathematical Structures in Computer Science, 20(2):127-168, 2010
15:00-15:45 Refreshments
15:45-16:45
Topology via Logic
Steve Vickers (Birmingham)
Scott's model of the lambda-calculus used topology in a central way: restricting function spaces to continuous functions (and that covered computable ones) circumvented fatal cardinality problems. This stimulated an examination of topology itself in computation.One focus (Abramsky, Smyth, ...) was on a fundamental role of open sets as properties that were finitely observable or semidecidable. Then, in the manner of a "logic of observable properties" (Abramsky's 1987 thesis), the opens can be taken as logical propositions prior to the points that model them. The logic was the "geometric logic", already known from the the point-free approaches to topology that had arisen in topos theory and predicative type theory, and in its full generality it embodies finite conjunctions and arbitrary disjunctions to correspond to intersections and unions of open sets.
My 1989 book "Topology via Logic" summarized the approach, albeit from a classical viewpoint that failed to bring out the important constructive benefits of point-free topology. In this it was like Johnstone's inspirational "Stone Spaces" (1982), but unlike Abramsky's thesis, which respected predicative type theory.
In my talk I shall present some of the deeper implications of the slogan "Topology via Logic": how the contraints of geometric logic suffice to guarantee continuity, both in the traditional sense and in a relativized sense that enables one to discuss bundles as continuous space-valued maps, the fibre depending continuously on the base point. I shall also touch on recent work on using Joyal's arithmetic universes as surrogates for toposes, removing the "arbitrary" infinite disjunctions from geometric logic and making do with a finitary logic that retains enough type theory to capture countable disjunctions by existential quantification.
16:45-17:45
Higher Inductive Types without Recursive Higher Constructors
Nicolai Kraus (Nottingham)
Inductive types in Martin-Lof type theory have constructors that define their elements. Homotopy type theory (HoTT) considers their generalisation, called 'higher inductive types' (HITs), with constructors that may define equalities. This is natural from the homotopical point of view. It can be used to construct higher structurs such as spheres, but it also allows constructions not specific to HoTT such as quotients.Although HITs are frequently used in HoTT, they are not yet well-understood. I discuss whether the full generality of inductive definitions is required for higher constructors. In particular, I show how the connectedness level of a type can be increased stepwise. This leads to a construction of the propositional truncation (a.k.a. squash type, bracket type) without recursive higher constructors. I also show that this can be used to extend a recent similar result by van Doorn.
from 17:45 Pub and Restaurant
Organisation
The 2015 Christmas Seminars are hosted by the School of Computer Science at the University of Birmingham.Please contact Paul Blain Levy for all enquiries.