| dbo:abstract
|
- In proof theory, ludics is an analysis of the principles governing inference rules of mathematical logic. Key features of ludics include notion of compound connectives, using a technique known as focusing or focalisation (invented by the computer scientist ), 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 on their concrete uses—that is distinct occurrences—it provides an abstract syntax for computer science, as loci can be seen as pointers on memory. The primary achievement 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 that takes a realizer for A, and uses it to compute a realizer for B. 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 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. (en)
- Na Teoria da Prova, Ludics é uma análise dos princípios que controlam as regras da lógica matemática. As principais características do Ludics são a noção de conectivos compostos usando uma técnica conhecida como “focalização” (inventada pelo cientista da computação ), e seu uso de locais ou loci sobre uma base ao invés de proposições. Mais precisamente, Ludics tenta reter os conectivos lógicos conhecidos e comportamento de prova, ao seguir o paradigma da computação interativa, similar ao que é feito na semântica dos jogos, a qual é fortemente relacionado. Ao abstrair a noção de fórmulas e focar nos seus usos concretos, ou seja, ocorrências distintas, ela permite prover uma sintaxe abstrata para a ciência da computação, já que os loci podem ser vistos como ponteiros ou memória. A primeira motivação de objetivos técnicos do Ludics é a descoberta da relação entre duas noções naturais, porém distintas, de tipo ou proposição. A primeira visão, que pode ser denominada como a interpretação de proposições da teoria de prova (ou “ao estilo-”), diz que o significado de uma proposição surge de suas regras de introdução e eliminação. A “focalização” refina este ponto de vista, ao diferenciar as proposições positivas, cujo significado surge de suas regras de introdução, das proposições negativas, cujo significado surge de suas regras de eliminação. Nos cálculos focados, é possível definir conectivos positivos ao fornecer somente regras de introdução, com a forma de regras de eliminação sendo forçadas por esta escolha. (Simetricamente, conectivos negativos podem ser definidos em cálculos focados ao fornecer somente regras de eliminação, com as regras de introdução forçadas por esta escolha). A segunda visão, que pode ser denominada como a interpretação de proposições computacional (ou de ), destaca a visão que fixa um sistema computacional e então fornece uma interpretação de “factibilidade” de proposições para dar-lhes algum conteúdo construtivo. Por exemplo, um realizador para a proposição “A implica B” é uma função computável que pega um realizador para A e o usa para computar um realizador para B. Observe que os modelos de factibilidade caracterizam realizadores para proposições em termos de seus comportamentos visíveis e não em termos de suas estruturas internas. Girard mostra que para lógica linear refinada de segunda ordem, dado um sistema computacional com “não-terminação” e paradas de erro como efeitos, factibilidade e focalização dão o mesmo significado aos tipos. O Ludics foram propostos pelo lógico Jean-Yves Girard. Seu artigo que apresenta o assunto, Locus solum: from the rules of logic to the logic of rules, tem algumas características que podem ser vistas como ‘excêntricas’ para uma publicação em lógica matemática (como por exemplo as ilustrações de Gambás Raivosos). É preciso notar que a intenção destas características é reforçar o ponto de vista de Jean-Yves Girard quando escrevia o artigo. E assim, oferece ao leitor a possibilidade de entender Ludics independente de seus contextos. (pt)
|
| rdfs:comment
|
- In proof theory, ludics is an analysis of the principles governing inference rules of mathematical logic. Key features of ludics include notion of compound connectives, using a technique known as focusing or focalisation (invented by the computer scientist ), and its use of locations or loci over a base instead of propositions. The primary achievement of ludics is the discovery of a relationship between two natural, but distinct notions of type, or proposition. (en)
- Na Teoria da Prova, Ludics é uma análise dos princípios que controlam as regras da lógica matemática. As principais características do Ludics são a noção de conectivos compostos usando uma técnica conhecida como “focalização” (inventada pelo cientista da computação ), e seu uso de locais ou loci sobre uma base ao invés de proposições. A primeira motivação de objetivos técnicos do Ludics é a descoberta da relação entre duas noções naturais, porém distintas, de tipo ou proposição. (pt)
|
