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

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

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

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

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

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

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

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

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

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

Sxyz=xz(yz)

(распределитель),

Kxy=x

(вычёркиватель).

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

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

I=\lambda x.x=SKK

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

Y=\lambda h.((\lambda x.h(xx))(\lambda x.h(xx))).

История

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

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

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

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

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

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

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

См. также

Имеется викиучебник по теме «Комбинаторы — это просто!»

Примечания

↑ Под ред. Ф. В. Константинова. Логика комбинаторная // Философская Энциклопедия : в 5 т.. — М. : Советская энциклопедия, 1960—1970.
↑ Кондаков, 1971.
↑ ¹ ² ³ МЭС, 1988, с. 275—276.
↑ ¹ ² Филд, Харрисон, 1993, с. 291—293.
↑ Cardone F., Hindley J. R. History of lambda calculus and combinators (Архивная копия от 10 октября 2011 на Wayback Machine), in Handbook of the History of Logic, Volume 5, D. M. Gabbay and J. Woods (eds) (Amsterdam: Elsevier Co., to appear).
↑ Schonfinkel M. Uber die Baustein der mathematischen Logik. — Math. Annalen, vol. 92, 1924, p. 305—316.
↑ Curry H. B. Grundlagen der kombinatorischen Logik. American Journal of Mathematics, 52:509—536, 789—834, 1930.
↑ Curien P.-L. Categorical combinatory logic. — LNCS, 194, 1985, p. 139—151.

Литература

Вольфенгаген В. Э. Комбинаторная логика в программировании. Вычисления с объектами в примерах и задачах. — 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 с.

[1] Под ред. Ф. В. Константинова. Логика комбинаторная // Философская Энциклопедия : в 5 т.. — М. : Советская энциклопедия, 1960—1970.

[_4114281388f7cb8a-2] Кондаков, 1971.

[_fa5c11ae79adf128-3] ¹ ² ³ МЭС, 1988, с. 275—276.

[_f6a539f7aa0cf5b6-4] ¹ ² Филд, Харрисон, 1993, с. 291—293.

[5] Cardone F., Hindley J. R. History of lambda calculus and combinators (Архивная копия от 10 октября 2011 на Wayback Machine), in Handbook of the History of Logic, Volume 5, D. M. Gabbay and J. Woods (eds) (Amsterdam: Elsevier Co., to appear).

[6] Schonfinkel M. Uber die Baustein der mathematischen Logik. — Math. Annalen, vol. 92, 1924, p. 305—316.

[7] Curry H. B. Grundlagen der kombinatorischen Logik. American Journal of Mathematics, 52:509—536, 789—834, 1930.

[8] Curien P.-L. Categorical combinatory logic. — LNCS, 194, 1985, p. 139—151.

[1]

[2]

[3]

[4]

[5]

[6]

[7]

[8]