WikiDer > Аффинная логика

Affine logic

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

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

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

Аффинную логику можно встроить в линейную логику, переписав аффинную стрелку как линейная стрелка .

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

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

Заметки

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

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

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

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