LICS on Wednesday

Detailed program
Wednesday July 24th, 2002
See also the unified by-slot program

All sessions take place in auditorium 1.

Session 9

Chair: Samson Abramsky

09:00-09:30  C.-H. L. Ong, Oxford U, UK
Observational equivalence of 3rd-order idealized Algol is decidable
We prove that observational equivalence of 3rd-order finitary Idealized Algol (IA) is decidable using Game Semantics. By modelling state explicitly in our games, we show that the denotation of a term M of this fragment of IA (built up from finite base types) is a compactly innocent strategy-with-state i.e. the strategy is generated by a finite view function fM. Given any such fM, we construct a real-time deterministic pushdown automata (DPDA) that recognizes the complete plays of the knowing-strategy denotation of M. Since such plays characterize observational equivalence, and there is an algorithm for deciding whether any two DPDAs recognize the same language, we obtain a procedure for deciding observational equivalence of 3rd-order finitary IA. This algorithmic representation of program meanings, which is compositional, provides a foundation for model-checking a wide range of behavioural properties of IA and other cognate programming languages. Another result concerns 2nd-order IA with full recursion: we show that observational equivalence for this fragment is undecidable.

09:30-10:00  Martin Hyland, U Cambridge, UK
Andrea Schalk, U Cambridge, UK
Games on graphs and sequantially realizable functionals
We present a new category of games on graphs and derive from it a model for Intuitionistic Linear Logic. Our category has the computational flavour of concrete data structures but embeds fully and faithfully in an abstract games model. It differs markedly from the usual Intuitionistic Linear Logic setting for sequential algorithms. However, we show that with a natural exponential we obtain a model for PCF essentially equivalent to the sequential algorithms model. We briefly consider a more extensional setting and the prospects for a better understanding of the Longley Conjecture.

10:00-10:30  Olivier Laurent, U Paris VII, France
Polarized games
We generalize the intuitionistic Hyland-Ong games to a notion of polarized games allowing games with plays starting by proponent moves. The usual constructions on games are adjusted to fit this setting yielding a game model for polarized linear logic with a definability result. As a consequence this gives a complete game model for various classical systems: LC, lambda-mu calculus, ... for both call-by-name and call-by-value evaluations.

Session 10

Chair: Andre Scedrov

11:00-11:30  Abbas Edalat, Imperial College, UK
Andre Lieutier, Dassault Systemes Provence and LMC/IMAG, France
Domain theory and differential calculus (functions of one variable)
We introduce a data type for differentiable functions in the framework of domain theory. Using a new structure, called tie of maps, which provide finitary information about the differential properties of a Scott continuous map, we define the derivative of a Scott continuous function on the domain of intervals, which is itself a Scott continuous function. This leads to a domain-theoretic generalization of the fundamental theorem of calculus. The central part of this work is to construct a domain for differentiable real valued functions of a real variable. The classical C¹ functions, equipped with its C¹ norm, is embedded into the set of maximal elements of this domain, which is a countably based bounded complete continuous domain with an effective structure. The construction can be generalized to Ck and C functions and, in future, to functions of several variables and analytic functions. While the question of computability for differentiable functions have been studied in the literature, this seems to be the first time that a proper data type for differential calculus is proposed which brings smooth mathematics in the realm of domain theory and type theory. As an immediate application, we present a domain-theoretic and effective generalization of Picard's theorem, which provides a data type and an algorithm for solving differential equations given by a vector field and an initial condition. At each step of computation of this algorithm, one gets an approximation which is an interval piecewise polynomial function with rational coefficients that provides precise information on the solution.

11:30-12:00  Alex Simpson, U Edinburgh, UK
Computational adequacy for recursive types in models of intuitionistic set theory
We present a general axiomatic construction of models of FPC, a recursively typed lambda-calculus with call-by-value operational semantics. Our method of construction is to obtain such models as full subcategories of categorical models of intuitionistic set theory. This allows us to obtain a notion of model that encompasses both domain-theoretic and realizability models. We show that the existence of solutions to recursive domain equations, needed for the interpretation of recursive types, depends on the strength of the set theory. The internal set theory of an elementary topos is not strong enough to guarantee their existence. However, solutions to recursive domain equations do exist if models of intuitionistic Zermelo-Fraenkel set theory are used instead. We apply this result to interpret FPC, and we provide necessary and sufficient conditions on a model for the interpretation to be computationally adequate, i.e. for the operational and denotational notions of termination to agree.

12:00-12:30  Daniele Varacca, U Aarhus, Denmark
The powerdomain of indexed valuations
This paper is about combining nondeterminism and probabilities. We study this phenomenon from a domain theoretic point of view. In domain theory, nondeterminism is modeled using the notion of powerdomain, while probability is modeled using the powerdomain of valuations. Those two functors do not combine well, as they are. We define the notion of powerdomain of indexed valuations, which can be combined nicely with the usual nondeterministic powerdomain. We show an equational characterization of our construction. Finally we discuss the computational meaning of indexed valuations, and we show how they can be used, by giving a denotational semantics of a simple imperative language.

