КОМБИНАТОРНАЯ ЛОГИКА

КОМБИНАТОРНАЯ ЛОГИКА – направление в основаниях и философии математики, в котором в качестве основных понятий выбираются: функция (оператор) и операция аппликации (application) – применение (приложение) функции f к аргументу g, пишут: (fg). Функции понимаются теоретико-операторно, бестипово, т.е. допустимы: (gf), (gg), (g(ff)), ((gg)(fg)) и т.д. Выражение вида f(x1, …, xn), является лишь записью для (...((fx1)x2)..хn). Тем самым многоместные функции сводятся к одноместным. Опуская скобки, пишут: fx1x2 … xn вместо х1, ...,  хn можно поставить f, получая fff …f.  Здесь n≥0 (если n = 0, то f – нульместная функция).

Исходными объектами (сокращенно, по X.Карри, обами) в комбинаторной логике служат константы и переменные (множество переменных может быть пустым). Новые обы строятся из исходных и полученных ранее по правилу: если a и b – обы, то (ab) считается обом. Выделяются три константы, обозначающие индивидуальные функции (комбинаторы): два собственных комбинатора К и S, удовлетворяющих равенствам Kab = а и Sabc = ac(bc), где a, b и с – произвольные обы (скобки в обах восстанавливаются по ассоциации влево) и один дедуктивный комбинатор U как некоторый аналог формальной импликации или оператора функциональности. Эти три комбинатора позволяют заменить любое предложение логико-математических языков комбинацией (обом) из К, S и U искобок, откуда и название «комбинаторная логика» (введенное Карри). Употребление же переменных вообще может быть исключено, что соответствует первоначальному замыслу М.И.Шейнфинкеля, Карри и А.Чёрча. К примеру, если А комбинатор такой, что Аху = x + у, а С комбинатор такой, что Cfxy = fyx [или в более обычных обозначениях: приложение комбинатора А к аргументам х, у дает x + у;приложение комбинатора С к fху) дает f(yx)], то сумму у + x в этом случае можно выразить как САху. Тождество x + у =у + x выражается при этом в виде Аху = САху. И если (как это делается обычно в математике) трактовать тождественное равенство f(x1, ..., хn)= g(x1 ..., хn) как другое выражение для f = g (т.е. считать, что функции f  и g, относящие обе одни и те же объекты к одним и тем же значениям аргументов, отождествляются нами), то другим выражением для тождества х + у = у + х будет формула А = CA, не содержащая переменных.

Создателем комбинаторной логики (1920) является московский математик Моисей Ильич Шейнфинкель (1887–1942). Он ввел комбинаторы К, S и U, сформулировал и обосновал, используя указанные равенства для К и S, принцип комбинаторной полноты, более общий, чем канторовское неограниченное теоретико-множественное свертывание. Шейнфинкель предложил один из первых способов уточнения интуитивного понятия алгоритма [АЛГОРИТМ], определив по существу комбинаторные алгоритмы как вариант реализации вычислительной (алгоритмической) части дискретно-комбинаторной программы Лейбница [ЛЕЙБНИЦ].

Независимо от Шейнфинкеля американские математики Карри и Чёрч получили аналогичные результаты. В их трудах комбинаторные алгоритмы представлены дедуктивно в виде доказуемо непротиворечивых исчислений негильбертовского типа. Таковы, в частности, ламбда-исчисления (λ-исчисления) Чёрча, эквивалентные чистой (без логических законов) комбинаторной логике Шейнфинкеля – Карри. Исчисления Шейнфинкеля – Чёрча – Карри оказались удачными теориями вычислений. Они дали толчок развитию теории рекурсий, различных видов алгоритмов, а в последнее время и информатики. Известны применения комбинаторной логики в доказательств теории [ДОКАЗАТЕЛЬСТВ ТЕОРИЯ], в семантике языков программирования, алгебре, топологии, теории категорий и др. разделах современного знания.

Бестиповые исчисления Шейнфинкеля – Чёрча – Карри (для краткости: ШЧК) были введены прежде всего в расчете на то, что их дедуктивные расширения станут основаниями математики и других наук. Пытаясь реализовать синтаксически дедуктивный комбинатор U, Карри и Чёрч построили также логико-математические исчисления гильбертовского типа, которые, однако, оказались противоречивыми: парадокс Клини – Россера (1936), парадокс Карри (1941). Отметим, что в парадоксе Карри из логических средств используются только имшшкативные, а правило modus ponens выступает как единственный логический источник противоречивости (см. Парадокс логический [ПАРАДОКС ЛОГИЧЕСКИЙ]). Поскольку все известные дедуктивные системы гильбертовского типа либо бедны выразительными возможностями, либо противоречивы, обращаются к идее ступенчатых расширений. Ступенчатые системы комбинаторной логики строятся на основе комбинаторных алгоритмов путем последовательных расширений бестиповых непротиворечивых исчислений ШЧК, опираясь на принципы дедуктивной полноты – правила введения операторов (прежде всего логических) в сукцедент (в заключение выводимостей) и в антецедент (в посылки выводимостей).

