2002 Clifford Lectures 

Mathematical Logic for Computer Science

Abstracts

The "Greats" (Brouwer, Kolmogorov, Goedel) raised in the 1930s a complex of fundamental questions of explicit logic which we can now characterize as determining the exact relation between deduction and computation. One such fundamental relation, stemming from the consistency proofs, has already become a cornerstone of Computer Science. This is the Curry-Howard Isomorphism between typed lambda-terms and intuitionistic deductions.

The Curry-Howard Isomorphism does not capture the self-referential mechanisms available in deductions in sufficiently rich formal systems and in programming languages. A discovery of a natural system of self-referential proof terms, which we call "proof polynomials", was essential in our recent solution to the famous open problem of Gödel (1933) concerning formalization of provability. Proof polynomials considerably extend the Curry-Howard Isomorphism and lead to a joint calculus of propositions and proofs which unifies several previously unrelated areas. We will explain this solution, and why it is likely to change our conception of the appropriate syntax and semantics for lambda-calculus based programming languages, automated deduction and formal verification, reasoning about knowledge,etc.

We use combinators to give a simple formulation of type-free applicative (i.e. functional programming) systems. The classical SK combinators allow all partial recursive functions to be represented, while the BCK combinators (corresponding to `affine' lambda calculus) normalize in linear time. To capture some intermediate classes of functions, we recall the notion of *Linear Combinatory Algebra* introduced by the present author (and first presented in a talk at MFPS `97) which gives a presentation of the computational ideas of Multiplicative Exponential Linear Logic in a combinatory format. Since standard combinatory logic can be interpreted into Linear Combinatory Logic, once again all recursive functions can be represented. However, in this refined setting we have more scope for capturing intermediate possibilities. If we omit both the comultiplication and the dereliction combinators, we get Elementary Combinatory Logic, which characterizes elementary time computation in a strong sense. More interestingly, if we remove comultiplication, and replace the contraction combinator by a `bounded' or `predicative' version, in which the number of copies made has to be decided a priori, then we obtain a system which characterizes polynomial time. This system is related to Lafont's `Soft Linear Logic'. It is a strikingly simple system, which admits a very simple and natural notion of model, by contrast to Girard's system of Light Linear Logic, which has to add a new modality to compensate for the loss of dereliction. For this reason, it may prove useful in obtaining a semantic perspective on complexity classes.

A simple type A is called finitely generated iff there is a finite set G of closed λ-terms (not necessarily of type A) such that all closed terms of type A are (modulo β,η-conversion) applicative combinations of elements of G. Statman asked to show that the `monster' type (((ω → ω) → ω) → ω) → (ω → ω) is not finitely generated. We outline a proof by Th. Joly of this fact along the following lines.

Given any full type structure MX over finite ground domains X, one can ask whether an element is lambda definable by a closed term. Let

D(A,X)= {f ε MAX | f is definable}.

The so-called Plotkin conjecture stated that lambda definability is decidable, in other words that D as a function of A and X is computable.  Loader refuted this conjecture by showing that the map A |→ D(A,X) is not computable for a fixed (and small) X.

Joly pointed out a strong link between finite generation and the orthogonal restriction of lambda-definability in the following result

     A is finitely generated iff  the map  X |→ D(A,X) is computable.

Moreover, by his analysis it can be decided which types A are finitely generated and the monster type is not among them.

We present higher-order accurate Taylor series methods for rigid body simulations which perform single-step updates by calculating the average rotation vector during a time step.  The higher-order Taylor series terms serve to correct for the non-linearity of rigid body motion. Our algorithms exactly preserve angular momentum, and approximately preserve energy.  We further present a method based on the Poinsot ellipsoid to readjust orientation as as to exactly preserve energy.          

The formulas for the Taylor series methods are established in the setting of general Lie groups so similar higher-order accurate methods apply to simulations in arbitrary Lie groups.  The proofs are based on the derivative of the exponential function.

Experiments on the simulation of a freely moving, wobbling, rigid body compare our Taylor series methods and energy preservation with a variety of other methods, including symplectic methods.           

Most of the talk is accessible to an audience without knowledge of Lie Groups.

