Аффинная логика - Affine logic

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

Название «аффинная логика» связано с линейная логика, от которого он отличается, допуская правило ослабления. Жан-Ив Жирар представил название как часть геометрия взаимодействия семантика линейной логики, характеризующая линейную логику в терминах линейной алгебры; здесь он ссылается на аффинные преобразования на векторных пространствах.^[1]

Аффинная логика предшествовала линейной логике. В. Н. Гришин использовал эту логику в 1974 г.^[2] после наблюдения этого Парадокс Рассела не может быть выведен в теории множеств без сжатия, даже с аксиома безграничного понимания.^[3] Точно так же логика легла в основу разрешимой подтеории логика предикатов, называемой «прямой логикой» (Ketonen & Wehrauch, 1984; Ketonen & Bellin, 1989).

Аффинную логику можно встроить в линейную логику, переписав аффинную стрелку ${ displaystyle A rightarrow B}$ как линейная стрелка ${ displaystyle A multimap B otimes top}$ .

В то время как полная линейная логика (то есть пропозициональная линейная логика с мультипликативными, аддитивными и экспоненциальными) неразрешима, полная аффинная логика разрешима.

Аффинная логика составляет основу юмор.

Заметки

^ Жан-Ив Жирар, 1997. 'Аффинный '. Сообщение в список рассылки TYPES.
^ Гришин, 1974, а позже, Гришин, 1981.
^ Ср. Фредерик Фитч с доказательно последовательная теория множеств

использованная литература

В.Н. Гришин, 1974. «Нестандартная логика и ее приложение к теории множеств». Исследования по формализованным языкам и неклассической логике (русский), 135–171. Издат, Наука, Москва. .
В.Н. Гришин, 1981. «Предикатные и теоретико-множественные исчисления, основанные на логике без правил сжатия», (рус.). Известия Академии Наук СССР Серия Математическая 45 (1): 47-68. 239. Математика. Известия СССР, 18, № 1, Москва.
Кетонен и Вейхраух, 1984, разрешимый фрагмент исчисления предикатов. Теоретическая информатика 32: 297-307.
Кетонен и Беллин, 1989. Повторное обращение к процедуре принятия решения: заметки по Direct Logic. В Линейная логика и ее реализация.

Смотрите также

Эта логика -связанная статья является заглушка. Вы можете помочь Википедии расширяя это.

[1] Жан-Ив Жирар, 1997. 'Аффинный '. Сообщение в список рассылки TYPES.

[2] Гришин, 1974, а позже, Гришин, 1981.

[3] Ср. Фредерик Фитч с доказательно последовательная теория множеств

[1]

[2]

[3]