The nineteenth meeting of the Wessex Theory Seminar took place on Thursday, 24. January 2013, pm, in Swansea.
Venue
Robert Recorde Room (Far-205), Faraday Building (= large blue building to the right on the campus), at Swansea University.
Lunch at 1pm in Cafe Fusion in Fulton house. Coffee at 1:45 in the Robert Recorde Room.
Programme
1:00-2:00: Lunch
2:00--2:40: Olle Fredriksson (Birmingham): Abstract machines for game semantics, revisited
2:40–3:20: Martin Churchill (Swansea): Modular Bisimulation Theory for Computations and Values
3:20--3:50: Coffee
3:50--4:30: Anupam Das (Bath): A new proof of the propositional pigeonhole principle, for weak monotone systems.
4:30--5:10: Takako Nemoto (JAIST): The proof theoretic strength of determinacy between \Sigma^0_1 and \Delta^0_2
5:10--5:20: Break
5:20--6:00: Peter Schuster (Leeds): Ideal Objects for Finite Methods
Abstracts
Olle Fredriksson and Dan Ghica: Abstract machines for game semantics, revisited: We define new abstract machines for game semantics which correspond to networks of conventional computers, and can be used as an intermediate representation for compilation targeting distributed systems. This is achieved in two steps. First we introduce the HRAM, a Heap and Register Abstract Machine, an abstraction of a conventional computer, which can be structured into HRAM nets, an abstract point-to-point network model. HRAMs are multi-threaded and subsume communication by tokens (cf. IAM) or jumps (cf. JAM). Game Abstract Machines (GAM), are HRAMs with additional structure at the interface level, but no special operational capabilities. We show that GAMs cannot be naively composed, but composition must be mediated using appropriate HRAM combinators. HRAMs are flexible enough to allow the representation of game models for languages with state (non-innocent games) or concurrency (non-alternating games). We illustrate the potential of this technique by implementing a toy distributed compiler for ICA, a higher-order programming language with shared state concurrency, thus significantly extending our previous distributed PCF compiler. We show that compilation is sound and memory-safe, i.e. no (distributed or local) garbage collection is necessary.
Martin Churchill: Modular Bisimulation Theory for Computations and Values: For structural operational semantics (SOS) of process algebras, various notions of bisimulation have been studied, together with rule formats ensuring that bisimilarity is a congruence. For programming languages, however, SOS generally involves auxiliary entities (e.g. stores) and computed values, and the standard bisimulation and rule formats are not directly applicable.
Here, we first introduce a notion of bisimulation based on the distinction between computations and values, with a corresponding liberal congruence format. We then provide metatheory for a modular variant of SOS (MSOS) which provides a systematic treatment of auxiliary entities. This is based on a higher order form of bisimulation, and we formulate an appropriate congruence format. Finally, we show how algebraic laws can be proved sound for bisimulation with reference only to the (M)SOS rules defining the programming constructs involved in them. Such laws remain sound for languages that involve further constructs.
Anupam Das: A new proof of the propositional pigeonhole principle, for weak monotone systems: The pigeonhole principle states that, if there are n+1 pigeons in n holes, there must be two pigeons in the same hole. This can be expressed as a sequence of propositional tautologies, PHP, that has become a benchmark in proof complexity in the last few decades.
Atserias, Galesi and Gavalda have constructed quasipolynomial-size proofs of PHP in the monotone (i.e. negation-free) sequent calculus, based on propositional encodings of certain counting functions. We use a similar approach here to obtain quasipolynomial-size proofs in the fragment free of cuts between ancestors of contraction and weakening steps.
Our argument operates in an equivalent system of the deep inference proof methodology, known to be equivalent to the aforementioned fragment of sequent calculi, where normalisation procedures are more suitable for the task at hand, due primarily to the locality of the inference rules. Our main construction is a formalisation of merge sort in deep inference in order to achieve appropriate permutations of the inputs for the required counting functions.
Takako Nemoto (JAIST): The proof theoretic strength of determinacy between \Sigma^0_1 and \Delta^0_2: It is known that determinacy of infinite games in very low level of the Borel hierarchy can be characterized by set comprehensions in second order arithmetic (cf: [1] and [2]). In this talk, we consider the proof theoretic strength of determinacyschemata between \Sigma^0_1 and \Delta^0_2.
[1] Subsystems of Second order arithmetic 2nd edition, S. G. Simpson, Cambridge University Press
[2] Infinite games in the Cantor space and subsystems of second order arithmetic, T. Nemoto, M. O. Medsalem and K. Tanaka, Mathematical Logic Quarterly, Volume 53, Issue 3 (2007), pp. 226 - 236.
Peter Schuster: Ideal Objects for Finite Methods: Somewhat miraculously, transfinite methods do work for proving quite a few theorems of a fairly finite nature. The corresponding ideal objects are typically invoked towards a contradiction, and therefore do not really exist (Hendtlass).We aim at exploring and exploiting this phenomenon: by reducing transfinite proof methods to finite ones, and thus exhibiting the computational content of the virtually inexistent ideal objects. This is work in progress and follows a bottom-up strategy, i.e. from concrete examples within mathematics to possible metamathematical observations. First case studies have proved sucessful [12, 5]: several theorems that admit short and elegant proofs by contradiction but with Zorn's Lemma have turned out to follow in a direct and elementary way from Raoult's Open Induction [8]. The maximal or minimal elements characteristic of any invocation of Zorn's Lemma are eliminated, and it is made possible to pass from classical to intuitionistic logic. If the theorem has finite input data, then a finite partial order carries the required instance of induction, which thus only needs mathematical induction. Besides the revised Hilbert Programme a la Kreisel and Feferman, inspirations come from the work on combinatorics by U. Berger and Coquand [1, 3]; from Coste, Lombardi, and Roy's dynamical algebra [4]; and from the interplay between pointwise and point-free topology in Sambin's basic picture [10]. In particular there are striking parallels to Maietti and Sambin's two-level foundations with a forget-restore option [2, 7, 6], and to Sambin's appeal for allowing the use of ideal objects in real mathematics once this is approved by, say, appropriate conservativity [9, 11]. This partially is joint work with F. Ciraulo, N. Gambino, M. Hendtlass, and D. Rinaldi.
1. Ulrich Berger. A computational interpretation of open induction. In F. Titsworth, editor, Proceedings of the Ninetenth Annual IEEE Symposium on Logic in Computer Science, pages 326-334. IEEE Computer Society, 2004.
2. Francesco Ciraulo and Giovanni Sambin. Finiteness in a minimalist foundation. In Types for proofs and programs, volume 4941 of Lecture Notes in Comput. Sci., pages 51-68. Springer, Berlin, 2008.
3. Thierry Coquand. Constructive topology and combinatorics. In Constructivity in computer science (San Antonio, TX, 1991), volume 613 of Lecture Notes in Comput. Sci., pages 159-164. Springer, Berlin, 1992.
4. Michel Coste, Henri Lombardi, and Marie-Francoise Roy. Dynamical method in algebra: Effective Nullstellensaetze. Ann. Pure Appl. Logic, 111(3):203{256, 2001.
5. Matthew Hendtlass and Peter Schuster. A direct proof of Wiener's theorem. In S. B. Cooper, A. Dawar, and B. Loewe, editors, How the World Computes. Turing Centenary Conference and Eighth Conference on Computability in Europe, volume 7318 of Lect. Notes Comput. Sci., pages 294-303, Berlin and Heidelberg, 2012. Springer. Proceedings, CiE 2012, Cambridge, UK, June 2012.
6. Maria Emilia Maietti. A minimalist two-level foundation for constructive mathematics. Ann. Pure Appl. Logic, 160(3):319{354, 2009.
7. Maria Emilia Maietti and Giovanni Sambin. Toward a minimalist foundation for constructive mathematics. In L. Crosilla and P. Schuster, editors, From Sets and Types to Topology and Analysis, volume 48 of Oxford Logic Guides, pages 91{114. Oxford: Oxford University Press, 2005.
8. Jean-Claude Raoult. Proving open properties by induction. Inform. Process. Lett., 29(1):19-23, 1988.
9. Giovanni Sambin. Steps towards a dynamic constructivism. In P. Gaerdenfors et al., editor, In the Scope of Logic, Methodology and Philosophy of Science, volume 315 of Synthese Library, pages 263-286, Dordrecht, 2002. Kluwer. 11th International Congress of Logic, Methodology and Philosophy of Science. Krakow, Poland, August 1999.
10. Giovanni Sambin. Some points in formal topology. Theoret. Comput. Sci., 305(1-3):347-408, 2003.
11. Giovanni Sambin. Real and ideal in constructive mathematics. In Epistemology versus ontology, volume 27 of Log. Epistemol. Unity Sci., pages 69{85. Springer, Dordrecht, 2012.
Attendance
From Bath:
Anupam Das
Cai Wingfield
Alessio Guglielmi
Willem Heijltjes
Jim Laird
From Birmingham:
Liang-Ting Chen
Olle Fredriksson
From Jaist:
Takako Nemoto
From Leeds:
Peter Schuster
From Swansea:
Arnold Beckmann
Ulrich Berger
Jens Blanck
Martin Churchill
Fredrik Nordvall Forsberg
Roger Hindley
Phillip James
Andrew Lawrence
Peter Mosses
Caspar Poulson
Monika Seisenberger
Paolo Torrini
Ferdinand Vesley
See all Wessex sites involved and meetings so far.