Введение

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