Комбина́торная ло́гика — направление математической логики , занимающееся фундаментальными (то есть не нуждающимися в объяснении и не анализируемыми) понятиями и методами формальных логических систем или исчислений . В дискретной математике комбинаторная логика тесно связана с лямбда-исчислением , так как описывает вычислительные процессы.

С момента своего возникновения комбинаторная логика и лямбда-исчисление были отнесены к неклассическим логикам . Дело заключается в том, что комбинаторная логика возникла в 1920-х годах, а лямбда-исчисление — в 1940-х годах как ветвь метаматематики с достаточно очерченным предназначением — дать основания математике. Это означает, что сконструировав требуемую «прикладную» математическую теорию — предметную теорию, — которая отражает процессы или явления в реальной внешней среде, можно воспользоваться «чистой» метатеорией как оболочкой для выяснения возможностей и свойств предметной теории. Вскоре также оказалось, что обе эти системы можно рассматривать как языки программирования (см. также комбинаторное программирование ).

К настоящему времени оба эти языка не только стали основой для всей массы исследований в области информатики , но и широко используются в теории программирования. Рост вычислительной мощности компьютеров привёл к автоматизации значительной части теоретического (логического и математического) знания, а комбинаторная логика вместе с лямбда-исчислением признаются основой для рассуждений в терминах объектов ^{[ источник не указан 3470 дней ]} .

Основные понятия

В комбинаторной логике в качестве основных понятий выступает одноместная функция и операция применения функции к аргументу ( аппликация ). Понятие функции принимается первичным по отношению к понятию множества . Функция понимается обобщённо и может оперировать с объектами равного ей уровня в качестве аргументов и значений. Так как аргументом функции может быть функция, многоместную функцию можно свести к одноместным .

Комбинатором называется функция ${\displaystyle f}$ , которая удовлетворяет равенству

${\displaystyle fg_{1}g_{2}\dots g_{n}=(\dots ((fg_{1})g_{2})\dots g_{n})=X,}$

где ${\displaystyle g_{1},g_{2},\dots ,g_{n}}$ ( ${\displaystyle n\geqslant 1}$ ) — некоторые функции, X — объект, построенный из функций применением аппликации .

Любой комбинатор может быть выражен через два комбинатора S и К , определённые следующими равенствами :

${\displaystyle Sxyz=xz(yz)}$ ( распределитель ),

${\displaystyle Kxy=x}$ ( вычёркиватель ).

По данному лямбда-выражению можно всегда построить аппликативное выражение . Для этого необходимо всего два комбинатора: S и K . В виде лямбда-выражений: ${\displaystyle K=\lambda x.\lambda y.x}$ , ${\displaystyle S=\lambda f.\lambda g.\lambda x.fx(gx)}$ . То есть, комбинаторную логику, определённую на этих комбинаторных объектах, можно рассматривать как модель лямбда-исчисления .

Другими примерами комбинаторов (в записи лямбда-исчисления) могут служить функция тождества , легко выражаемая через S и K :

${\displaystyle I=\lambda x.x=SKK}$

и комбинатор неподвижной точки или Y-комбинатор :

${\displaystyle Y=\lambda h.((\lambda x.h(xx))(\lambda x.h(xx))).}$

История

В 1920 году комбинаторы как специальные математические сущности первоначально были введены М. Шейнфинкелем . Несколькими годами позже они независимо были переоткрыты Х. Карри , благодаря которому с тех пор были выполнены основные продвижения в комбинаторной логике (хотя другие исследователи, например, Россер, в различное время также участвовали в этой работе). Почти в то же самое время Чёрчем , Россером и Клини было начато развитие λ-конверсии.

С 1970-х годов комбинаторы использовались в трёх главных аспектах: во-первых, для построения логических систем , основанных на абстрактной записи операции; во-вторых, в теории доказательств как основа записи конструктивных функций различного вида; в-третьих, при построении и анализе некоторых языков программирования в компьютерных науках .

Категориальная комбинаторная логика

В рамках комбинаторной логики строится специальный вариант теории вычислений, называемый категориальной абстрактной машиной . Для этого вводится в рассмотрение особый фрагмент комбинаторной логики — категориальная комбинаторная логика . Она представлена набором комбинаторов, каждый из которых имеет самостоятельное значение как инструкция системы программирования. Тем самым в комбинаторную логику встраивается ещё одно полезное приложение — система программирования, основанная на декартово замкнутой категории (д. з. к.). Это позволяет ещё раз на новом уровне переосмыслить связь операторного и аппликативного стиля программирования.

Иллативная комбинаторная логика

Пользуясь представлениями об объектах как абстрактных математических сущностях, обладающих определёнными подстановочными свойствами, можно строить системы логических рассуждений . Наиболее известная среди таких систем основана на комбинаторах.

Логика , основанная на комбинаторах, или иллативная комбинаторная логика , строится из теории комбинаторов или лямбда-исчисления, расширенного дополнительными константами — экстра-константами , — вместе с соответствующими аксиомами и правилами вывода, которые обеспечивают средства дедуктивного вывода.

См. также

• Аппликативные вычислительные системы
• Функциональное программирование
• Типизированное лямбда-исчисление

Примечания

Литература

• Вольфенгаген В. Э. Комбинаторная логика в программировании. Вычисления с объектами в примерах и задачах. — 2-е изд.. — М. : АО Центр ЮрИнфоР, 2003. — 204 с. — ISBN 5-89158-101-9 .
• Кондаков Н. И. Логический словарь / Горский Д. П.. — М. : Наука, 1971. — 656 с.
• Филд А., Харрисон П. Функциональное программирование = Functional Programming. — М. : Мир, 1993. — 637 с. — ISBN 5-03-001870-0 .
• Математический энциклопедический словарь / Ю. В. Прохоров. — М. : Советская энциклопедия, 1988. — 847 с.
• А. С. Кузичев. // Новая философская энциклопедия : в 4 т. / пред. науч.-ред. совета В. С. Стёпин . — 2-е изд., испр. и доп. — М. : Мысль , 2010. — 2816 с.