Дискретна математика

РЕФЕРАТ

На предмет: Дискретна математика

тема:

як формальна система

студентки 2 курсу 23 групи

Зміст

1. Визначення комбінатора

2. Комбінаторна логіка як формальна система: алфавіт,

аксіоми, правила виведення

Комбінаторна логіка: алфавіт

Комбінаторна логіка: побудова термів

Комбінаторна логіка: аксіоми

Комбінаторна логіка: правила виведення

3. Приклади комбінаторів

Угоди про позначення

Синтаксис комбінаторної логіки

Редукція комбінаторів

4. Визначення базису. Основні базиси комбінаторної

5. Приписування типів комбінаторам. Виведення типів

6. Приклади функцій базових комбінаторів SML

Запровадження

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

Далі буде представлено формальне запровадження типізований варіант комбінаторної логіки, спочатку запропонований Х. Каррі. Виклад формальної теорії буде проводитись у традиційній для математики послідовності:

алфавіт, аксіоми та правила виведення. Потім буде обговорюватися поняття базового набору комбінаторів: буде розглянуто кілька варіантів базисів, включаючи мінімально можливий.

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

Визначення комбінатора

Зміннаx називаєтьсявільною у ламбда-вираженні(термі) виду λx.A, якщо вона не має входжень у терм A; в іншому випадку змінна x називаєтьсязв'язаною.

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

Абстракція або λ-абстракція у свою чергу будує функції за заданими виразами. Саме якщо — вираз, що вільно містить x, тоді запис означає: функція λ від аргументу x, яка має вигляд t) позначає функцію . Таким чином, за допомогою абстракції можна конструювати нові функції. Вимога, щоб x вільно входило в t, не дуже суттєво - достатньо припустити, що якщо це не так.

Приклади:

Терм, що не містить вільних змінних, називається комбінатором.

Комбінаторна логіка як формальна система: алфавіт, аксіоми, правила виведення

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

Алфавіт - безліч допустимих символів.

Твердження – правилаутворення термінальних символів.

Аксіоми – елементарні твердження, істинність яких приймається без доказу.

Правила вывода – правила перетворення одних символів (об'єктів) мови на інші.

Правила виведення

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

(I) - аксіома рефлексивності рівності, а правила CR.1 та CR.2 - його

транзитивність та симетричність.

Два правила CR.3 і CR.4 - це конгруентність рівності.

Аксіоми (K) та (S) постулюють існування двох базисних перетворень

Аксіома (I) означає існування комбінатора (функції)тотожності, тобто. наявність тотожного перетворення, у якому будь-який аргумент відображається сам у себе.

Аксіома (K) означає існування комбінатора (функції) взяттяпершої проекції, тобто. першого елемента впорядкованої пари або першого списку. Інтуїтивно ясно, що ця аксіома близька до мов функціонального програмування, що оперує списками, і відповідає фундаментальній операції взяття головного (першого) елемента списку.

Якщо відновити опущені дужки, вони набудуть вигляду

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

Як іншийприклад можна навести комбінаторK(SKK), що реалізує функцію проекції на другий аргумент:

Дещо простіше це ж перетворення можна задати за допомогою комбінатораSK :

Таким чином, одне й те саме співвідношення вхід-вихід можна уявитиу мові комбінаторної логіки різними алгоритмічними перетвореннями.

Як додаткову ілюстрацію покажемо, як засобами комбінаторної логіки представити властивість комутативності додавання.

Легко перевірити, що комбінатор S(S(KS)(S(KK)S))(KS), який ми для

стислості позначимо за допомогою C, здійснює наступне перетворення.

Властивість комутативності додавання в аплікативному записі має вигляд

Оскільки CAxy=Ayx, те саме може бути представлено як Axy=CAxy. Оскільки змінні x і y грають лише допоміжну роль, можуть бути опущені. Результуючий запис, що виражає комутативність операції A, виглядає дуже просто.

Жодні змінні не потрібні, оскільки за правилами комбінаторної логіки для будь-яких двох термів X і Y з A = CA виводиться AXY = AYX.

A=CA ⇒ AX=CAX ⇒ AXY=CAXY ⇒ AXY=AYX

Приклади комбінаторів

Проілюструємо представлену формальну систему комбінаторної логіки необхідними прикладами комбінаторів. Розглянемо характеристичні співвідношення для комбінаторів, які згодом виявляться теоретично цікавими та практично корисними в даному курсі (деякі із співвідношень збігаються із введеними раніше аксіомами):

(I) I a = a; Співвідношення (I), як зазначалося, характеризує комбінатортотожності.

(3) (K) До ab = a; ).

