В теории доказательств , лудика — это анализ принципов, управляющих правилами вывода математической логики . Ключевые особенности лудики включают понятие составных связок, использование техники, известной как фокусирование или фокусировка (изобретенной ученым-компьютерщиком Жаном-Марком Андреоли), и ее использование местоположений или локусов над базой вместо предложений .
Точнее, ludics пытается извлечь известные логические связки и доказательства поведения, следуя парадигме интерактивных вычислений, подобно тому, что делается в игровой семантике , с которой она тесно связана. Абстрагируя понятие формул и фокусируясь на их конкретном использовании — то есть на отдельных случаях — она предоставляет абстрактный синтаксис для компьютерной науки , поскольку loci можно рассматривать как указатели на память.
Главным достижением лудики является открытие связи между двумя естественными, но различными понятиями типа или предложения.
Первая точка зрения, которую можно назвать теоретико-доказательной или интерпретацией предложений в стиле Генцена , гласит, что значение предложения возникает из правил его введения и исключения. Фокусировка уточняет эту точку зрения, различая положительные предложения, значение которых возникает из правил их введения, и отрицательные предложения, значение которых возникает из правил их исключения. В сфокусированных исчислениях можно определить положительные связки, указав только правила их введения, при этом форма правил исключения будет навязана этим выбором. (Симметрично, отрицательные связки могут быть определены в сфокусированных исчислениях, указав только правила исключения, при этом правила введения будут навязаны этим выбором.)
Вторая точка зрения, которую можно назвать вычислительной или интерпретацией предложений Брауэра–Гейтинга–Колмогорова , предполагает, что мы фиксируем вычислительную систему заранее, а затем даем интерпретацию реализуемости предложений, чтобы придать им конструктивное содержание. Например, реализатор для предложения «A подразумевает B» — это вычислимая функция, которая берет реализатор для A и использует его для вычисления реализатора для B. Модели реализуемости характеризуют реализаторы для предложений с точки зрения их видимого поведения, а не с точки зрения их внутренней структуры.
Жирар показывает, что для аффинной линейной логики второго порядка , если задана вычислительная система с незавершением и остановкой из-за ошибки в качестве эффектов, реализуемость и фокусировка придают типам одинаковое значение.
Ludics был предложен логиком Жаном-Ивом Жираром . Его статья, знакомящая с ludics, Locus solum: от правил логики к логике правил , имеет некоторые черты, которые могут показаться эксцентричными для публикации по математической логике (например, иллюстрации скунсов). Цель этих черт — усилить точку зрения Жана-Ива Жирара на момент ее написания. И, таким образом, она дает читателям возможность понять ludics независимо от их бэкграунда. [ сомнительно — обсудить ] [ необходима цитата ]