The tenth meeting of the Wessex Theory Seminar took place on Thursday, 7. April 2011 in Swansea.
Lectures were given in Robert Recorde Room (Far-205), Faraday Building (= big blue building to the right on the campus), at Swansea University.
There was a light buffet lunch available from 12:30 onwards for people arriving for the seminar.
This is part of a fruitful ongoing research programme, jointly developed with
Paulo Oliva, which is characterized by the slogan "selection functions everywhere".
I'll present the theory of selection functions, and discuss its role in
game theory, proof theory, topology, higher-type computation, among others.
Selection functions form a strong monad, which can be defined in any
cartesian closed category, and has a morphism into the continuation
monad. In certain categories of domains or spaces, the strength can be
infinitely iterated. This infinite strength is an amazingly versatile
functional that (i) optimally plays sequential games, (ii) realizes
the Double Negation Shift used to realize the classical axiom of
countable choice, and (iii) implements a computational version of the
Tychonoff Theorem from topology. The infinite strength turns out to be
built-in in the functional language Haskell, called sequence, and can
be used to write unexpected programs that compute with infinite
objects, sometimes surprisingly fast. The selection monad also gives
rise to a new translation of classical logic into intuitionistic
logic, which we refer to as the Peirce translation, as monad algebras
are objects that satisfy Peirce's Law.
In this survey talk I will show, through simple examples, how Gödel's dialectica
interpretation allows for the extraction of programs from classical proofs. We will
start with simple theorems from classical predicate logic, and then move into
more complex theorems involving induction and countable choice. The novel
aspect of the talk will centre around the use of the product of selections 1,2 to
obtain direct and readable programs.
1 Martín Escardó and Paulo Oliva, Selection functions, bar recursion and backward induction.
Mathematical Structures in Computer Science, 20(2):127-168, 2010
2 Martín Escardó and Paulo Oliva, Sequential games and optimal strategies.
Proceedings of the Royal Society A, 2010
This talk presents an overview of an ongoing program of
research aiming to produce a representation-independent formalism for
reasoning about search problems and the algorithms used to solve them.
Unlike previous approaches, the focus of this work is on formalising the
notion of search space rather than just the parts of the space explored
by given algorithms. Algebraic structures, I-Spaces, are used to
represent search spaces so that the results are syntax and language
independent. The basic definition of I-Spaces, a model of computation
and an algebraic semantics for CSPs are given as an illustration of this
I will present an ongoing work, joint with Thorsten Altenkirch, on
foundations of Martin-Löf Type Theory which is addressing the question
whether equality of types can be isomorphism or a related notion. Such
a "Higher Dimensional Type Theory" would make it easy to reason about
mathematical concepts up to isomorphism.
A paradigmatic example is that of a vector space which can be
equivalently represented by any of its bases. While it is convenient
to work with any particular base, it is equivalently important that
the choice is irrelevant in the sense that all choices give rise to
the same structure. Currently, this is not possible in Intensional
Type Theory as different bases give rise to coercible but not
extensionally equal vector spaces. In computer science, one routinely
needs to model programming structures which are extensional, however
some concrete syntax is required for definition of programs over the
structures. In greater generality, the problem is the definition of
elimination constants which are irrelevant of the choice made in the
This work is inspired by a proposal by Vladimir Voevodsky on univalent
models of type theory which is also related to recent results by
Garner & van den Berg and Lumsdaine on the weak omega groupoid model
of Type Theory. Our goal is to develop a syntactic theory, which is
computationally well behaved, which supports higher dimensional
Identity Types (i.e. uniqueness of identity proofs doesn't hold) and
which supports extensional reasoning about functions. The upshot of
such a theory would be to seamlessly integrate axiomatic definitions
of mathematical structures in terms of variables, operations and
equations on the one hand and their model theoretic presentations
which work with a chosen representation in a given semantic domain, on
the other hand. An example is Type Theory itself; a faithful model of
which is still an open and bothering problem.
Components and Specifications
PLanCompS is a 4-year EPSRC-funded joint research project between
Swansea, Royal Holloway and City, with Microsoft Research Cambridge
as a project partner, starting mid-2011. It is to establish and test the
practicality of a component-based framework for the design, specification
and implementation of programming languages. The main novelty will be
the creation of a substantial collection of highly reusable, validated language
components called fundamental constructs (funcons). Crucially, the
semantic specification of each funcon will be independent, not needing any
reformulation when funcons are combined or new funcons added to the
collection; specifying a translation of a language to funcons will define both
the static and dynamic semantics of the language. All specifications will be
provided online in an open access repository, with browsing and searching
supported by a digital library interface.
This talk gives a brief presentation of the project, which is about to
recruit three (preferably postdoc) research assistants and two PhD students.
From Queen Mary:
See all Wessex sites involved and meetings so far.