Ludics
From Wikipedia, the free 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 connectives, 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.
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.
[edit] See also
[edit] External link
- Girard, J-Y, Locus solum: from the rules of logic to the logic of rules (.ps.gz), Mathematical Structures in Computer Science, 11, 301--506, 2001.
