О предикативности лямбда-исчисления

Предисловие

Лямбда-исчисление является основанием для построения семантики языков программирования [см.: 2, 6, 5]. В 60-е гг. XX в. "Скотт описал в его <лямбда-исчисления> терминах семантику языков программирования" [2, с. 6]. С одной стороны, имеется результат о вложении лямбда-исчисления в модальную логику [1] (и далее – в более простые предикативные логики), а также доказательство непротиворечивости лямбда-исчисления [12] С другой стороны, интуитивные представления о не-формализуемости непредикативных конструкций в лямбда-исчислении, изложенные в монографии [11], подлежат более строгому изложению, что и описано далее в статье.

1.    Иерархия логических структур

Гносеологические основания 6уровневой иерархии математических представлений (понятий), в т. ч. логических, и их последовательнсть в истории математики рассмотрены ранее [см.: 10]. В работе [11] описана иерархия логических структур от 5-го уровня (формальных систем и лямбда- исчисления), допускающая вложение структур одного уровня (начиная с 5-го) в более низкий уровень. Схема рассуждений такова.

Как указано в работе [1], лямбда-исчисление "вкладывается" в модельную логику. Далее, легко видеть, модальная логика вкладываема в некоторую многозначную логику. Многозначная логика вкладывается в декартово произведение двузначных логих. Двузначная логика реализуема на некоторых множествах (несамопринадлежащих), (см., например, диаграммы Венна или рисунок).

О невозможности непредикативных конструкций в лямбда-исчислении из интуитивных соображений (на примерах результатов теории множеств с самопринадлежностью) уже сказано [11]. Однако имеются и иные рассуждения относительно этого.

2.    Предикативность лямбда-исчисления

Основной принцип лямбда-исчисления заключается в наличии лямбда-абстрактора. "Пусть t (^ t(x)) - выражение, содержащее, быть может, переменную х, тогда lx.t(x) - это такая функция f, которая сопоставляет аргументу а значение t(a). Иными словами, имеет

место (1x.t(x))a = t(a)" [2, с. 18] 1 .

С другой стороны, в теории алгоритмов имеется следующий сильный результат [4]: "Для всякого алфавита А может быть указан такой нормальный алгоритм U над А, что невозможен нормальный алгоритм в А, эквивалентный U относительно <этого же алфавита> А.

В качестве такого алгоритма можно, например, взять удваивающий алгоритм над алфавитом А, т .е. такой, что нормальный алгоритм U над А, что U(P)=PP, где P - слово в А."

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

В лямбда-исчислении такой буквой, находящейся вне удвоения, является символ "1" лямбда-абстракции (эту лямбда-абстракцию задаёт человек, используя лямбда-исчисление). Соответственно гносеологической схемы отражения действительности в сознании для внешнего по отношению к сознанию отображения непредикативных конструкций необходимо удваивание образа действительности [11, 8]. То есть лямбда-абстракция не действует на саму себя - не является непредикативной -значит, предикативна. Доказана теорема.

Теорема 1. Лямбда-исчисление - предикативно. □

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

3.    Сопоставление лямбда-исчисления и непредикативности

С одной стороны, лямбда-исчисление допускает модель в непредикативной семантике самопринадлежности [7, 9, 11]; с другой

Пример логики объемов понятий на неса-мопринадлежащих множествах стороны, лямбда-исчисление является предикативным. Таким образом, предикативные конструкции являются частью вообще логических конструкций, среди которых необходимо есть и непредикативные. Этот содержательный результат аналогичен выделению в множестве всех множеств (самопринадлежащем, непредикативном) множества, содержащего все неса-моприналежащие множества [11].

Заключение

Таким образом, показано, что ввиду предикативности лямбда-исчисления и того, что оно реализует семантику языков программирования, непредикативные конструкции не реализуемы посредством языков программирования 2.