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

Размещено на http: //www. allbest. ru/

Пермский государственный национальный исследовательский университет Россия, 614990, Пермь, ул. Букирева, 15

Математика

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

В.Л. Чечулин

chechulinvl@mail.ru ; (342) 2-396-424

Аннотация

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

Ключевые слова: лямбда-исчисление; иерархия логических структур; предикативность; непредикативность.

Annotatіon

About predicative of the lambda-calculus

V. L. Chechulin

Perm State University, Russia, 614990, Perm, Bukirev st., 15

chechulinvl@mail.ru; (342) 2-396-424

Based on the theorem of Nagorniy about doubling of words in the alphabet shown that lambda-calculus was predicative, unformalizable in lambda-calculus impredicative structures. This result coincides with similar findings obtained in the theory of sets with selfconsidering.

Key words: lambda-calculus; a hierarchy of logical structures; predication; impredicative.

Предисловие

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

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

математический логический нагорный лямбда

Пример логики объемов понятий на несамопринадлежащих множествах

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

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

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

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

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

(x.t(x))a = t(a)" [2, с. 18]

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

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

U(P)=PP,

где P - слово в А."

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

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

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

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

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

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

Заключение

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

Список литературы

1. Артемов С.Н. Погружение модального -исчисления в логику доказательств // Математическая логика и алгебра: тр. Матем. ин-та им. В.А.Стеклова. 2003. Т. 242. С.44-58.

2. Барендрегдт Х. Лямбда-исчисление: его синтаксис и семантика / пер. с англ. М.: Мир, 1985. 608 с.

3. Карри Х. Основания математической логики / пер. с англ. М.: Мир, 1969. 568 с.

4. Нагорный Н.М. К усилению теоремы приведения теории алгоритмов // Докл. Акад. наук СССР. 1953. Т. 90, №3. С. 341-342.

5. Хендерсон П. Функциональное программирование: применение и реализация / пер. с англ. М.: Мир,1983. 350 с.

6. Чёрч А. Введение в математическую логику. Т. 1 / пер. с англ. М.: Иностр. лит., 1961.

7. Чечулин В.Л. О приложениях семантики самопринадлежности // Вестник Пермского университета. Сер. Математика Механика. Информатика. 2009. Вып. 3 (29). C.10-17.

8. Чечулин В.Л. Ограничения информаци-онных методов // Искусственный интеллект: философия, методология, инновации: матер. III Всерос. конф. МИРЭАМ: "Связь-Принт", 2009. С. 47-48.

9. Чечулин В.Л. Об одном варианте модельной области лямбда-исчисления // Синтаксис и семантика логических систем: матер. 3_й Рос. школы-семинара. Иркутск, 2010. С.112-114.

10. Чечулин В.Л. О последовательности 6 исторических этапов появления основных математических понятий // Вестник Пермского университета. Сер. Математика. Механика. Информатика. Вып. 2 (2). 2010. С.115-124.

11. Чечулин В.Л. Теория множеств с самопринадлежностью (основания и некоторые приложения) / Перм. гос. ун-т. Пермь, 2010. 100с.

12. Чечулин В.Л. О непротиворечивости лямбда-исчисления // В мире научных открытий. Сер. Математика. Механика. Информатика. 2011, №1. С. 203-206. URL: http://www.nkras.ru/articles/2011/1/vypusk12011.pdf

13. Chechulin V.L. About the selfconsidering semantic in the mathematical logic // Bull. Symbolic Logic. 2010. Vol.16, Is.1. P.111-112.

Размещено на Allbest.ru