Комбінатори – це просто!

Зміст

Комбінаторна логіка (від слова «комбінатор», а не «комбінаторика») — це напрям у математичній логіці, розроблений у першій половині XX століття логіками Мойсеєм Шейнфінкелем та Хаскеллом Каррі як науку про обчислювальні процеси. Хоча спочатку цей вид логіки претендував лише на те, щоб видалити з логічних висловлювань змінні, через деякий час в інформатиці були отримані прикладні результати, що показали, що комбінаторну логіку можна використовувати для обчислень.

На комбінаторну логіку можна як на деяке спрощення λ-числения [1] , у якому немає символу λ, проте функціональні абстракції представлені обмеженим набором символів, званих «комбінаторами». Такі комбінатори не містять змінних, є функціями вищого порядку, тобто як аргументи можуть приймати на вхід інші функції, а також описують певні правила перетворення об'єктів, поданих їм на вхід як аргументи.

Іншими словами, комбінаторна логіка - це формалізм для представлення функціональних залежностей між вхідними та вихідними даними. У цьому формалізмі залежності і самі дані записуються в тому самому дуже обмеженому алфавіті.

Базові об'єкти комбінаторної логіки, що у формальної системі, визначають саму комбінаторну логіку. Визначимо такі елементи формальної системи:

Алфавіту.
Твердження (множина правильно побудованих формул).
Аксіоми.
Правила виведення.

Під алфавітом розуміється набір символів, допустимих нотації записів термів у комбінаторної логіці. Загалом за допомогою нотації комбінаторної логіки можна записувати об'єкти кількох типів - константи, змінні, термита спеціальні знаки.

Константи позначаються малі літери латинського алфавіту, можливо з індексами. Зазвичай для позначення констант беруться символи початку алфавіту. Змінні позначаються також малими літерами, можливо, з індексами, але вони зазвичай вибираються з кінця алфавіту: c 1 > , c 2 & gt; - Константи, 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 > . Для того, щоб розуміти наведені визначення,необхідно бути знайомим із синтаксисом цієї мови на рівні, достатньому для визначення типів та функцій. Розгляд цих тем виходить за межі цієї статті, тому зацікавленого читача можна надіслати до спеціалізованої літератури.

Для перетворення комбінаторів необхідно спочатку визначити тип даних їхнього представлення. Відповідно до визначення комбінаторного терму визначення такого типу виглядає так:

Це визначення повністю відповідає математичному, яке свідчить, що комбінаторний терм - це або змінна (Var - від англійського слова "variable"), або абстракція (Lam & gt; - від англійського слова "lambda"), або додаток одного комбінаторного терму до іншого ( App - від англійського слова "application").

Для того щоб мати можливість переглядати отримані результати перетворення комбінаторних термів, необхідно визначити тип Combinator екземпляром класу Show, який є класом величин, які можуть бути відображені. Звичайно, інтерпретатор мови Haskell може самостійно визначити такий екземпляр, але зробить це не так красиво, як можна зробити вручну. Тому вводиться таке визначення:

Тут видно, що змінна відображається просто своїм ім'ям, яке є рядком символів. Застосування комбінаторних термів один до одного просто записується перерахуванням комбінаторних термів один за одним із взяттям у дужки, якщо другий терм складний. А абстракція записується за допомогою символу (\) із зазначенням сигнатури та характеристики.

Додатково, хоча це й не обов'язково, можна реалізувати предикат, який перевіряє, чи є задана змінна вільною в комбінаторному термі, що досліджується. Цей предикат визначається так:

Все в повній відповідності доматематичним визначенням.

Якщо передати це визначення функції transform, то на виході буде така конструкція: S(S(KS)(S(KK)(S(KS)(S(KK)I)))))(K(S(S(KS)( S(KK)I))(KI)))!

Було б дивно, якби комбінаторна логіка не могла бути тим інструментом, за допомогою якого можна було б висловлювати різні об'єкти. Дійсно, формалізм комбінаторної логіки, незважаючи на дуже обмежений алфавіт, є цілком достатнім для вираження таких базових понять математики, як булеві значення істини, упорядковані пари деяких значень, натуральні числа, списки. Це, своєю чергою, дозволяє практично повністю змоделювати теорію функціонального програмування у межах простої комбінаторної логіки.

