Людис

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

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

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

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

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

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

Людис был предложен логиком Жаном-Ивом Жираром . Его статья, представляющая лудики, Locus solum: от правил логики к логике правил , имеет некоторые особенности, которые можно рассматривать как эксцентричные для публикации по математической логике (например, иллюстрации скунсов). Следует отметить, что целью этих статей является отстаивание точки зрения Жан-Ива Жирара на момент написания статьи. И, таким образом, он предлагает читателям возможность понимать лудики независимо от их происхождения.

Внешние ссылки

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