The twelfth meeting of the Wessex Theory Seminar will take place on Thursday 15 September 2011 at the Queen Mary, University of London.
Venue: Seminar Room BR 4.2 (Computer Science Building, fourth floor, entrance via Bancroft Road).
If you can arrive early, we will be having lunch at Mucci's (inside Campus, opposite Library) from 12 o'clock.
I'll describe ongoing work with my student Vilius Naudziunas on a domain-specific language for implementing various algebraic structures (semirings, ordered semigroups, etc). Expressions in the language are made up of
constants (representing simple algebras such as min-plus) and combinators that construct new structures from components (such as direct and lexicographic products).
The key feature of the language is that it has been designed so that a fixed class of important properties (such as distributivity, idempotence, commutativity, and so on) are automatically proved or refuted by the type system of the language. This allows a user to specify complex algebraic structures and obtain these proofs (or refutations) automatically. It is hoped that the language and its implementation will facilitate the rapid exploration of the algebraic design space.
We have implemented a prototype using the Coq theorem prover. All of the essential theorem proving — for the "typing rules" — is performed at "language design time." Users writing algebraic expressions at "specification time" do not run Coq directly. Rather, they run code that has been extracted automatically from the (constructive) proofs of our library of Coq theorems.
The widely quoted Limited Principle of Omniscience (LPO) is not provable in constructive mathematics, and in particular in ML Type Theory (or in Agda, hopefully).
However, if you suitably enlarge the set of natural numbers with a point at infinity, then you get a set that constructively satisfies the principle of omniscience, in all varieties of constructive mathematics.
Here is a proof written in Agda:
(Given my track record of using Agda in funny ways, I emphasize that this formal proof (1) doesn't disable the termination checker, (2) doesn't use postulates, (3) doesn't rely on translations of classical proofs into intuitionistic proofs, etc. It is in the purest possible fragment of Agda, corresponding to traditional ML Type Theory.)
A proof in human notation is also available in a reference given in the above link. I will present both versions of the proof in the talk, and show that in fact there are plenty of infinite sets that satisfy the principle of omniscience in all varieties of constructive mathematics.
Partial polymorphic stream functions are characterised by their (partial) indexing function which maps elements of the result stream to elements of the input streams. We can define stream functions with mutual recursive equations using primitives 'cons', 'head' and 'tail'. We show that such equations are in fact expressive enough to define all the partial polymorphic stream function.
From Altran Praxis:
Paul Blain Levy
Rasmus L. Petersen
See all Wessex sites involved and meetings so far.