Нечто про комбинаторы
Некоторое время назад, когда писа́л пятую главу к своей будущей книге, наткнулся на интересные комбинаторы, которые нашёл в методическом пособии В. Э. Вольфенгагена. Комбинаторы сии называются: формальная импликация (X), оператор функциональности (F), импликация (P), конъюнкция, дизъюнкция и отрицание. Более того, были ещё и кванторы всеобщности и существования, выраженные при помощи комбинаторов (я не стал включать их в книгу). Перечисленные комбинаторы выражаются друг через друга так:
X = C(BCF)I
F = B(CB2B)X
P = YX
& = B2(CXI)(C(CBB2P)P)
V = B2(CXI)(C(CBB2(B(F&))P)P)
! = CP(XWXI)
Весьма непростые выражения (в них комбинаторы B, B2, C, I, Y и F определяются стандартно). Однако одним из заданий к пятой главе является получение комбинаторных характеристик данных объектов. Что я и попытался сделать вчера. Начал с простого — X. Вот, что из этого вышло:
X = C(BCF)I =F C(BC(B(CB2B)X))I
Пробуем редуцировать данное выражение, подставляя вместо отсутствующих объектов свободные переменные (жирным выделяется редуцируемый на очередном шаге комбинатор):
C(BC(B(CB2B)X))Iab =C BC(B(CB2B)X)aIb =B C(B(CB2B)Xa)Ib =C B(CB2B)XabI =B CB2B(Xa)bI =C B2(Xa)BbI =B2 Xa(BbI)
Проводить редукцию далее нет никакого смысла, т. к. будет происходить «накрутка» выражения в скобках. Поэтому надо рассмотреть, что из себя представляет этот объект в скобках:
(BbI)c =B b(Ic) =I b(c) = bc
Из этой редукции следует по одному из пра́вил вывода комбинаторной логики, что (BbI) = b. Тогда получается, что:
Xab = Xab
Редукция вернула тот же самый объект. Что делать? Каков смысл этого? Кто это всё придумал?
![[info]](http://p-stat.livejournal.com/img/userinfo.gif){kind=small}
_darkus_) wrote,
