[FOM] Girard's new program

[Andre Scedrov]

Alasdair asks what is the basic new advance in foundational studies 
offered by ludics. 

I will try to describe very informally, in broad strokes, what I think is 
the _question_ that ludics is aiming to answer. Regarding the proposed answer,
one does have to tackle the references David Pym and I listed earlier, 
including: 

Jean-Yves Girard. Locus Solum: From the rules of logic to the logic of rules. 
Mathematical Structures in Computer Science 11(3): 301-506 (2001). 

The question that ludics is aiming to answer is "What is a logical proof?". 
So far, ludics has offered an answer in the case of propositional logical 
proofs, including second-order propositional proofs. 

One might say, what is there to do other than cite the usual formal 
systems and the usual inductive definitions of formal derivations and proofs. 
Here are the rules, and if you follow them, you will have a logical proof. 
This is the answer of the rules of logic. 

Ludics is aiming to answer a deeper question: what are the general invariance
principles from which logical rules come about? Imagine having a conversation
with Gentzen, or perhaps even Aristotle, asking them just why and how did they
arrive at such and such a formulation of logical rules. Was there a method? 
Are there structural restrictions that one must observe? Was Gentzen somehow 
forced to give his particular answer? That is, is there the logic of rules? 

The question is not new. It was discussed by Lorenzen in the 1950s, who 
offered an answer in terms of dialogues, debates, and strategies. Ludics 
continues this direction, drawing on modern developments in logic 
(such as realizability interpretations of intuitionistic logic, and in 
particular formalized realizability) and in computer science. 

What does computer science have to do with this? 

One connection is provided by query-based computational paradigms such as 
logic programming. Instead of our imaginary conversation with Gentzen, let 
us ask what is Prolog basically doing when given a Horn clause. One answer 
is that it is searching for a cut-free proof. But the unsuccessful searches, 
what do they produce? And how is the backtracking done and other branches 
explored? On which structure is this happening? Can it be optimized? With 
respect to what structure? Here the work of Dale Miller and of Jean-Marc 
Andreoli provides information on some of the desired invariance properties. 
[J.-M. Andreoli. Logic programming with focusing proofs in linear logic. 
Journal of Logic and Computation 2(3), 1992.] 

Another connection with computer science is provided by semantics of 
functional programming languages. Are there mathematical conditions on 
models that characterize those objects in models that denote programming
language expressions? Can one give purely semantic description of models 
all of whose objects denote programming language expressions? This is 
the question of so-called full abstraction, more recently also called
full completeness. This question is answered in the papers by Hyland and 
Ong and by Abramsky, Jagadeesan, and Malacaria I mentioned earlier. 
Their answers are formulated in terms of games and strategies, in a much 
more refined form of Lorenzen's approach. The Hyland-Ong approach provides
a somewhat tighter characterization of the two, and this is perhaps the 
closest technical precursor to ludics. The paper by Faggian and Hyland 
in CSL 2002 mentioned by Pym provides a detailed decription of the 
relationship between the work of Hyland and Ong and certain aspects 
of ludics. 

  
  Andre Scedrov