Такая трактовка выводимостей позволила ограничить иерархии двумя ярусами. Первый – исчисления ШЧК. Второй вводится как расширение первого на базе исчисления секвенций [ИСЧИСЛЕНИЕ СЕКВЕНЦИЙ] – классической логики предикатов первого порядка, распространенной на обы комбинаторной логики, без постулируемого (в силу известного результата Г.Генцена [ГЕНЦЕН]1934 г.) правила сечения. Логические связки и кванторы представляются в виде обов, составленных из символов алфавита комбинаторной логики, являющихся константами первого яруса. Среди всех двухярусных систем выделяется А-система со всеми логическими операторами и оператором λ. Ее правила, объединяют два яруса в формальное исчисление (в соответствии с программой Гильберта; см. Формализм [ФОРМАЛИЗМ]), для которого доказываются теоремы о полноте (в смысле Гёделя, ср. его теоремы 1931 г. о неполноте известных исчислений гильбертовского типа) и непротиворечивости (в классическом секвенциальном смысле). Эти правила суть

где а и b – обы, Г, Θ – наборы обов, → и ⇒ суть символы секвенций 1-го и 2-го ярусов, алгоритмической (вычислительной) и дедуктивной (генценовской) соответственно. Говорят, что об а конвертируется в об b, если секвенция а → b выводима в чистой комбинаторной логике (в исчислении ШЧК).

Все элементы языка множеств теории [МНОЖЕСТВ ТЕОРИЯ]записываются как обы комбинаторной логики с точностью до конвертируемости. Так, атомарная формула b ε а представляется обом bа, по формуле С и переменной x строится новый терм (новое множество) как об λхС, отражая тем самым исходный принцип Кантора: неограниченное образование новых множеств.

В классе всех выводов A-системы выделяется подкласс M всех выводов, в которых применения правила *, структурных и логических правил 2-го яруса ограничены описанными элементами теории множеств. В основе M лежат два принципа, характеризующие канторовскую («наивную») теорию множеств: неограниченное теоретико-множественное свертывание и классическая логика предикатов 1-го порядка без ограничений, соответствующие двум ярусам A-системы. Класс М выступает как вариант непротиворечивой формализации канторовской теории множеств.

Знаменитый парадокс Рассела (1902) отражается в классе M в виде выводов двух дедуктивных секвенций ⇒D) и ⇒⌉D, где ⌉ – знак отрицания, a D – об: ∃λу.Пλх. = (x ε у)(⌉(х ε x)), представляющий частный случай известной схемы теоретико-множественного свертывания, записанной на языке комбинаторной логики.

Литература:

1. Логика комбинаторная (Яновская С.Л.).– В кн.: Философская энциклопедия, т. 3. М., 1964;

2. Schönfmkel M. Über die Bausteine der Mathematischen Logik. – «Math. Annalen», 1924, Bd 92;

3. Seldin J.P., Hindley J. R. (eds.). Το Η.Β.Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism. L., 1980;

4. Rezus A. A Bibliography of Lambda-Calculi. Combinatory Logics and Related Topics. Amsterdam, 1982;

5. Барендрегт X. Ламбда-исчисление. Его синтаксис и семантика. М., 1985;

6. Кузичев А.С.Об одной арифметически непротиворечивой λ-теории. – «Zeitschrift für Math. Logik und Grundlagen der Mathematik», 1983, Bd 29, H. 5;

7. Кузичева З.Α., Кузечев А.С. Системы с бесконечной логикой и неограниченным принципом свертывания. К 150-летию со дня рождения Г.Кантора. – В кн.: Бесконечность в математике: философские и исторические аспекты. М., 1997;

8. Кузичев А.С. Вариант формализации канторовской теории множеств. – Доклады Российской Академии наук, 1999, т. 369, № 6;

9. Он же. Решение проблемы Гильберта по Колмогорову. – Там же, 2000, т. 371, № 3.

А.С.Кузичев