(S) S abc = ac(bc); Співвідношення (S) характеризує комбінатор-конектор, який визначає порядок «зв'язування» «інструкцій» програми таким чином, що третя «інструкція» "розподіляється" по парі з двох перших.

(B) B abc =a(bc); Співвідношення (B) характеризує комбінаторкомпозиції, який утворює послідовність комбінаторних термів і служить для об'єднання більш елементарних «інструкцій» у складніші, а в результаті – в «програми».

(C) C abc = acb;

(W) W xy = xyy. Співвідношення (C) і (W) визначають відповіднопермутацію (перестановку) ідублювання аргументів.

Угоди про позначення

На жаль, відносна простота опису попередніх етапів формальної теорії комбінаторної логіки (алфавіту, аксіом та правил виведення) породжує досить громіздкі викладки при моделюванні обчислень.

У зв'язку з міркування економії простору для виведення співвідношень приймаються такі умовчання, що дозволяють значно скоротити запис і збільшити зручність прочитання та обробки комбінаторних термів.

По-перше, дужки для операціїаплікаціївідновлюються по асоціаціївліво, наприклад:

X Y = (X Y), X Y Z = ((X Y) Z), …

По-друге, надлишкові дужки можуть опускатися, наприклад:

(X Y) = X Y, ((X Y) Z) = X Y Z, …

Редукція комбінаторів

Редукція (перетворення для скорочення запису) комбінаторних термів можлива відповідно до правил виведення, аналогічним аксіомам (K) і (S).

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

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

У ході досліджень було з'ясовано, що редукція (перетворення для скорочення запису) комбінаторних термів можлива відповідно до правил виведення, аналогічних аксіом (K) і (S).

Проілюструємо моделювання механізму редукції наступним прикладом.

Приклад.Розглянемо комбінаторний терм виду S K K x.

Користуючись аксіомами (К) та (S), а також правилами виведення, зробимо редукцію терму:

S K K x = (за правилом S ) = K x (K x) = (за правилом K ) x.

В результаті отримуємо, що S K K x = x, звідки, з урахуванням аксіом та правила (I),

Бази комбінаторів

Безліч (мінімальної потужності) комбінаторів, через елементи якого висловимо довільний комбінатор, називається (мінімальним)базисом.

Мінімальний базис : .

Інші приклади базисів : ; ; .

Приклади.

Розкладання термів у базисі:

B = S(KS)K; W = SS (K (SKK)); C = S(BBS)(KK).

Розкладання у базисі – аналог програмування.

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

Необхідність продовження міркувань призводить до поняття базису.

Безліч (мінімальної потужності) комбінаторів, через елементи якого висловимо довільний комбінатор, називається (мінімальним) базисом.

Як виявляється, можна довести, що:

1) базис термів длякомбінаторної логіки дійсно існує (причому існує безліч можливих базисів);

2) для будь-якого базису справедливо, що він забезпечує уявлення довільного комбінаторного терму (через властивість повноти, яким володіє система комбінаторної логіки);

3) мінімальний базис складається з двох «інструкцій»-комбінаторів, наприклад, .

Наведемо ще кілька прикладів базисів: ; ; .

Розкладання термів у базисі для раніше розглянутих комбінаторів має вигляд:

B = S(KS)K; W = SS (K (SKK)); C = S(BBS)(KK).

Розкладання в базисі аналогічне програмування мовою базисних інструкцій.

Бібліографія

1) Комбінаторна логіка як формальна система

2) Доповідь на засіданні науково-дослідного семінару сектору логіки Інституту філософії РАН. 6 травня 2010 р.