Сам собою спосіб кодування даних у рамках комбінаторної логіки не є досить виразним, більше того, іноді здається, що таке кодування химерно і надумано. З точки зору ефективності обчислень також є проблеми - оптимізація в прикладних трансляторах мов програмування дозволяє кодувати та проводити обчислення над закодованими даними ефективніше. Однак цей спосіб кодування даних є досить цікавим з точки зору математики, оскільки дозволяє зрозуміти, в тому числі, і те, що дані можуть нести в собі та способи їх обробки.

Булеві значення

Справді, запропонований спосіб кодування можна легко перевірити:

Цілком природно, що над представленими значеннями істинності повинні бути функції до виконання базових операцій булевої логіки. Такі базові операції може бути виражені через умовні висловлювання. Способи кодування трьох базисних булевих операцій (заперечення, кон'юнкція та диз'юнкція) виглядають так:

Читачевіпропонується самостійно перевірити дані тотожності щодо їх вірності. І тому необхідно розглянути таблиці істинності для перелічених логічних операцій та порівняти їх із традиційними таблицями істинності.

Нумерали Чорча

Цілком зрозуміло, що для кодування чисел або подібних до них об'єктів можна використовувати будь-який спосіб вираження, головне, що потім на такому способі можна було б побудувати прийнятні операції, тотожні тим, що визначені для чисел. Тому, власне, способів кодування чисел існує багато. Але найпершим способом був той, що запропонований А. Чорчем, і тепер має назву «нумерали Черча».

і так далі. Тобто щодо індукції ці об'єкти можна визначити як:

За своєю суттю ці комбінатори створюють ітеративне застосування заданої функції до деякого аргументу, причому кількість ітерацій дорівнює числу, що визначається нумералом:

Для цих об'єктів досить простим способом можна визначити функції для додавання, множення та зведення в ступінь. Це робиться так:

Доказ цих тотожностей легко проводиться за індукцією та пропонується для самостійного опрацювання.

Упорядковані пари

Ще один досить важливий об'єкт, що має велике практичне значення у функціональному програмуванні, є впорядкована пара, що складається з двох значень. З пар створюються списки та облікові структури, які у свою чергу є одним із основних об'єктів обробки у функціональних мовах. [3]

Для кодування пари за допомогою комбінаторних термів необхідно створити функцію, яка є конструктором такої пари. Це можна зробити так:

Цей комбінатор складає пару з двох заданих об'єктів будь-якої природи.Для того, щоб дістати ці об'єкти з пари, необхідні так звані селектори, тобто функції для доступу до елементів пари. Ці селектори можна визначити так:

Ці комбінатори «виймають» перше або друге значення переданої їм на вхід пари. Наприклад, можна довести, що вираз:

h e a d (p a i r x y) = x (\mathbf \, x \, y) = x & gt;

Загальні зауваження

Слід зазначити, що запропоновані способи кодування даних та методів для їх обробки за допомогою інструментів комбінаторної логіки є скоріше не заданою догмою, але шаблонами, за якими можна проводити обчислення над закодованими даними. Якщо розглянути такі способи кодування докладніше, то видно, що і нумерали Черча, і впорядковані пари можуть приймати на вхід не тільки значення для кодування, але і функції для їх обробки.

Так, визначення пари є досить універсальним – воно не обмежує поняття впорядкованої пари якимись спеціальними рамками, а залишає розробнику вибирати спосіб упакування об'єктів у пару. Тому будь-яка пара як функція очікує на вхід деяку функцію двох аргументів, яка після застосування повертає до початкових об'єктів і визначає саму пару. Це означає, що й операції для розпакування пари (селектори) мають бути різними у кожному конкретному випадку. Наведені вище визначення є шаблонами. Однак і ці шаблони власними силами також працюють.

Всі ці міркування стосуються інших прикладів. Це означає, що комбінаторна логіка надає вченим і розробникам універсальний інструмент абстрактного проектування методів на вирішення широкого класу завдань.

Розглянуте у цій статті запровадження основи комбінаторної логіки не претендує на цілісність викладу,та й неможливо у малій науково-популярній статті викласти складну науку про обчислення, на якій засновано реалізацію багатьох функціональних мов програмування. Тому всіх зацікавлених читачів можна надіслати до вивчення комбінаторної логіки та λ-обчислення за підручниками, що повноцінно описує ці найцікавіші напрямки логіки. Як напрями для подальшого вивчення можна порадити розглянути такі питання:

Автор оригінального тексту статті дякує Антонюку Д. А., який допоміг написати функції мовою Haskell для трансформації комбінаторних термів у базис S > , K > , I >