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

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

см. Логика комбинаторная.

Философская Энциклопедия. В 5-х т. — М.: Советская энциклопедия. Под редакцией Ф. В. Константинова. 1960—1970.

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

    КОМБИНАТОРНАЯ ЛОГИКА — направление в основаниях и философии математики, в котором в качестве основных понятий выбираются: функция (оператор) и операция аппликации (application) — применение (приложение) функции/к аргументу^, пишут: (fg). Функции понимаются теоретико-операторно, бестипово, т. е. допустимы: (gf), (gg), (g(fi)), ((gg)(ig)) и т. д. Выражение видаДх/,..., χ„) является лишь записью для (...((/λ/)^)...χ„). Тем самым многоместные функции сводятся к одноместным. Опуская скобки, пишут: fKjXs-.x^•, вместо Χι,..., х„ можно поставить f, получая^.../ Здесь η > 0 (если η = 0, то/— нульместная функция).

    Исходными объектами (сокращенно, по X. Карри, обами) в комбинаторной логике служат константы и переменные (множество переменных может быть пустым). Новые обы строятся из исходных и полученных ранее по правилу: если а и b — обы, то (ab) считается обом. Выделяются три константы, обозначающие индивидуальные функции (комбинаторы): два собственных комбинатора А'и S, удовлетворяющих равенствам КаЬ = а и Sabc =- ac(bc), где а, b и с — произвольные обы (скобки в обах восстанавливаются по ассоциации влево) и один дедуктивный комбинатор U как некоторый аналог формальной импликации или оператора функциональности. Эти три комбинатора позволяют заменить любое предложение логико-математических языков комбинацией (обом) из К, Su UK скобок, откуда и название “комбинаторная логика” (введенное Карри). Употребление же переменных вообще может быть исключено, что соответствует первоначальному замыслу М. И. Шейнфинкеля, Карри и А. Чёрча. К примеру, если А комбинатор такой, что Аху = χ + у, а С комбинатор такой, что Cficy =fyx [или в более обычных обозначениях: приложение комбинатора А к аргументам х, у дает χ + у; приложение комбинатора С кДх}') дает/(узс)], то сумму у + х в этом случае можно выразить как САху. Тождество х + у =у + х выражается при этом в виде Аху = САху. И если (как это делается обычно в математике) трактовать тождественное равенство/^/, ...,x„)=g(x/, ...,x„) как другое выражение для/^ g (т. е. считать, что функции/ и g, относящие обе одни и те же объекты к одним и тем же значениям аргументов, отождествляются нами), то другим выражением для тождества х+у^у+х будет формула А = СА, не содержащая переменных.

    Создателем комбинаторной логики (1920) является московский математик Моисей Ильич Шейнфинкель (1887—1942). Он ввел комбинаторы К, S Α U, сформулировал и обосновал, используя указанные равенства для Кя S, принцип комбинаторной полноты, более общий, чем канторовское неограниченное теоретико-множественное свертывание. Шейнфинкель предложил один из первых способов уточнения интуитивного понятия алгоритма, определив по существу комбинаторные алгоритмы как вариант реализации вычислительной (алгоритмической) части дискретно-комбинаторной программы Лейбница.

    Независимо от Шейнфинкеля американские математики Карри и Чёрч получили аналогичные результаты. В их трудах комбинаторные алгоритмы представлены дедуктивно в виде доказуемо непротиворечивых исчислений негильбертовского типа. Таковы, в частности, ламбда-исчисления (?-исчисления) Чёрча, эквивалентные чистой (без логических законов) комбинаторной логике Шейнфинкеля—Карри. Исчисления Шейнфинкеля—Чёрча—Карри оказались удачными теориями вычислений. Они дали толчок развитию теории рекурсий, различных видов алгоритмов, а в последнее время и информатики. Известны применения комбинаторной логики в доказательств теории, в семантике языков программирования, алгебре, топологии, теории категорий и др. разделах современного знания.

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

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

    а->Ь . (Ь ->ϋ)(α,Γ=>θ) , (Γ =^ Θ, д) (а -> Ь) *λ:——Γ———.——;λ*: a=>b

    r=>Q,b

    где а и b — обы, Γ, θ — наборы обов, —> и => суть символы секвенций 1-го и 2-го ярусов, алгоритмической (вычислительной) и дедуктивной (генценовской) соответственно. Говорят, что об а конвертируется в об b, если секвенция а -” b выводима в чистой комбинаторной логике (в исчислении ШЧК). Все элементы языка множеств теории записываются как обы комбинаторной логики с точностью до конвертируемости. Так, атомарная формула b ε а представляется обом Ьа, по формуле С и переменной χ строится новый терм (новое множество) как об АдС, отражая тем самьм исходный принцип Кантора: неограниченное образование новых множеств.

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

    Знаменитый парадокс Рассела (1902) отражается в классе M в виде выводов двух дедуктивных секвенций =>D и =>1Z>, где 1 — знак отрицания, a D — об: Ξλγ.Πλχ. s (χ ε y)((́x ε χ)), представляющий частный случай известной схемы теоретико-множественного свертывания, записанной на языке комбинаторной логики.

    Лит.: Логика комбинаторная (Яновская С. А.).— В кн.: Философская энциклопедия, т. }. М., 1964; Sdinnßnkel M. Über die Bausteine der Mathematischen Logik. — “Math. Annalen”. 1924, Bd 92; Seidin J. /', Hindley J. R. (eds.). To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism. L., 1980: Rews A. A Bibliography of LambdaCalculi. Combinatory Logics and Related Topics. Amsterdam, 1982; Барендрегт X. Лямбда-исчисление. Его синтаксис и семантика. М., 1985; kynrice А. С. Об одной арифметически непротиворечивой ?-теории. — “Zeitschrift für Math. Logik und Grundlagen der Mathematik”, 1983, Bd 29. H. 5; Кузччева З. А., Ку:шчев А. С. Системы с бесконечной логикой м неограниченным принципом свертывания. К 150-летиюсо дня рождения Г. Кантора. — В кн.: Бесконечность в математике: философские и исторические аспекты. М., 1997; КузичевА. С. Вариант формализации канторовской теории множеств.—Доклады Российской Академии наук. 1999. т. 369, № 6; Он же. Решение проблемы Гильберта по Колмогорову. — Там же, 2000, т. 371. № 3.

    А. С. Кузичев

Новая философская энциклопедия: В 4 тт. М.: Мысль. Под редакцией В. С. Стёпина. 2001.