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

Найдено 3 определения
Показать: [все] [проще] [сложнее]

Автор: [российский] Время: [советское] [современное]

Комбинаторная логика
одно из направлений в математической логике, занимающееся анализом понятий, к-рые в рамках классической математической логики принимаются без дальнейшего изучения. К их числу принадлежат понятия переменной, функции, правила подстановки и т. п. В классической математической логике пользуются правилами двух родов. Первые формулируются просто и используются без всяких ограничений. Таково, напр., правило modus ponens. Оно формулируется так: если выведены предложения «Если А, то В» и «А»», то выводится предложение «В». Это правило доступно для одноактного автоматического выполнения. Др. (напр., правило подстановки) формулируются очень сложно и предполагают ряд ограничений и оговорок (без них они не могут использоваться чисто формально). Одной из задач К. л. является создание таких формальных систем, где не будет встречаться правил, подобных правилу подстановки. Начало К. л. было положено трудами советского математика М. И. Шейнфинкеля (осн. результаты были опубликованы в 1924). Независимо от него А. Чёрч построил исчисление ламбда-конвер-сии, тесно связанное с К. л. Важные результаты получены также американским логиком X. Керри. Проблемы К. л. разрабатываются Б. Россе-ром, В. Креигом, Р. Фейсом и др.

Источник: Философский словарь. 1963