We suggest a general proof-theoretical setting--based on well-founded proof orderings--which allows one an abstract view of notions developed in the theory of rewriting, including canonical inference, reduced formulae, critical formulae, redundancy, and completion.  The "canonical basis" of a theory is characterized as (1) theorems that appear as assumptions in minimal proofs; (2) non-redundant theorems; (3) conclusions of trivial proofs; and (4) the limit of a completion process.

Cryptographic protocols are short sequences of messages that use cryptography to allow principals to authenticate each other and agree on new shared secrets.  They are fundamental to security in electronic commerce and networked systems generally.  However, it is tricky to be sure exactly what they achieve, in the presence of an attacker, or in some cases whether they achieve any useful security goal.  Problems may arise even with strong cryptography.

In this talk, we use the strand space formalism to study cryptographic protocols.  We present a widely applicable method, which we call the authentication test method, to determine exactly what authentication and secrecy goals a protocol achieves.  We will also explain how to use the same ideas as a heuristic to create new (demonstrably correct) protocols, developing a new electronic commerce protocol as an example.  This is joint work with F. Javier Thayer.

We start with the foundational problem ``What is computation?'' and arrive at the ASM paradigm and the ASM thesis: for every computer system A, at any fixed abstraction level, there is an ASM B that is behaviorally equivalent to A and, in particular, simulates A step for step.  We will mention also some theoretical and experimental validation of the thesis.

The P versus NP problem is the best known unsolved problem in theoretical computer science with deep implications about the limits of feasible computations and the nature of mathematics. Its solution will be rewarded by a million dollar prize from the Clay Foundation which ranks it among the seven most important open problems in mathematics. More important, its solution will be a major step towards understanding what is feasibly computable and, indirectly, the limits of feasible rational reasoning .The solution will also clarify how much harder is it to compute a proof of a theorem than to check the correctness of a proof.

At the same time, the P versus NP question is only one of many other important " separation " problems of the rich structure of natural complexity classes below exponential space. It is believed that these complexity classes are all different, but there are no proofs (yet) to justify these beliefs.

This talk will revisit the P versus NP problem in this broader setting, review the attempts to solve the separation problems, explore connections between these problems, and review their relation to descriptive complexity and interactive proofs.

There are many examples in real life of formal systems that support certain constructions or proofs, but that do not provide direct support for remembering what was done so that it does not have to be redone in the future.  The task of publication and citation is typically left to some metasystem that is provided as an afterthought.  Examples include programming languages (class libraries), automated deduction systems (lemma libraries), and mathematics (journal publication).

In this talk I will develop the idea of publication/citation from a proof-theoretic perspective.  In this context we can regard publication/citation as an optimization, essentially an instance of common subexpression elimination on proof terms. I will describe a simple complete proof system for universal Horn equational logic with two new proof rules "publish" and "cite". These rules allow the inclusion of proved theorems in a library and later citation with specialization by a given substitution. The novel twist, however, is that the combinator corresponding to the publish rule wraps the proof term to inhibit beta-reduction upon citation, giving a "citation token" that is type-equivalent to the original proof but that does not explicitly specialize when cited. This is how common subexpression elimination is achieved.

The weakening rule that forgets a library entry, which would normally be considered trivial, becomes quite interesting in this context.  It must replace all citations of the forgotten lemma with the various specializations of the original proof.  The corresponding combinator does this simply by unwrapping all occurrences of the citation token, allowing the deferred beta-reductions to take place.

There have been various interactions between two person games and logic.  Examples include the well known Ehrenfuecht-Fraisse games for first order logic.  However there are other applications too, both of games to logic and of logic to games, the last being due to the speaker.  Moreover, there are game theoretic semantics for the Hintikka-Sandu IF logics as well as for related logics which include for instance partial information logics, which we have developed jointly with Jouko Vaannanen. Game theoretic semantics can also be given for D-structures which generalize classical, intuitionistic, and the *-logic of Ehrenfeucht. We will give on overview.

We define a restriction LHA of Heyting arithmetic HA with the property that all extracted programs are feasible. The restrictions consist in linearity and ramification requirements.

In automated verification one uses algorithmic techniques to establish the correctness of the design with respect to a given property. Automated verification is based on a small number of key algorithmic ideas, tying together graph theory, automata theory, and logic. In this self-contained talk I will describe how this "holy trinity" gave rise to automated-verification tools.

Click here to register

Back to Clifford Lectures page