Комбинаторите станаха лесни!
Съдържание
Комбинаторната логика (от думата „комбинатор“, а не „комбинаторика“) е клон на математическата логика, разработен през първата половина на 20-ти век от логиците Мойсей Шейнфинкел и Хаскел Къри като наука за изчислителните процеси. Въпреки че първоначално този вид логика претендираше само за премахване на променливи от логически изявления, след известно време бяха получени приложени резултати в компютърните науки, показващи, че комбинаторната логика може да се използва за извършване на изчисления.
Комбинаторната логика може да се разглежда като известно опростяване на λ-смятането [1], при което няма символ λ, а всички функционални абстракции са представени от ограничен набор от символи, наречени „комбинатори“. Такива комбинатори не съдържат променливи, те са функции от по-висок ред, тоест те могат да приемат други функции като вход и също така описват определени правила за трансформиране на обекти, дадени им като аргументи.
С други думи, комбинаторната логика е формализъм за представяне на функционални зависимости между входовете и изходите. В този формализъм зависимостите и самите данни са написани в една и съща много ограничена азбука.
Основните обекти на комбинаторната логика, участващи във формалната система, определят самата комбинаторна логика. Нека дефинираме следните елементи на официалната система:
- Азбука.
- Твърдения (много добре оформени формули).
- Аксиоми.
- Правила за теглене.
Азбуката се разбира като набор от символи, разрешени в нотирането на термини в комбинаторната логика. Като цяло, използвайки нотацията на комбинаторната логика, можете да пишете обекти от няколко типа - константи, променливи, термини и специални знаци.
Константите се обозначават с малки букви от латинската азбука, вероятно с индекси. Обикновено символите от началото на азбуката се приемат за означаване на константи. Променливите също се означават с малки букви, вероятно с индекси, но обикновено се избират от края на азбуката: c 1>, c 2> са константи, x, y са променливи.
Понякога обаче ще се използва различна нотация за подчертаване на постоянни обекти. Този метод се състои в подчертаване на имената на константи в удебелен шрифт - този запис ще се използва, ако името на константата се състои от повече от един символ: i f>, t r u e>, p a i r> и други.
Комбинаторните термини (или просто „изрази“) ще се означават с главни букви от латинската азбука, вероятно също с индекси: M, N и т.н.
Както можете да видите, създаването на комбинаторни термини ще доведе до лавинообразно въвеждане на такива термини в скоби. За да се намали броят на скобите в комбинаторни записи на термини, се въвеждат конвенции за скоби, които се състоят във факта, че липсващите скоби се възстановяват чрез асоциативност вляво:
X Y Z = ((X Y) Z)
Като аксиоми, включени в набора от добре оформени формули, обикновено се разграничават следните:
Остава да се разгледат правилата за извод, които се използват в комбинаторната логика за трансформиране на един член в друг и описване на връзката на конвертируемост (=). Тези правила за извод по своята същност описват тази връзка, като уточняват нейните характеристики.
Както можете да видите, първите три правила са описание на свойствата на рефлексивност, симетрия и транзитивност. Съвкупността от тези свойства е характеристиките на отношението на еквивалентност, тоест отношението на конвертируемост (=) разделя целия набор от комбинаторни термини на някои класове на еквивалентност, спрямо които можем да кажем, че съдържащите се в тях термини са конвертируеми във всеки други (еквивалентни един на друг).
Освен това трябва да се отбележи, че под името на комбинатора ще се разбира символът, който го обозначава, подписът на комбинатора ще означава лявата страна на правилото, а характеристиката ще означава дясната страна на правилото, описващо самия комбинатор.
Тези комбинатори включват следното:
Тези комбинатори намаляват някои трансформации доста значително. [2]
Съвсем ясно е обаче, че всички изброени комбинатори могат да бъдат изразени един през друг. Следните формули показват изразяването на нови комбинатори по отношение на вече известни:
Внимателният читател е поканен да провери независимо тези формули. За да направите това, достатъчно е да използвате аксиомите за комбинаторите S> и K> и да замените променливите във формулите в дадено количество (според дефинициите).
Този пример също показа, че има безкрайно много начини за разлагане на обекти в комбинаторна основа, така че винаги има смисъл да се говори за „минимално“ разлагане, т.е. такова, което използва минималния брой комбинатори и скоби.
Тези правила използват ламбда нотация, която е приета в ламбда смятане. Съвсем лесно е да конвертирате комбинатор с неговия подпис и характеристика в λ-нотация - вместо символа, обозначаващ самия комбинатор, използвайте символа "λ", а вместо символа "=" използвайте точката ". ".
Този раздел съдържа текста на програма в Haskell, която преобразува дадения комбинатор в основата S>, K>, I>. За да разберете горните дефиниции, трябва да сте запознати със синтаксиса на този език на ниво, достатъчно за дефиниране на типове и функции. Разглеждането на тези теми е извън обхвата на тази статия, така че заинтересованият читател може да бъде насочен към специализираната литература.