Сколько лямбда-термов имеют нормальную форму? Как меняются термины в результате бета-редукции? Давайте рассмотрим некоторые характеристики! [Субтитры]
Абстрактный
В этой статье мы исследуем некоторые числовые характеристики лямбда-термов, проводя эксперименты над всеми возможными замкнутыми термовами размеров ∈ [1;10]. Точнее, мы делаем бета-редукции к терминам до тех пор, пока они не придут к нормальной форме (если она у них есть), а затем анализируем результат.
Ключевые слова: лямбда-исчисление, лямбда-терм, бета-редукция, стратегия редукции, нормальная стратегия, нормальная форма, эксперимент, генератор термов.
Введение, мотивация и вклад
Анализ характеристик нормальной формы необходим не только для лучшего понимания лямбда-термов и науки о лямбда-исчислении в целом, но и для тестирования компиляторов и оптимизации программ, ожидаемая эффективность которых зависит от размера термов. Кроме того, существуют другие программы, которые работают непосредственно с лямбда-исчислением, например, системы ATP (автоматическое доказательство теорем). Все эти программы нужно тестировать на больших лямбда-термах, поэтому важно исследовать характеристики и поведение всевозможных термов.
Эта статья основана на моей дипломной работе (диссертации). Что касается моего вклада, то первое, что я сделал, это изучил всю соответствующую теорию, по которой я мог бы написать группу статей в будущем. Во-вторых, на основе статьи[1] я научился считать размер терминов и генерировать все возможные термины любого размера. Наконец, я реализовал интерпретатор[2] бета-редукции и провел эксперименты на языке C++17 (правда, это был не самый простой способ). В будущем я собираюсь написать еще одну статью[3], посвященную сравнению различных стратегий редукции.
P.S: если вы хотите расширить мои исследования, не стесняйтесь использовать мою программу[2], но не забудьте упомянуть меня, пожалуйста :). Также извините за мой английский; Я не носитель языка.
Краткая теория
В этом разделе мы вспомним некоторые основные концепции.
Закрытый термин–термин без свободных переменных. (𝜆x.𝜆y.xy) закрыт; (𝜆𝑥.𝜆y.xz) ‒ нет.
Бета-редекс (или просто редекс) ‒ терм вида (𝜆𝑥.𝑀)𝑁, где x — переменная, M и N — произвольные лямбда-термы.
Бета-редукция — это процесс замены аргументов в функции. Процедура бета-редукции аналогична вызову функции в языке программирования.
Термин находится в нормальной форме, если он не может быть сокращен (нет редексов). Термин имеет нормальную форму, если существует последовательность бета-редукций, начинающаяся с самого термина и заканчивающаяся его нормальной формой.
Не каждый термин имеет нормальную форму. Например,
Не всякая последовательность редукций приводит терм к нормальной форме. Например,
Мы можем предположить, что указанный выше термин не имеет нормальной формы, но если мы выберем другой редекс, то получим нормальную форму.
Если терм имеет нормальную форму, то редукция нормального порядка (или просто нормальная стратегия) в конце концов достигнет ее согласно теореме стандартизации.
В статье[1], которую я настоятельно рекомендую прочитать, авторы предложили способ подсчета размера терминов и способ генерации всех возможных термов с определенным размером и определенным количеством свободных переменных.
В таблице ниже показано количество всех возможных терминов размером n(строк) и количество свободных переменных m(столбцов).
Эксперименты
В общем, я реализовал интерпретатор лямбда-исчисления[2] на C++17, а потом проводил эксперименты, учитывая статью[1]. Я сократил все возможные замкнутые термы размерами от 1 до 10 включительно, установил существование нормальных форм и собрал некоторые характеристики. Из-за высоких вычислительных затрат мы ограничены размером 10. Количество всех возможных закрытых термов размера 11 равно 851 368 766; это слишком много, чтобы вычислить. Теперь посмотрим на результаты.
Доля терминов, находящихся в нормальной форме, среди всех терминов составляет 0,64. По мере увеличения размера соотношение изменяется следующим образом
Как видим, отношение монотонно убывает. Количество термов без редексов внутри растет медленнее, чем количество всех возможных термов по мере увеличения размера термов.
Отныне мы считаем статистику среди закрытых терминов, исключая термины, которые уже находятся в нормальной форме.
Если термин имеет последовательность бета-редукций, которая приводит к нормальной форме, мы будем называть эту последовательность цепочкой редукции.
Согласно приведенному выше графику, по мере увеличения размера терминов количество шагов редукции для приведения термина к нормальной форме в среднем увеличивается, но ненамного.
Среди терминов размера 10 более 65% терминов приводятся к нормальной форме за 1 шаг; где-то 25% в 2 шага; 5% — в 3 шага, согласно гистограмме выше.
Согласно приведенному выше графику, мы можем предположить, что зависимость уменьшенного размера терминов от исходного размера терминов является линейной. В среднем в результате сокращения размеры сроков уменьшаются в 1,5–2 раза.
Из графика выше видно, что средний максимальный размер терминов при сокращении линейно зависит от размера исходных терминов. Средний максимальный размер терминов при сокращении лишь немного превышает размер исходных терминов. Предположительно, результат означает, что средние члены не расширяются в большие члены при сокращении.
На приведенном ниже графике видно, что с увеличением размера терминов в среднем отношение максимального размера терминов при сокращении к исходному размеру терминов практически не растет. Эти величины практически не зависят друг от друга.
При разработке программы я выяснил, что программно установить факт отсутствия нормальных форм можно двумя способами:
1. Термины могут быть приведены в термины, которые уже появились в « список сокращений», во время процедуры сокращения. Например,
Я называю эти термины зацикливанием.
2. Члены могут не достигать своих нормальных форм в сотнях, тысячах сокращений или могут быть сокращены до членов величиной в десятки тысяч. Из-за больших вычислительных затрат приходится ограничивать количество шагов редукции и подсчет максимального размера термов (например, выполнение шага редукции с термом размером 32 000 занимает больше минуты). Я называю эти термины растущими. Я использовал следующие ограничения для экспериментов:
По мере увеличения размера терминов доля «зацикленных» термов уменьшается, а «растущих» терминов — увеличивается.
Важно отметить, что если терм «зацикленный», то он точно не имеет нормальной формы. Но если терм «возрастающий», мы не можем точно сказать, имеет он нормальную форму или нет. Это зависит от лимитов, а с высокими лимитами невозможно провести эксперимент, к сожалению, из-за больших вычислительных затрат.
Так что эксперименты не совсем точны; по мере увеличения размеров терминов увеличивается и доля «возрастающих» термов, поэтому установить факт отсутствия нормальных форм становится затруднительно. Но тем не менееэксперименты показывают общую картину.
Я надеюсь, что эта небольшая статья каким-то образом поможет другим в более крупных исследованиях. Спасибо за прочтение!
