Ludics
Encyclopedia
In proof theory
, ludics is an analysis of the principles governing inference rules of mathematical logic
. Key features of ludics are its notion of compound connectives using a technique known as focusing or focalisation (invented by the computer scientist Jean-Marc Andreoli), and its use of locations or loci over a base instead of propositions.
More precisely, ludics tries to retrieve known logical connective
s, and proof behaviours, by following the paradigm of interactive computation, similarly to what is done in game semantics
to which it is closely related. By abstracting the notion of formulae and focusing of their concrete uses, that is distinct occurrences, it allows to provide an abstract syntax for computer science
, as loci can be seen as pointers on memory.
The primary technical achievement motivation of ludics is the discovery of a relationship between two natural, but distinct, notions of type or proposition.
The first view, which might be termed the proof-theoretic or Gentzen-style interpretation of propositions, says that the meaning of a proposition arises from its introduction and elimination rules. Focalization refines this viewpoint, by distinguishing between positive propositions, whose meaning arises from their introduction rules, and negative propositions, whose meaning arises from their elimination rules. In focused calculi, it is possible to define positive connectives by giving only their introduction rules, with the shape of the elimination rules being forced by this choice. (Symmetrically, negative connectives can be defined in focused calculi by giving only the elimination rules, with the introduction rules forced by this choice.)
The second view, which might be termed the computational or Brouwer-Heyting-Kolmogorov interpretation of propositions, takes the view that we fix a computational system up front, and then give a realizability
interpretation of propositions to give them constructive content. For example, a realizer for the proposition "A implies B" is a computable function which takes a realizer for A, and uses it to compute a realizer for B. Observe that realizability models characterize realizers for propositions in terms of their visible behavior, and not in terms of their internal structure.
Girard shows that for second-order affine linear logic, given a computational system with nontermination and error stops as effects, realizability and focalization give the same meaning to types.
Ludics was proposed by the logician Jean-Yves Girard
. His paper introducing Ludics, Locus solum: from the rules of logic to the logic of rules, has some features that may be seen as eccentric for a publication in mathematical logic
(such as illustrations of Positive Skunks). It has to be noted, that the intent of these features is to enforce the point of view of Jean-Yves Girard
at the time of its writing. And, thus, it offers to readers the possibility to understand ludics independently of their backgrounds.
Proof theory
Proof theory is a branch of mathematical logic that represents proofs as formal mathematical objects, facilitating their analysis by mathematical techniques. Proofs are typically presented as inductively-defined data structures such as plain lists, boxed lists, or trees, which are constructed...
, ludics is an analysis of the principles governing inference rules of mathematical logic
Mathematical logic
Mathematical logic is a subfield of mathematics with close connections to foundations of mathematics, theoretical computer science and philosophical logic. The field includes both the mathematical study of logic and the applications of formal logic to other areas of mathematics...
. Key features of ludics are its notion of compound connectives using a technique known as focusing or focalisation (invented by the computer scientist Jean-Marc Andreoli), and its use of locations or loci over a base instead of propositions.
More precisely, ludics tries to retrieve known logical connective
Logical connective
In logic, a logical connective is a symbol or word used to connect two or more sentences in a grammatically valid way, such that the compound sentence produced has a truth value dependent on the respective truth values of the original sentences.Each logical connective can be expressed as a...
s, and proof behaviours, by following the paradigm of interactive computation, similarly to what is done in game semantics
Game semantics
Game semantics is an approach to formal semantics that grounds the concepts of truth or validity on game-theoretic concepts, such as the existence of a winning strategy for a player, somewhat resembling Socratic dialogues or medieval theory of Obligationes. In the late 1950s Paul Lorenzen was the...
to which it is closely related. By abstracting the notion of formulae and focusing of their concrete uses, that is distinct occurrences, it allows to provide an abstract syntax for computer science
Computer science
Computer science or computing science is the study of the theoretical foundations of information and computation and of practical techniques for their implementation and application in computer systems...
, as loci can be seen as pointers on memory.
The primary technical achievement motivation of ludics is the discovery of a relationship between two natural, but distinct, notions of type or proposition.
The first view, which might be termed the proof-theoretic or Gentzen-style interpretation of propositions, says that the meaning of a proposition arises from its introduction and elimination rules. Focalization refines this viewpoint, by distinguishing between positive propositions, whose meaning arises from their introduction rules, and negative propositions, whose meaning arises from their elimination rules. In focused calculi, it is possible to define positive connectives by giving only their introduction rules, with the shape of the elimination rules being forced by this choice. (Symmetrically, negative connectives can be defined in focused calculi by giving only the elimination rules, with the introduction rules forced by this choice.)
The second view, which might be termed the computational or Brouwer-Heyting-Kolmogorov interpretation of propositions, takes the view that we fix a computational system up front, and then give a realizability
Realizability
Realizability is a part of proof theory which can be used to handle information about formulas instead of about the proofs of formulas. A natural number n is said to realize a statement in the language of arithmetic of natural numbers...
interpretation of propositions to give them constructive content. For example, a realizer for the proposition "A implies B" is a computable function which takes a realizer for A, and uses it to compute a realizer for B. Observe that realizability models characterize realizers for propositions in terms of their visible behavior, and not in terms of their internal structure.
Girard shows that for second-order affine linear logic, given a computational system with nontermination and error stops as effects, realizability and focalization give the same meaning to types.
Ludics was proposed by the logician Jean-Yves Girard
Jean-Yves Girard
Jean-Yves Girard is a French logician working in proof theory. His contributions include a proof of strong normalization in a system of second-order logic called system F; the invention of linear logic; the geometry of interaction; and ludics...
. His paper introducing Ludics, Locus solum: from the rules of logic to the logic of rules, has some features that may be seen as eccentric for a publication in mathematical logic
Mathematical logic
Mathematical logic is a subfield of mathematics with close connections to foundations of mathematics, theoretical computer science and philosophical logic. The field includes both the mathematical study of logic and the applications of formal logic to other areas of mathematics...
(such as illustrations of Positive Skunks). It has to be noted, that the intent of these features is to enforce the point of view of Jean-Yves Girard
Jean-Yves Girard
Jean-Yves Girard is a French logician working in proof theory. His contributions include a proof of strong normalization in a system of second-order logic called system F; the invention of linear logic; the geometry of interaction; and ludics...
at the time of its writing. And, thus, it offers to readers the possibility to understand ludics independently of their backgrounds.
External links
- Girard, J-Y, Locus solum: from the rules of logic to the logic of rules (.pdf), Mathematical Structures in Computer Science, 11, 301–506, 2001.
- Girard reading group at Carnegie-Mellon University (a wiki about Locus Solum)