Lecture Notes in Computer Science 5028 CommencedPublicationin1973 FoundingandFormerSeriesEditors: GerhardGoos,JurisHartmanis,andJanvanLeeuwen EditorialBoard DavidHutchison LancasterUniversity,UK TakeoKanade CarnegieMellonUniversity,Pittsburgh,PA,USA JosefKittler UniversityofSurrey,Guildford,UK JonM.Kleinberg CornellUniversity,Ithaca,NY,USA AlfredKobsa UniversityofCalifornia,Irvine,CA,USA FriedemannMattern ETHZurich,Switzerland JohnC.Mitchell StanfordUniversity,CA,USA MoniNaor WeizmannInstituteofScience,Rehovot,Israel OscarNierstrasz UniversityofBern,Switzerland C.PanduRangan IndianInstituteofTechnology,Madras,India BernhardSteffen UniversityofDortmund,Germany MadhuSudan MassachusettsInstituteofTechnology,MA,USA DemetriTerzopoulos UniversityofCalifornia,LosAngeles,CA,USA DougTygar UniversityofCalifornia,Berkeley,CA,USA GerhardWeikum Max-PlanckInstituteofComputerScience,Saarbruecken,Germany Arnold Beckmann Costas Dimitracopoulos Benedikt Löwe (Eds.) Logic and Theory of Algorithms 4th Conference on Computability in Europe, CiE 2008 Athens, Greece, June 15-20, 2008 Proceedings 1 3 VolumeEditors ArnoldBeckmann SwanseaUniversity SingletonPark,Swansea,SA28PP,UnitedKingdom E-mail:[email protected] CostasDimitracopoulos UniversityofAthens UniversityCampus,AnoIlisia,15771Athens,Greece E-mail:[email protected] BenediktLöwe UniversiteitvanAmsterdam PlantageMuidergracht24,1018TVAmsterdam,TheNetherlands E-mail:[email protected] LibraryofCongressControlNumber:2008928722 CRSubjectClassification(1998):F.1,F.2.1-2,F.4.1,G.1.0,I.2.6,J.3 LNCSSublibrary:SL1–TheoreticalComputerScienceandGeneralIssues ISSN 0302-9743 ISBN-10 3-540-69405-6SpringerBerlinHeidelbergNewYork ISBN-13 978-3-540-69405-2SpringerBerlinHeidelbergNewYork Thisworkissubjecttocopyright.Allrightsarereserved,whetherthewholeorpartofthematerialis concerned,specificallytherightsoftranslation,reprinting,re-useofillustrations,recitation,broadcasting, reproductiononmicrofilmsorinanyotherway,andstorageindatabanks.Duplicationofthispublication orpartsthereofispermittedonlyundertheprovisionsoftheGermanCopyrightLawofSeptember9,1965, initscurrentversion,andpermissionforusemustalwaysbeobtainedfromSpringer.Violationsareliable toprosecutionundertheGermanCopyrightLaw. SpringerisapartofSpringerScience+BusinessMedia springer.com ©Springer-VerlagBerlinHeidelberg2008 PrintedinGermany Typesetting:Camera-readybyauthor,dataconversionbyScientificPublishingServices,Chennai,India Printedonacid-freepaper SPIN:12278411 06/3180 543210 Preface CiE 2008: Logic and Theory of Algorithms Athens, Greece, June 15–20,2008 Computability in Europe (CiE) is an informal network of European scientists working on computability theory, including its foundations, technical develop- ment, and applications. Among the aims of the network is to advance our the- oretical understanding of what can and cannot be computed, by any means of computation. Its scientific vision is broad: computations may be performed with discrete or continuous data by all kinds of algorithms, programs, and ma- chines. Computations may be made by experimenting with any sort of physical system obeying the laws of a physical theory such as Newtonian mechanics, quantum theory, or relativity. Computations may be very general, depending on the foundations of set theory; or very specific, using the combinatorics of finite structures. CiE also works on subjects intimately related to computation, especially theories of data and information, and methods for formal reasoning about computations. The sources of new ideas and methods include practical developments in areas such as neural networks, quantum computation, natural computation, molecular computation, computational learning. Applications are everywhere,especially,inalgebra,analysisandgeometry,ordatatypesandpro- gramming. Within CiE there is general recognition of the underlying relevance of computability to physics and a broad range of other sciences, providing as it does a basic analysis of the causal structure of dynamical systems. Thisvolume,LogicandTheoryofAlgorithms,istheproceedingsofthefourth ina series ofconferencesofCiE that washeld atthe UniversityofAthens, June 15–20,2008. ThefirstthreemeetingsofCiEwereattheUniversityofAmsterdamin2005, at the University of Wales Swansea in 2006, and at the University of Siena in 2007.Theirproceedings,editedin2005byS.BarryCooper,BenediktLo¨we,and Leen Torenvliet, in 2006 by Arnold Beckmann, Ulrich Berger, Benedikt Lo¨we, and John V. Tucker, and in 2007 by S. Barry Cooper, Benedikt Lo¨we, and Andrea Sorbi, were published as Springer Lecture Notes in Computer Science, Volumes 3526, 3988, and 4497, respectively. VI Preface CiE and its conferences have changed our perceptions of computability and itsinterfacewithotherareasofknowledge.Thelargenumberofmathematicians andcomputerscientistsattendingtheseconferencehadtheirviewofcomputabil- ity theory enlarged and transformed: they discovered that its foundations were deeper andmore mysterious,its technicaldevelopmentmorevigorous,its appli- cations wider and more challenging than they had known. The Athens meeting promised to extend and enrich that process. The annual CiE conference, based on the Computability in Europe network, has become a major event, and is the largest international meeting focused on computability theoretic issues. The series is coordinated by the CiE Conference Series Steering Committee: Arnold Beckmann (Swansea) Paola Bonizzoni (Milan) S. Barry Cooper (Leeds) Benedikt Lo¨we (Amsterdam, Chair) Elvira Mayordomo (Zaragoza) Dag Normann (Oslo) Peter van Emde Boas (Amsterdam) We will reconvene 2009 in Heidelberg and 2010 in Ponta Delgada (Ac¸ores). Structure and Programme of the Conference The conference was based on invited tutorials and lectures, and a set of special sessions on a range of subjects; there were also many contributed papers and informalpresentations.This volume contains25 ofthe invited lectures and 33% of the submitted contributed papers, all of which have been refereed. There will be a number of post-proceedings publications, including special issues of Theory of Computing Systems, Archive for Mathematical Logic, and Journal of Algorithms. Tutorials John V. Tucker (Swansea), Applied Computability: A European Perspective Moshe Y. Vardi (Houston TX), Logic, Automata, Games, and Algorithms Opening Lecture Keith Devlin (Stanford CA), The Computing Species Invited Plenary Talks Rosalie Iemhoff (Utrecht), Kripke Models for Constructive Set Theory Antonina Kolokolova (St. John’s NL), Many Facets of Complexity in Logic Johann Makowsky (Haifa), Uniform Algebraic Reducibilities Between Parameterized Numeric Graph Invariants Dag Normann (Oslo), 50 Years of Continuous Functionals PrakashPanangaden(Montr´ealQC), Domain Theory and the Causal Structure of Space-Time Preface VII Christos Papadimitriou (Berkeley CA), On Nash, Brouwer, and Other Non-Constructive Proofs Jiˇr´ıWiedermann (Prague) and Jan van Leeuwen (Utrecht), How We Think of Computing Today Special Sessions Algorithmsin the History of Mathematics,organizedbyJensHøyrupand Karine Chemla Andr´eaBr´eard(Lille), A Summation Algorithm from 11th Century China: Pos- sible Relations Between Structure and Argument Marouane Ben Miled (Tunis): Preuves et Algorithmes Dans Un Contexte Alg´ebrique, Entre le 9e et le 12e Si`ecle, Harold Edwards (New York), Kronecker’s Algorithmic Mathematics Jens Høyrup (Roskilde), The Algorithm Concept – Tool for Historiographic In- terpretation or Red Herring? Formalising Mathematics and Extracting Algorithms from Proofs, or- ganized by Henk Barendregt and Monika Seisenberger JohnHarrison(Hillsboro),New(Un)Decidability Resultsfrom theFormalization of Mathematics Pierre Letouzey (Paris), Extraction in Coq: An Overview Lawrence C. Paulson (Cambridge), The Relative Consistency of the Axiom of Choice Mechanized Using Isabelle/ZF Christophe Raffalli (Le Bourget du Lac), Krivine’s Realizability: From Storage Operators to the Intentional Axiom of Choice Higher-Type Recursion and Applications,organizedbyUlrichBergerand Dag Normann LarsKristiansen(Oslo),Recursion in Higher Types and Resource Bounded Tur- ing machines John Longley (Edinburgh), Interpreting Localized Computational Effects Using Higher Type Operators Ralph Matthes (Toulouse), Recursion on Nested Datatypes in Dependent Type Theory Colin Riba (Sophia Antipolis), Rewriting with Unions of Reducibility Families Algorithmic Game Theory, organized by Elias Koutsoupias and Bernhard von Stengel Constantinos Daskalakis (Berkeley CA), Computing Equilibria in Large Games We Play Hugo Gimbert (Bordeaux), Solving Simple Stochastic Games Rahul Savani (Warwick), A Simple P-Matrix Linear Complementarity Problem for Discounted Games Troels Bjerre Sørensen (Aarhus), Deterministic Graphical Games Revisited Quantum Algorithms and Complexity, organizedby Viv Kendonand Bob Coecke VIII Preface Dan Browne (London), A Classical Analogue of Measurement-Based Quantum Computation? Jiannis K. Pachos (Leeds), Why Should Anyone Care About Computing with Anyons? PeterRichter(Orsay),The Quantum Complexity of Markov Chain Monte Carlo Matthias Christandl (Cambridge), A Quantum Information-Theoretic Proof of theRelationBetweenHorn’sProblemandtheLittlewood-Richardson Coefficients Biology and Computation, organized by Natasha Jonoska and Giancarlo Mauri Alessandra Carbone (Paris), Genome Synthesis and Genomic Functional Cores Matteo Cavaliere (Trento), Computing by Observing Erzs´ebet Csuhaj-Varju´ (Budapest), P Automata: Membrane Systems as Acceptors Mark Daley (London ON), On the Processing Power of Protozoa Organization and Acknowledgements The conference CiE 2008 was organized by: Dionysis Anapolitanos (Athens), ArnoldBeckmann(Swansea),CostasDimitracopoulos(Athens, Chair),Michael Mytilinaios (Athens) †, Thanases Pheidas (Heraklion), Stathis Zachos (Athens and New York NY). The Programme Committee was chaired by Arnold Beckmann and Costas Dimitracopoulos: Luigia Aiello (Rome) Elvira Mayordomo (Zaragoza) Thorsten Altenkirch (Nottingham) Franco Montagna (Siena) Klaus Ambos-Spies (Heidelberg) Michael Mytilinaios (Athens) † Giorgio Ausiello (Rome) Mogens Nielsen (Aarhus) Arnold Beckmann (Swansea) Isabel Oitavem (Lisbon) Lev Beklemishev (Moscow) Catuscia Palamidessi(Palaiseau) Paola Bonizzoni (Milan) Thanases Pheidas (Heraklion) Stephen A. Cook (Toronto ON) Ramanujam (Chennai) Barry Cooper (Leeds) Andrea Schalk (Manchester) Costas Dimitracopoulos (Athens) Uwe Sch¨oning (Ulm) Rod Downey (Wellington) Helmut Schwichtenberg (Munch) Elias Koutsoupias (Athens) Alan Selman (Buffalo NY) Orna Kupferman (Jerusalem) Andrea Sorbi (Siena) Sophie Laplante (Orsay) Ivan Soskov (Sofia) Hannes Leitgeb (Bristol) Christopher Timpson (Oxford) Benedikt Lo¨we (Amsterdam) Stathis Zachos (Athens and New York NY) We are delighted to acknowledge and thank the following for their essential financial support: Bank of Greece, Graduate Program in Logic and Algorithms (MPLA), Hellenic Ministry of Education, John S. Latsis Foundation, National Preface IX and Kapodistrian University of Athens, Rizareio Foundation, The Elsevier Foundation. The high scientific quality of the conference was possible through the con- scientious work of the Programme Committee, the special session organizers, and the referees. We are grateful to all members of the Programme Committee for their efficient evaluations and extensive debates, which established the final programme. We also thank the following referees: Jesus Aranda Bhaskar DasGupta Hans Hyttel Andreas Abel Constantinos Eyke Hu¨llermeier Peter Aczel Daskalakis Rosalie Iemhoff Klaus Aehlig Adam Day Natasha Jonoska Pilar Albert Alberto Dennunzio Reinhard Kahle Spyridon Ilias Diakonikolas Eirini Kaldeli Antonakopoulos Arnaud Durand Christos Kapoutsis Luis Antunes Martin Dyer Basil Karadais Toshiyasu Arai Mirna Dzamonja Jarkko Kari Argimiro Arratia Martin Escardo Elham Kashefi Albert Atserias Michael Fellows Viv Kendon David Aubin Fernando Ferreira Thomas Kent Olivier Bournez Jean-Christophen Iordanis Kerenidis John Baez Filliatre Bakhadyr Khoussainov Evangelos Bampas Joe Fitzsimons Peter Koepke Freiric Barral Ga¨elle Fontaine George Koletsos Ulrich Berger Enrico Formenti Konstantinos Kollias Riccardo Biagioli Dimitris Fotakis Costas Koutras Guillaume Bonfante Pierluigi Frisco Simon Kramer Andrey Bovykin Hristo Ganchev Natalio Krasnogor Vasco Brattka Parmenides Werner Kuich Mark Braverman Garcia Cornejo Piyush P. Kurur Thomas Brihaye William Gasarch Geoffrey LaForte Gerth Brodal Yiannis Michael Lampis Dan Browne Giannakopoulos Troy Lee Manuel Campagnolo Sergey Goncharov Alberto Leporati Douglas Cenzer Joel David Hamkins David Lester Arkadevn Aram Harrow Paolo Liberatore Chattopadhyay Chrysafis Hartonas Kamal Lodaya Panagiotis Cheilaris Bastiaan Heeren Maria Lopez-Valdes Luca Chiarabini Christoph Heinatsch Salvador Lucas Chi Tat Chong Denis Hirschfeldt Jack H. Lutz Petr Cintula John Hitchcock Guillaume Malod F´elix Costa Peter Hoyer Evangelos Markakis Paola D’Aquino Simon Huber Euripides Markou Bemb´e Daniel Franz Huber Giancarlo Mauri Olivier Danvy Martin Hyland Alexander Meduna X Preface Klaus Meer Ion Petre Sebastiaan Terwijn Emanuela Merelli Mauro Piccolo Neil Thapen Wolfgang Merkle George Pierrakos P.S. Thiagarajan Dale Miller Natacha Portier Jacobo Toran Peter Bro Miltersen Katerina Potika Edmondo Trentin Eugenio Moggi Florian Ranzi Trifon Trifonov Antonio Montalban Diana Ratiu Tarmo Uustalu Malika More Kenneth Regan Pierre Valarcher Philippe Moser Jan Reimann Frank Valencia Luca Motto Ros Gerhard Reinelt Peter van Emde Boas Anders Mo¨ller Martin Roetteler Angelina Vidali Margherita Napoli Jeremie Roland Nicolas Vieille Vincent Nesme David Rydeheard Anastasios Viglas Phuong Nguyen Markus Sauermann Giuseppe Vizzari Long Nguyen Ruediger Schack Paul Voda Andre Nies Stefan Schimanski Vladimir Vyugin Karl-Heinz Niggl Peter Schuster Andreas Weiermann Tobias Nipkow Monika Seisenberger Pascal Weil Christos Nomikos Domenico Senato Philip Welch Martin Ochoa Sunil Easaw Simon Thomas Wilke Carlos Olarte Reed Solomon Joost Winter Martin Otto Ludwig Staiger Ronald de Wolf Aris Pagourtzis Frank Stephan Guohua Wu Jens Palsberg Lutz Strassburger Yue Yang Prakash Panangaden Aaron Stump Alberto Zanardo Katia Papakonstan Kristian Støvring Liyu Zhang -tinopoulou Kohei Suenaga Martin Ziegler Nikos Papaspyrou Nik Sultana Albert Ziegler Gheorghe Paun S.P. Suresh Vittorio Amos Ziparo A. Pavan Deian Tabakov Sylvain Perifel Aris Tentes We thank Andrej Voronkov for his EasyChair system which facilitated the work of the Programme Committee and the editors considerably. April 2008 Arnold Beckmann Costas Dimitracopoulos Benedikt Lo¨we