Ағылшыншамен салыстырыңыз: абзацты басыңыз — түпнұсқа терезеде ашылады. Абзац астындағы EN түймесі оны мәтін ішінде көрсетеді.
Кіріспе
Дәлелдер теориясында лудика – математикалық логиканың тұжырымдамалық ережелерін реттейтін қағидаларды талдау. Лудиканың негізгі ерекшеліктері құрама байланыстар туралы түсінік, «фокус» немесе «фокализация» деп аталатын әдіс (компьютер ғалымы Жан Марк Андреоли тапқан) және базаның орнына «орналасқан жерлер» (loci) қолданылуын қамтиды. Нақтырақ айтқанда, лудика, ойын семантикасындағыдай, белгілі логикалық байланыстар мен дәлелдеу мінез-құлқыларын интерактивті есептеу үлгісін қолданып қалпына келтіруге тырысады, олармен тығыз байланысты. Формулалар туралы түсінікті абстракциялап, олардың нақты қолданылуына – яғни, жеке оқиғаларға – назар аудару арқылы, ол компьютер ғылымы үшін абстрактілі синтаксис ұсынады, себебі орналасқан жерлерді жадтағы мекенжайлар ретінде қарастыруға болады. Лудиканың маңызды жетістігі – екі табиғи, бірақ әртүрлі «түр» немесе «ұсыныс» түсінігі арасындағы байланысты табу. Бірінші көзқарас, оны дәлелдеу теориясының немесе Гентцен стиліндегі ұсыныстардың түсіндірілуі деп атауға болады, ұсыныстың мағынасы оның енгізу және жою ережелерінен туындайды дейді. Фокализация бұл көзқарасты оң ұсыныстарды (олардың мағынасы енгізу ережелерінен туындайды) және теріс ұсыныстарды (олардың мағынасы жою ережелерінен туындайды) ажырату арқылы жетілдіреді. Фокустық есептеулерде оң байланыстарды тек олардың енгізу ережелерін беру арқылы анықтауға болады, ал жою ережелерінің нысаны осы таңдаумен анықталады. (Симметриялы түрде, теріс байланыстарды фокустық есептеулерде тек жою ережелерін беру арқылы, ал енгізу ережелері осы таңдаумен анықталады.) Екінші көзқарас, оны есептеу немесе Брауэр–Хейтинг–Колмогоровтың ұсыныстарды түсіндіруі деп атауға болады, есептеу жүйесін алдын ала белгілеп, ұсыныстарға конструктивті мазмұн беру үшін оларды іске асыру мүмкіндігін түсіндіреді. Мысалы, «A-дан B шығады» ұсынысының іске асырылуы – A үшін іске асырылуды қабылдап, одан B үшін іске асырылуды есептейтін есептелетін функция. Іске асыру модельдері ұсыныстар үшін іске асырылуды олардың ішкі құрылымы бойынша емес, көрінетін мінез-құлқы бойынша сипаттайды. Жирар екінші реттік аффиндік сызықтық логика үшін, есептеу жүйесінде аяқталмау және қателіктердің тоқтатылуы әсер ретінде қарастырылса, іске асыру және фокализация түрлерге бірдей мағына беретінін көрсетті. Лудиканы логик Жан Ив Жирар ұсынған. Оның лудиканы таныстыратын «Locus solum: логика ережелерінен ережелердің логикасына» атты мақаласы математикалық логикадағы жарияланым үшін эксцентрикалық деп есептелетін кейбір ерекшеліктерге ие (мысалы, скункстардың суреттері). Бұл ерекшеліктердің мақсаты Жан Ив Жирардың оны жазған кездегі көзқарасын нығайту екенін атап өту керек. Осылайша, ол оқырмандарға лудиканы олардың біліміне қарамастан түсінуге мүмкіндік береді.
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 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 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.