Приглашаем посетить сайт
КОМБИНАТОРНАЯ ЛОГИКА
КОМБИНАТОРНАЯ ЛОГИКА - направление в основаниях и философии математики, в котором в качестве основных понятий выбираются: функция (оператор) и операция аппликации (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.
А. С. Кузичев