Session 11

Chair: Daniel Leivant

14:00-15:00  Stephen A. Cook, U Toronto, Canada
Invited lecture: Complexity Classes, Propositional Proof Systems, and Formal Theories

15:00-15:30  William Hesse, U Massachusetts, USA
Neil Immerman, U Massachusetts, USA
Complete problems for dynamic complexity classes
We present the first complete problems for dynamic complexity classes including the classes Dyn-FO and DynThC°, the dynamic classes corresponding to relational calculus and (polynomially bounded) SQL, respectively. The first problem we show complete for Dyn-FO is a single-step version of the circuit value problem (SSCV).
Of independent interest, our construction also produces a first-order formula, ζ, that is in a sense universal for all first-order formulas. Since first-order formulas are stratified by quantifier depth, the first-order formula ζ emulates formulas of greater depth by iterated application. As a corollary we obtain a fixed quantifier block, QBC, that is complete for all first-order quantifier blocks.

Session 12

Chair: Phokion Kolaitis

16:00-16:30  Albert Atserias, Techn. U of Catalonia, Spain
Unsatisfiable random formulas are hard to certify
We prove that every property of 3CNF formulas that implies unsatisfiability and is expressible in Datalog has asymptotic probability zero when formulas are randomly generated by taking 6n non-trivial clauses of exactly three literals uniformly and independently. Our result is a consequence of designing a winning strategy for Duplicator in the existential k-pebble game on the structure that encodes the 3CNF formula and a fixed template structure encoding a satisfiable formula. The winning strategy makes use of certain extension axioms that we introduce and hold almost surely on a random 3CNF formula. An interesting feature of our result is that it brings the fields of Propositional Proof Complexity and Finite Model Theory together. To make this connection more explicit, we show that Duplicator wins the existential pebble game on the structure encoding the Pigeonhole Principle and the template structure above. Moreover, we also prove that there exists a 2k-Datalog program expressing that an input 3CNF formula has a Resolution refutation of width k. As a consequence to our result and the known size-width relationship in Resolution, we obtain new proofs of the exponential lower bounds for Resolution refutations of random 3CNF formulas and the Pigeonhole Principle.

16:30-17:00  Michael Soltys, McMaster U, Canada
Stephen A. Cook, U Toronto, Canada
The proof complexity of linear algebra
We introduce three formal theories of increasing strength for linear algebra in order to study the complexity of the concepts needed to prove the basic theorems of the subject. We give what is apparently the first feasible proofs of the Cayley-Hamilton theorem and other properties of the determinant, and study the propositional proof complexity of matrix identities.

17:00-17:30  Daniel Leivant, Indiana U Bloomington, USA
Calibrating computational feasibility by abstraction rank
We characterize computationally the functions provable in second order logic with set existence restricted to natural classes of first order formulas. A classification of first-order set-existence by implicational rank yields a natural hierarchy of complexity classes within the class of Kalmar-elementary functions: The functions over {0,1}* constructively provable using set existence for formulas of implicational rank ≤k are precisely the functions computable in deterministic time O(expk(n)), where exp0=∪k(λn.nk), and expk+1=2expk. (For k>0 provability here is by normal deductions, a demonstrably necessary proviso.) In particular, set-existence for positive formulas yields exactly PTime. We thus obtain lean and natural formalisms for codifying feasible mathematics, which are expressive both in allowing second order definitions and reasoning, and in incorporating equational programming and reasoning about program convergence in a direct and uncoded style.
Through a formula-as-type morphism, we also obtain a link with lambda definability, which we exhibit in the full paper: The functions over {0,1}* definable in the polymorphic lambda calculus F2 over a base of type of words, using first-order type-arguments of rank ≤k, are precisely the functions computable in deterministic time O(expk(n)) (again, for k>0 definability is by normal λ-terms.) The poly-time case was proved (directly) in D. Leivant/J.Y. Marion, Lambda-caluclus characterizations of poly-time, Fund.Inform.19, pp. 167-184, 1993.

Session 13: Short Paper Session

Chair: Gordon Plotkin

17:30-17:40  Jonathan Ford, U New England, Australia
Ian A. Mason, U New England, Australia
Natarajan Shankar, SRI International, USA
Short presentation: Lessons learned from formal developments in PVS

17:40-17:50  Sylvain Soliman, INRIA Rocquencourt, France
Short presentation: CLP implementation of a phase model checker

17:50-18:00  Jens Chr. Godskesen, IT U of Copenhagen, Denmark
Thomas Hildebrandt, IT U of Copenhagen, Denmark
Vladimiro Sassone, U Sussex, UK
Short presentation: An overview of MR, a calculus of mobile resources

18:00-18:10  Claudia Faggian, U Cambridge, UK
Short presentation: Ludics dynamics: Designs and interactive observability

20:00-21:00  LICS Business Meeting