Комбинаторная логика - это обозначение, которое устраняет необходимость в количественно выраженных переменных в математической логике. Он был введен Мозесом Шенфинкелем и Хаскеллом Карри, а в последнее время использовался в информатике в качестве теоретической модели вычислений и также как основа для разработки языков функционального программирования. Он основан на комбинаторах, которые были введены Шёнфинкелем в 1920 году с целью предоставления аналогичного способа построения функций - и удаления любого упоминания переменных - особенно в логика предиката. Комбинатор - это функция высшего порядка, которая использует только приложение функции и ранее определенные комбинаторы для определения результата на основе своих аргументов.
Комбинаторная логика изначально задумывалась как «предварительная логика», которая проясняет роль количественно определенных переменных в логике, по сути, путем их устранения. Другой способ устранения количественных переменных - это логика функтора предиката Quine . Хотя выразительная сила комбинаторной логики обычно превосходит логику первого порядка, выразительная сила логики функтора предиката идентична таковой логики первого порядка ( Куайн 1960, 1966, 1976 гг.).
Первоначальный изобретатель комбинаторной логики, Моисей Шёнфинкель, ничего не опубликовал по комбинаторной логике после своей оригинальной статьи 1924 года. Хаскелл Карри заново открыл комбинаторы, работая инструктором в Принстонском университете в конце 1927 года. В конце 1930-х годов Алонзо Черч и его студенты в Принстоне изобрели соперника формализм для функциональной абстракции, лямбда-исчисление, которое оказалось более популярным, чем комбинаторная логика. Результатом этих исторических непредвиденных обстоятельств было то, что до тех пор, пока теоретическая информатика не начала проявлять интерес к комбинаторной логике в 1960-х и 1970-х годах, почти все работы по этому предмету были выполнены Хаскеллом Карри и его учениками или Роберт Фейс в Бельгии. Карри и Фейс (1958) и Карри и др. (1972) рассматривают раннюю историю комбинаторной логики. Более современное рассмотрение комбинаторной логики и лямбда-исчисления вместе можно найти в книге Барендрегта, в которой рассматриваются модели Дана Скотт, разработанные для комбинаторной логики в 1960-е и 1970-е годы.
В информатике комбинаторная логика используется как упрощенная модель вычислений, используемых в теории вычислимости и теория доказательств. Несмотря на свою простоту, комбинаторная логика улавливает многие важные особенности вычислений.
Комбинаторную логику можно рассматривать как вариант лямбда-исчисления, в котором лямбда-выражения (представляющие функциональную абстракцию) заменены ограниченным набором комбинаторов, примитивные функции без свободных переменные. Лямбда-выражения легко преобразовать в комбинаторные выражения, а комбинаторное сокращение намного проще, чем лямбда-сокращение. Следовательно, комбинаторная логика использовалась для моделирования некоторых нестрогих языков функционального программирования и аппаратного обеспечения. Самой чистой формой этого представления является язык программирования Unlambda, единственными примитивами которого являются комбинаторы S и K, дополненные вводом / выводом символов. Unlambda не является практическим языком программирования, но представляет некоторый теоретический интерес.
Комбинаторной логике можно дать множество интерпретаций. Многие ранние работы Карри показали, как преобразовать наборы аксиом традиционной логики в уравнения комбинаторной логики (Hindley and Meredith 1990). Дана Скотт в 1960-х и 1970-х годах показала, как объединить теорию моделей и комбинаторную логику.
Лямбда-исчисление связано с объектами, называемыми лямбда-термами, которые могут быть представлены следующими тремя формами строк:
где - имя переменной, взятое из предопределенного бесконечного набора имен переменных, а и - лямбда-термины.
Термины формы называются абстракциями. Переменная v называется формальным параметром абстракции, а - телом абстракции. Член представляет функцию, которая, примененная к аргументу, связывает формальный параметр v с аргументом, а затем вычисляет результирующее значение - то есть возвращает , где каждое вхождение v заменено аргументом.
Термины формы называются приложениями. Вызов или выполнение функции модели приложения: функция, представленная , должна быть вызвана с в качестве аргумента, и вычисляется результат. Если (иногда называемый applicationand) является абстракцией, термин может быть сокращен: , аргумент, можно подставить в тело вместо формального параметра , и результатом является новый лямбда-термин, эквивалентный старому. Если лямбда-термин не содержит подтермов в форме тогда оно не может быть сокращено и, как говорят, находится в нормальной форме.
Выражение представляет результат взятия члена E и замены в нем всех свободных вхождений v на a. Таким образом, мы пишем
По соглашению, мы берем как сокращение для ( то есть приложение левоассоциативное ).
Мотивация для этого определения редукции заключается в том, что оно отражает существенное поведение всех математических функций. Например, рассмотрим функцию, которая вычисляет квадрат числа. Мы могли бы написать
(Использование "" для обозначения умножения.) x здесь - формальный параметр функции. Чтобы вычислить квадрат для определенного аргумента, скажем 3, мы вставляем его в определение вместо формального параметра:
To оценить получившееся выражение , нам пришлось бы прибегнуть к нашим знаниям умножения и числа 3. Поскольку любое вычисление - это просто композиция вычисления вычисления подходящие функции на подходящих примитивных аргументах, этого простого принципа подстановки достаточно, чтобы уловить основной механизм вычислений. Более того, в лямбда-исчислении такие понятия, как «3» и «» могут быть представлены без какой-либо необходимости во внешне определенных примитивных операторах или константах. В лямбда-исчислении можно идентифицировать термины, которые при соответствующей интерпретации ведут себя как число 3 и как оператор умножения q.v. Кодирование Чёрча.
Известно, что лямбда-исчисление по вычислительной мощности эквивалентно многим другим правдоподобным моделям вычислений (включая машины Тьюринга ); то есть любое вычисление, которое может быть выполнено в любой из этих других моделей, может быть выражено в лямбда-исчислении, и наоборот. Согласно тезису Черча-Тьюринга, обе модели могут выражать любые возможные вычисления.
Возможно, удивительно, что лямбда-исчисление может представлять любые мыслимые вычисления, используя только простые понятия абстракции функций и приложений, основанные на простой текстовой подстановке терминов вместо переменных. Но еще более примечательно то, что абстракции даже не требуется. Комбинаторная логика - это модель вычислений, эквивалентная лямбда-исчислению, но без абстракции. Преимущество этого заключается в том, что вычисление выражений в лямбда-исчислении довольно сложно, потому что семантика подстановки должна определяться с большой осторожностью, чтобы избежать проблем с захватом переменных. Напротив, вычисление выражений в комбинаторной логике намного проще, потому что нет понятия подстановки.
Поскольку абстракция - единственный способ создания функций в лямбда-исчислении, что-то должно заменить ее в комбинаторном исчислении. Вместо абстракции комбинаторное исчисление предоставляет ограниченный набор примитивных функций, из которых могут быть построены другие функции.
Комбинаторные термины имеют одну из следующих форм:
Синтаксис | Имя | Описание |
---|---|---|
x | Переменная | Символ или строка, представляющие комбинаторный термин. |
P | Примитивная функция | Один из символов комбинатора I, K, S. |
(M N) | Приложение | Применение функции к аргументу. M и N - комбинаторные термины. |
Примитивные функции - это комбинаторы или функции, которые, если их рассматривать как лямбда-термы, не содержат свободных переменных.
Чтобы сократить обозначения, общее соглашение таково, что или даже , обозначает термин . Это то же общее соглашение (левоассоциативность), что и для множественного применения в лямбда-исчислении.
В комбинаторной логике каждый примитивный комбинатор имеет правило редукции вида
, где E - термин, упоминающий только переменные из набора {x 1... x n }. Таким образом, примитивные комбинаторы ведут себя как функции.
Простейшим примером комбинатора является I, тождественный комбинатор, определяемый как
для всех членов x. Другой простой комбинатор - K, который производит постоянные функции: (K x) - это функция, которая для любого аргумента возвращает x, поэтому мы говорим
для всех членов x и y. Или, следуя соглашению для множественного приложения,
Третий комбинатор - S, который является обобщенной версией приложения:
Sприменяет x к y после первой подстановки z в каждый из них. Или, другими словами, x применяется к y внутри среды z.
Данные S и K, Iсами по себе не нужны, поскольку его можно построить из двух других:
для любого члена x. Обратите внимание, что хотя ((SKK ) x) = (I x) для любого x, (SKK ) само по себе не равно I . Мы говорим термины экстенсивно равны. Экстенсиональное равенство отражает математическое понятие равенства функций: две функции равны, если они всегда производят одинаковые результаты для одних и тех же аргументов. Напротив, сами термины вместе с сокращением примитивных комбинаторов охватите понятие интенсионального равенства функций: две функции равны, только если они имеют идентичные реализации, вплоть до раскрытия примитивных комбинаторов, когда эти комбинаторы применяются к достаточному количеству аргументов.Существует много способов реализовать функцию идентичности; (SKK ) и I входят в число этих способов. (SKS ) - это еще один. Мы будем использовать слово «эквивалент» для обозначения экстенсионального равенства, оставляя за собой равные для идентичных комбинаторных терминов.
Более интересным комбинатором является комбинатор с фиксированной точкой или Y комбинатор, который может использоваться для реализации рекурсии.
Sи K могут быть составлены для создания комбинаторов, которые экстенсивно равны любому лямбда-члену и, следовательно, согласно тезису Чёрча, любой вычислимой функции вообще. Доказательство состоит в том, чтобы представить преобразование T [], которое преобразует произвольный лямбда-член в эквивалентный комбинатор.
T [] может быть определено следующим образом:
Обратите внимание, что T [], как указано, не является хорошо типизированной математической функцией, а скорее средство переписывания терминов: хотя оно в конечном итоге дает комбинатор, преобразование может генерировать промежуточные выражения, которые не являются ни лямбда-терминами, ни комбинаторами, с помощью правила (5).
Этот процесс также известен как устранение абстракции. Это определение является исчерпывающим: любое лямбда-выражение будет подчиняться ровно одному из этих правил (см. Сводка по лямбда-исчислению выше).
Это связано с процессом абстракции скобок, который берет выражение E, построенное из переменных и приложения, и производит выражение комбинатора [x] E, в котором переменная x не свободна, так что [x] E x = E. Очень простой алгоритм абстракции скобок определяется индукцией по структуре выражений следующим образом:
Абстракция скобок индуцирует перевод от лямбда-терминов к выражениям комбинатора, интерпретируя лямбда-абстракции с использованием алгоритма абстракции скобок.
Например, мы преобразуем лямбда-член λx.λy. (yx) в комбинаторный член:
Если мы применим этот комбинаторный термин к любым двум членам x и y (подавая их в порядке очереди в комбинатор «справа»), он уменьшится следующим образом:
Комбинаторное представление, ( S(K(SI )) (S(KK ) I)) намного длиннее, чем представление в виде лямбда-члена λx.λy. (yx). Это типично. В общем, конструкция T [] может расширить лямбда-член длины n до комбинаторного члена длины Θ (n).
Преобразование T [] мотивировано желанием устранить абстракцию. Два особых случая, правила 3 и 4, тривиальны: λx.x явно эквивалентно I, а λx.E явно эквивалентно (K T [E]), если x не выглядит свободным в E.
Первые два правила также просты: переменные преобразуются в самих себя, а приложения, которые разрешены в комбинаторных терминах, преобразуются в комбинаторы просто путем преобразования аппликатора и аргумента в комбинаторы.
Интересны правила 5 и 6. Правило 5 просто говорит, что чтобы преобразовать сложную абстракцию в комбинатор, мы должны сначала преобразовать его тело в комбинатор, а затем исключить абстракцию. Правило 6 фактически устраняет абстракцию.
λx. (E₁ E₂) - это функция, которая принимает аргумент, например a, и заменяет его на лямбда-член (E₁ E₂) вместо x, получая (E₁ E₂) [x: = a]. Но подстановка a в (E₁ E₂) вместо x - это то же самое, что замена его в E₁ и E₂, поэтому
По экстенсиональному равенству
Следовательно, чтобы найти комбинатор, эквивалентный λx. (E₁ E₂), достаточно найти комбинатор, эквивалентный (S λx.E₁ λx. E₂) и
, очевидно, отвечает всем требованиям. E₁ и E₂ содержат строго меньше приложений, чем (E₁ E₂), поэтому рекурсия должна заканчиваться лямбда-термом без каких-либо приложений вообще - либо переменной, либо члена формы λx.E.
Комбинаторы, генерируемые преобразованием T [], могут быть уменьшены, если мы примем во внимание правило η-редукции:
λx. (E x) - функция, которая принимает аргумент x и применяет функцию E к Это; это экстенсивно равно самой функции E. Поэтому достаточно преобразовать E в комбинаторную форму.
Принимая во внимание это упрощение, приведенный выше пример выглядит следующим образом:
Этот комбинатор эквивалентен более раннему, более длинному:
Аналогично исходная версия преобразование T [] преобразовало тождественную функцию λf.λx. (fx) в (S(S(KS ) (S(KK ) I)) (KI )). С помощью правила η-редукции λf.λx. (f x) преобразуется в I.
Существуют одноточечные базисы, из которых любой комбинатор может быть составлен экстенсивно равным любому лямбда-члену. Простейшим примером такого базиса является {X }, где:
Нетрудно проверить, что:
Поскольку {K, S} является основой, отсюда следует, что {X } также является основой. В языке программирования Iota в качестве единственного комбинатора используется X .
Другой простой пример одноточечного базиса:
На самом деле существует бесконечно много таких баз.
В дополнение к S и K, статья Шёнфинкеля включала два комбинатора, которые теперь называются B и C со следующими сокращениями:
Он также объясняет, как они в поворот можно выразить только с помощью S и K:
Эти комбинаторы чрезвычайно полезны при переводе логики предикатов или лямбда-исчисления в выражения комбинатора. Они также использовались Карри, а гораздо позже Дэвидом Тернером, имя которого было связано с их вычислительным использованием. Используя их, мы можем расширить правила преобразования следующим образом:
Использование комбинаторов B и C, преобразование λx.λy. (yx) выглядит следующим образом:
И действительно, (CIxy) сокращается до (yx):
Мотивация здесь в том, что B и C являются ограниченными версиями S . В то время как S принимает значение и подставляет его как в приложение, так и в свой аргумент перед выполнением приложения, C выполняет замену только в приложении, а B только в споре.
Современные названия комбинаторов взяты из докторской диссертации Хаскелла Карри 1930 г. (см. Система B, C, K, W ). В исходной статье Шенфинкеля то, что мы сейчас называем S, K, I, Bи C, называлось S, C, I, Zи T соответственно.
Уменьшение размера комбинатора, которое является результатом новых правил преобразования, также может быть достигнуто без введения B и C, как показано в разделе 3.2.
Следует проводить различие между CLK, описанным в этой статье, и исчислением CLI. Различие соответствует различию между вычислением λ K и λ I. В отличие от исчисления λ K, исчисление λ I ограничивает абстракции до:
Как следствие, комбинатор K не присутствует ни в исчислении λ I, ни в исчислении CLI. Константы CLI: I, B, Cи S, которые образуют основу, из которой могут быть составлены все члены CLI(по модулю равенства). Каждый член λ I может быть преобразован в равный комбинатор CLIв соответствии с правилами, аналогичными приведенным выше для преобразования членов λ K в комбинаторы CLK. См. Главу 9 в Barendregt (1984).
Преобразование L [] из комбинаторных членов в лямбда-члены тривиально:
Обратите внимание, однако, что это преобразование не является обратным преобразованием какой-либо из версий T [], которые мы видели.
A нормальная форма - это любой комбинаторный термин, в котором встречающиеся примитивные комбинаторы, если таковые имеются, не применяются к достаточному количеству аргументов для упрощения. Непонятно, имеет ли общий комбинаторный термин нормальную форму; эквивалентны ли два комбинаторных члена и т. д. Это равносильно неразрешимости соответствующих проблем для лямбда-членов. Однако прямое доказательство выглядит следующим образом:
Во-первых, член
не имеет нормальной формы, потому что он сводится к самому себе после трех шагов, как показано ниже:
и, очевидно, никакой другой порядок сокращения не может сделать выражение короче.
Теперь предположим, что N был комбинатором для обнаружения нормальных форм, такой что
Теперь пусть
теперь рассмотрим член (SIIZ). Имеет ли (SIIZ) нормальную форму? Это происходит тогда и только тогда, когда также выполняется следующее:
Теперь нам нужно применить N к (SIIZ). Либо (SIIZ) имеет нормальную форму, либо нет. Если он имеет нормальную форму, то вышесказанное сокращается следующим образом:
, но Ω не имеет нормальной формы, Итак, мы получили противоречие. Но если (SIIZ) не имеет нормальной формы, вышесказанное сокращается следующим образом:
, что означает, что нормальная форма (SIIZ) - это просто I, еще одно противоречие. Следовательно, гипотетический комбинатор нормальной формы N не может существовать.
Комбинаторный логический аналог теоремы Райса гласит, что не существует полного нетривиального предиката. Предикат - это комбинатор, который при применении возвращает либо T, либо F . Предикат N является нетривиальным, если есть два аргумента A и B такие, что N A = T и N B = F . Комбинатор N является полным тогда и только тогда, когда N M имеет нормальную форму для каждого аргумента M. Тогда аналог теоремы Райса говорит, что каждое полное pr edicate тривиально. Доказательство этой теоремы довольно просто.
Доказательство: Путем сокращения до абсурда. Предположим, что существует полный нетривиальный предикат, скажем N . Поскольку N предполагается нетривиальным, существуют комбинаторы A и B такие, что
Теорема о фиксированной точке дает: АБСУРДУМ = (ОТРИЦАНИЕ АБСУРДМ), для
Поскольку N должно быть полным либо:
Следовательно (N ABSURDUM) не является ни T, ни F, что противоречит предположению о том, что N будет - полный нетривиальный предикат. Q.E.D.
Из этой теоремы неразрешимости сразу следует, что не существует полного предиката, который мог бы различать термины, имеющие нормальную форму, и термины, не имеющие нормальной формы. Также следует, что не существует никакого полного предиката, скажем EQUAL, такого что:
Если бы EQUAL существовало, то для всех A λx. (EQUAL x A) должно было бы быть полным нетривиальным предикатом.
Дэвид Тернер использовал свои комбинаторы для реализации языка программирования SASL.
Кеннет Э. Айверсон использовал примитивы на основе о комбинаторах Карри в его языке программирования J, преемнике APL. Это позволило Айверсону называться неявным программированием, то есть программированием в функциональных выражениях, не содержащих переменных, а также мощными инструментами для работы с такими программами. Оказывается, неявное программирование возможно на любом APL-подобном языке с пользовательскими операторами.
Изоморфизм Карри – Ховарда подразумевает связь между логикой и программирование: каждое доказательство теоремы интуиционистской логики соответствует сокращению типизированного лямбда-члена и наоборот. Более того, теоремы можно отождествить с сигнатурами функционального типа. В частности, типизированная комбинаторная логика соответствует системе Гильберта в теории доказательств.
Комбинаторы K и S соответствуют аксиомам
и применение функции соответствует отстранению (modus ponens) правило
Исчисление, состоящее из AK, ASи MP, является полным для импликационного фрагмента интуиционистской логики, который можно рассматривать как следует. Рассмотрим множество W всех дедуктивно замкнутых наборов формул, упорядоченных по включению. Тогда - это интуиционистский фрейм Крипке, и мы определяем модель в этом кадре по
Это определение подчиняется условиям выполнения →: с одной стороны, если и таково, что и , затем по modus ponens. С другой стороны, если , то по теореме дедукции, следовательно, дедуктивное замыкание - элемент такой, что , и .
Пусть A будет любой формулой, которая не доказуема в исчислении. Then A does not belong to the deductive closure X of the empty set, thus , and A is not intuitionistically valid.