Как сделать лямбда-исчисление сильным нормализующим без системы типов?

9

Существует ли какая-либо система, похожая на лямбда-исчисление, которая сильно нормализуется, без необходимости добавлять систему типов поверх нее?

MaiaVictor
источник
5
Вопрос немного не сфокусирован: что вы подразумеваете под «похожим»? Финальные автоматы похожи? -исчисления является универсальной моделью вычислений, так что все , что есть «похожи» на него, вероятно , скрытый элемент завершения форм расчета. λ
Мартин Бергер,

Ответы:

22

Я могу придумать несколько возможных ответов из линейной логики.

Самым простым является аффинное лямбда-исчисление: рассмотрим только лямбда-термины, в которых каждая переменная встречается не более одного раза. Это условие сохраняется путем восстановления, и сразу видно, что размер аффинных членов строго уменьшается с каждым шагом восстановления. Следовательно, нетипизированное аффинное лямбда-исчисление сильно нормализуется.

Более интересные примеры (с точки зрения выразительности) дают так называемые «легкие» лямбда-исчисления, возникающие из подсистем линейной логики, введенных Жираром в «Световой линейной логике» (Информация и вычисления 143, 1998). как «Мягкая линейная логика» Лафона (Теоретическая информатика 318, 2004). В литературе есть несколько таких исчислений, возможно, хорошим справочником является «Легкое аффинное лямбда-исчисление и сильная нормализация за полиномиальное время» (Архив математической логики 46, 2007). В этой статье Теруи определяет лямбда-исчисление, основанное на лёгкой аффинной логике, и доказывает для него сильный результат нормализации. Несмотря на то, что типы упоминаются в статье, они не используются в доказательстве нормализации. Они полезны для аккуратной формулировки основного свойства лёгкого аффинного лямбда-исчисления, а именно того, что члены определенного типа представляют в точности функции Polytime. Подобные результаты известны для элементарных вычислений с использованием других «легких» лямбда-исчислений (статья Теруи содержит дополнительные ссылки).

В качестве дополнительного примечания интересно отметить, что в терминах теории доказательств аффинное лямбда-исчисление соответствует интуиционистской логике без правила сжатия. Гришин заметил (до введения линейной логики), что при отсутствии сжатия наивная теория множеств (т. Е. С неограниченным пониманием) непротиворечива (т. Е. Парадокс Рассела не дает противоречия). Причина в том, что исключение выреза для наивной теории множеств без сжатия может быть доказано прямым аргументом уменьшения размера (как тот, который я привел выше), который не зависит от сложности формул. Посредством соответствия Карри-Говарда это в точности нормализация нетипизированного аффинного лямбда-исчисления. Это путем перевода парадокса Рассела в линейную логику и «подстройкой» экспоненциальные модальности, так что никакое противоречие не могло быть выведено, что Жирар придумал легкую линейную логику. Как я уже упоминал выше, в вычислительном отношении легкая линейная логика дает характеристику вычислимых функций за полиномиальное время. В терминах теории доказательств непротиворечивая наивная теория множеств может быть определена в легкой линейной логике так, что доказуемо полные функции - это точно вычислимые функции за полиномиальное время (на эту тему есть еще одна статья Теруи, «Теория аффинного множества света: наивный»). теория множеств полиномиального времени ", Studia Logica 77, 2004).

Дамиано Мазза
источник
Я бы сказал, что легкое аффинное лямбда-исчисление Теруи набрано, учитывая ограничения на использование аффинных переменных, стратифицированные операторы let и моноидальность оператора! Просто эти ограничения вводятся неформально. LLL Жирара также напечатан.
Мартин Бергер
@ Мартин: я не согласен. Структурные ограничения, накладываемые на лёгкие аффинные термины, имеют иную природу, чем ограничения системы типирования. Самым большим отличием является то, что типирование обязательно индуктивное, тогда как формирование скважины (то есть стратификация, аффинное использование и т. Д.) Может быть определено как комбинаторное свойство термина. Так, например, когда вы вводите термин, вы обычно должны вводить его подтермы, тогда как подтерма стратифицированного термина не нуждается в стратификации.
Дамиано Мазза
Извините, еще одна вещь о LLL Жирара: система, очевидно, типизирована, потому что она включает в себя формулы. Однако, как я уже упоминал в своем ответе, формулы не играют никакой роли в устранении сокращения LLL. Фактически, могут быть добавлены произвольные фиксированные точки формул (включая парадоксальную формулу Рассела, которая эквивалентна его собственному отрицанию!) Без LLL, становящейся непоследовательной. Это связано с тем, что исключение среза выполняется по «чисто структурным» причинам, независимо от того, что вы можете прикреплять типы к своим доказательствам (технически теорема об исключении среза для LLL может быть доказана в нетипизированных сетях доказательств).
Дамиано Мазза
Хорошо, если вы сделаете индуктивность условием чего-то, что является системой печати. Это интересная точка зрения, с которой я раньше не сталкивался.
Мартин Бергер
... и это точка зрения, я бы сказал, ошибочна. Например, в системах, включающих подтипирование (в более общем смысле, при рассмотрении внешней интерпретации типов в смысле Рейнольдса), вполне естественно использовать коиндуктивный взгляд на типирование. В литературе немало примеров (хотя я думаю, что это недооценивают).
Ноам Цайлбергер
12

Оригинальная статья Черча и Россера «Некоторые свойства обращения» описывает нечто, что может служить примером того, что вы ищете.

Если вы используете строгое лямбда-исчисление, где в каждом вхождении вас есть то, что появляется свободным в , то без системы типов выполняется следующее свойство (это теорема 2 в статье Черча и Россера):λx.MxM

Если является нормальной формой , то существует такое число , что любая последовательность сокращений, начинающаяся с , приведет к [по модулю альфа-эквивалентности] после не более чем сокращений.BAmABm

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

Роб Симмонс
источник
1
Что-то не в порядке, так как не фигурирует в заключении. m
Андрей Бауэр
Закончил утверждение теоремы на этот раз, спасибо. Часть, которую я написал как [по модулю альфа-эквивалентности], изначально была «(в приложениях правила I)», что означает то же самое, если я не помню Правило I правильно.
Роб Симмонс
10

Вот забавный, Нил Джонс и Нина Бор:

Завершение по значению в нетипизированном -calculusλ

В нем показано, как применить анализ изменения размера (тип анализа потока управления, который обнаруживает бесконечные циклы) для нетипизированных -terms. Это довольно хорошо на практике, но, конечно, ограничивается -terms без определенных констант (хотя метод может быть расширен для более общего использования).λλ

Преимущество типирования, конечно, заключается в низкой стоимости и модульности подхода: в общем случае анализ завершения очень немодулярен, но набор может быть выполнен «по частям».

Коди
источник
Это действительно интересно!
MaiaVictor