ЛОГИКА КОМБИНАТОРНАЯ
одно из направлений логики, занимающихся ее основаниями, т.е. такими осн. понятиями и методами, к-рые при построении формальных логич. систем или исчислений предполагаются обычно не нуждающимися в пояснениях (содержательно понятными) и не анализируются. Особое внимание уделяется при этом понятиям переменной, функции, множества, различению типов переменных (предметные, предикатные, пропозициональные и др.), правилу подстановки, логич. антиномиям. В системах математической логики (призванных формализовать логич. выводы) правила вывода, хотя и формулируются содержательно, но, по идее, должны быть вполне доступны для одноактного автоматич. выполнения. Нек-рые из них, вроде известного modus ponens, позволяющего из выведенных уже формул А и (A ? B) вывести формулу В, представляются непосредственно удовлетво-ряющими этому требованию. В др. случаях, прежде всего для правила подстановки (особенно на место предикатных переменных), формулировка правила настолько сложна (требует введения ряда новых терминов, проверки выполнения или невыполнения трудно формулируемых условий), что даже квалифицированному специалисту бывает нелегко решить вопрос о ее корректности. Выполнить такое правило поэтому во многих случаях отнюдь не просто. В Л. к. правило подстановки сводится к цепочке правил, не более сложных, чем modus ponens. Анализ выявляет трудности и в др. упомянутых выше понятиях, формализацией (или устранением) к-рых и занимается Л. к. История Л. к. начинается с труда сов. математика М. И. Шейнфинкеля "О кирпичах матем. логики" [(М. Sch?nfinkel, ?ber die Bausteine der mathematischen Logik, "Math. Ann.", 1924, Bd 92); краткое пояснение смысла исходных функций Шейнфинкеля имеется в статье С. А. Яновской "Основания математики и математическая логика" (см. сб. "Математика в СССР за тридцать лет 1917–1947", 1948, с. 31–33) ], положившего в основу логики нек-рые три индивидуальные функции С, S, U (рассматриваемые как особые предметы, отличные от значений функций) и одну операцию: приложения функции к аргументу (к-рым может быть и функция), обозначаемую только тем, что знак аргумента ставится непосредственно за знаком функции. Функции от n аргументов (n-местные функции) сводятся Шейнфинкелем к функциям от одного аргумента (к одноместным функциям). Задание же последних не предполагает у него (в отличие от того, как это принято в т.н. классич. математике) предварит, задания множеств значений аргументов и значений функции. Понятие функции оказывается, т.о., независимым от понятия множества, с к-рым связаны большие трудности (см. Парадокс). Шейнфинкель полагал, что введенных им функций С, S, U достаточно для представления любых выражений математич. логики (в т.ч. и содержащих кванторы "все" и "существует") в виде слов в алфавите, состоящем только из трех латинских букв С, S, U и скобок. Выражения логики должны были сводиться, т.о., к комбинациям (с повторениями) из букв С, S, U (и скобок), откуда и название "Л. к." (предложенное в 1930 X. Керри). Употребление же переменных должно было быть вообще исключено из логики. Чтобы показать на простом примере, как это делается, рассмотрим комбинатор А такой, что Аху=х+у, и комбинатор С такой, что Cfxy=fyx; [приложение комбинатора А к аргументам х, у дает х+у; приложение комбинатора С к f(х, у) дает f(y, x) – в более обычных обозначениях ]. Сумму у +х в таком случае можно выразить как С Аху. Тождество х+у = у+х выражается при этом в виде Аху=САху. И если (как это делается обычно в математике) трактовать тождественное равенство f(х1, хп) = g(x1,..., хп) как другое выражение для того, что f=g (т.е. считать, что функции f и g, относящие обе одни и те же объекты к одним и тем же значениям аргументов, отождествляются нами), то другим выражением для тождества х+у=у+х будет А=CA – формула, не содержащая переменных. Как показало дальнейшее развитие идей Шейнфинкеля, их осуществление – в применении к той части Л. к., к-рая призвана была заменить уже и оперирование с кванторами, – оказалось отнюдь не столь простым, как это представлялось их автору, и потребовало дальнейших исследований. Среди последних выделяются прежде всего работы Керри. Первые работы Керри по Л. к. появились в 1929–30. В них он пользовался системой исходных функций ("комбинаторов"), отличной от введенной Шейнфинкелем, а также разработал технику вывода для Л. к., к-рой не было у Шейнфинкеля. Непротиворечивость той части системы Л. к., в к-рой еще нет аналога для кванторов (т.н. "чистой" Л. к.), также была доказана в этих работах Керри. В это же время Черчем было разработано его исчисление ?-конверсии, в к-ром были получены первые в истории науки доказательства неразрешимости нек-рых массовых проблем (см. Алгоритм, Разрешения проблемы). В диссертации "Математическая логика без переменных" (J. В. Rosser, A mathematical logic without variables, 1935) амер. математик Россер показал эквивалентность Л. к. и исчисления ?-конверсии. В том же 1935 Клини и Россер обнаружили противоречие в первоначальной системе Черча, к-рое, т.о., оказалось имеющим место и в применении к Л. к.: не к "чистой", а к "заключительной" (illative), включающей импликацию и аналоги для кванторов. Чтобы избежать этого противоречия, "заключительную" Л. к. приходится строить либо как неклассическую, либо как содержащую предметы разных (не сводимых друг к другу) категорий (что и было сделано Керри). В логику приходится, т.о., включать нек-рые сведения о предметах (о существовании разных категорий предметов и, следовательно, о нек-рых специфич. свойствах их), к-рые естественно относить уже к области онтологии или еще более конкретных наук, изучающих специфицированные предметы. В развитии Л. к., т.о., полностью подтверждаются принципы, ясные с т. зр. материалистич. диалектики: о неотделимости логики от онтологии, о роли противоречия в развитии науки, о способах "снятия" противоречия с помощью большей конкретизации исследуемых предметов и др. Поскольку в Л. к. исходным является понятие функции, а не множества, естественно, встает задача построить теорию множеств, исходя из Л. к. Такие попытки предприняли Керри в 1934 (опубликовано только резюме его работы) и Коген (1955), в работе к-рого (она посвящена обоснованию средствами Л. к. системы аксиом Геделя для теории множеств) нем. математик Титгемейер обнаружил, однако, противоречие, свидетельствующее о том, что попытка Когена не удалась. В 1952 Керри предложил использовать Л. к. при составлении программ для вычислит. машин. Лит.: Curry H., An analysis of logical substitution, "Amer. J. Math.", 1929, v. 51, p. 363–84; его же, Grundlagen der kombinatorischen Logik, там же, 1930, v. 52, p. 509–36; 789–834; его же, Foundations of the theory of abstract sets from the standpoint of combinatory logic, "Bull. Amer. Math. Soc.", 1934, v. 40, No 9, p. 654; eго же, The logic of program composition, в кн.: Applications scientifiques de la logique math?matique. Actes du 2-е colloque international de logique math?matique, Paris, 22–30 a?ut 1952, P. – Louvain, 1954, p. 97–102; Кleene S. С. and Rosser J. В., The inconsistency of certain formal logics, "Annales Mathem.", 1935, v. 36, ser. 2, p. 630–36; Cogan E. J., A formalization of the theory of sets from the point of view of combinatory logic, "Z. math. Logik und Grundlagen Math.", 1955, Bd 1, H. 3, S. 198–240; Curry H. and Feys R., Combinatory logic, v. 1, Amst., 1958 (имеется библиогр.); Titgemeyer R., ?ber einen Widerspruch in Cogans Darstellung der Mengenlehre, "Z. math. Logik und Grundl. Math.", 1961, Bd 7, H. 3. С. Яновская. Москва.

Источник: Философская Энциклопедия. В 5-х т.

КОМБИНАТОРНАЯ ЛОГИКА
направление в основаниях и философии математики, в котором в качестве основных понятий выбираются: функция (оператор) и операция аппликации (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; Sdinnnkel M. Uber 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 fur Math. Logik und Grundlagen der Mathematik», 1983, Bd 29. H. 5; Кузччева З. А., Ку:шчев А. С. Системы с бесконечной логикой м неограниченным принципом свертывания. К 150-летиюсо дня рождения Г. Кантора. — В кн.: Бесконечность в математике: философские и исторические аспекты. М., 1997; КузичевА. С. Вариант формализации канторовской теории множеств.—Доклады Российской Академии наук. 1999. т. 369, № 6; Он же. Решение проблемы Гильберта по Колмогорову. — Там же, 2000, т. 371. № 3.
А. С. Кузичев

Источник: Новая философская энциклопедия