Ludics - Ludics

В теория доказательств, юмор представляет собой анализ принципов, регулирующих правила вывода математическая логика. Ключевые особенности ludics включают понятие сложных связок с использованием техники, известной как фокусировка или же фокусировка (изобрел компьютерный ученый Жан-Марк Андреоли ), и его использование локации или же места над базой вместо предложений.

Точнее, ludics пытается восстановить известные логические связки и доказательства поведения, следуя парадигме интерактивных вычислений, аналогично тому, что делается в семантика игры с которым он тесно связан. Абстрагируя понятие формул и сосредотачиваясь на их конкретном использовании, то есть различных случаях, он обеспечивает абстрактный синтаксис за Информатика, поскольку локусы можно рассматривать как указатели на память.

Основное достижение юдизма - открытие взаимосвязи между двумя естественными, но различными понятиями типа или предложения.

Первая точка зрения, которую можно было бы назвать теоретико-доказательственной или Gentzen -стиль интерпретации предложений, гласит, что смысл предложения возникает из правил его введения и исключения. Фокализация уточняет эту точку зрения, проводя различие между положительными предложениями, значение которых вытекает из их правил введения, и отрицательными предложениями, значение которых возникает из их правил исключения. В сфокусированных исчислениях можно определить положительные связки, задав только правила их введения, при этом форма правил исключения определяется этим выбором. (Симметрично, отрицательные связки могут быть определены в сфокусированных исчислениях, задав только правила исключения, а правила введения обусловлены этим выбором.)

Вторая точка зрения, которую можно было бы назвать вычислительной или Интерпретация Брауэра-Гейтинга-Колмогорова предложений, считает, что мы фиксируем вычислительную систему заранее, а затем даем осуществимость интерпретация предложений для придания им конструктивного содержания. Например, реализатор для предложения «A подразумевает B» является вычислимой функцией, которая принимает реализатор для A и использует его для вычисления реализатора для B. Модели реализуемости характеризуют реализаторы для предложений с точки зрения их видимого поведения, а не в с точки зрения их внутренней структуры.

Жирар показывает, что для аффинного второго порядка линейная логика, учитывая вычислительную систему с неопределенностью и ошибками, прекращающимися, поскольку эффекты, реализуемость и фокусировка придают типам то же значение.

Ludics был предложен логик Жан-Ив Жирар. Его статья, представляющая Ludics, Locus solum: от правил логики к логике правил, имеет некоторые особенности, которые могут показаться эксцентричными для публикации в математическая логика (например, иллюстрации Positive Skunks). Следует отметить, что целью этих функций является обеспечение соблюдения точки зрения Жан-Ив Жирар на момент написания. И, таким образом, он предлагает читателям возможность понимать юмор независимо от их происхождения.^{[сомнительный – обсуждать]}

внешняя ссылка

Жирар, J-Y, Locus solum: от правил логики к логике правил (.pdf), Математические структуры в компьютерных науках, 11, 301–506, 2001.
Группа чтения Жирара в Университет Карнеги Меллон (вики о Locus Solum)