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

ОБОБЩЕНИЕ

По темата: Дискретна математика

тема:

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

Студенти 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, AXY=AYX се извлича от A=CA.

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

Примери за комбинатори

Нека илюстрираме представената формална система от комбинаторна логика с необходимите примери за комбинатори. Помислете за характерните отношения за комбинатори, които по-късно ще се окажат теоретично интересни и практически полезни в този курс (някои от отношенията съвпадат с аксиомите, въведени по-рано):

(I) I a = a; Отношението (I), както вече беше отбелязано, характеризира комбинаторана идентичността.

(K) K ab = a; Отношението (K) характеризира комбинатора на първата проекция (наричан иначеотменител, т.е. "отменя" "изпълнението" на всички "инструкции" с изключение на първата).

(S) S abc = ac(bc); Отношението (S) характеризира комбинатора-конектор, който определя реда на "свързване" на "инструкциите" на програмата по такъв начин, че третата "инструкция" е "разпределена" върху двойка от първите две.

(B) B abc =a(bc); Отношението (B) характеризиракомбинатора за композиция, който формира последователност от комбинаторни термини и служи за комбиниране на по-елементарни "инструкции" в по-сложни и в крайна сметка в "програми".

(C) C abc = acb;

(W) W xy = xyy. Релациите (C) и (W) определят съответнопермутация (пермутация) идублиране на аргументи.

Конвенции за обозначения

За съжаление, относителната простота на описание на предишните етапи на формалната теория на комбинаторната логика (азбука, аксиоми и правила за извод) генерира доста тромави изчисления при моделиране на изчисления.

В тази връзка, от съображения за спестяване на място, се приемат следните настройки по подразбиране за извеждане на отношения, които позволяват значително намаляване на нотацията и увеличаване на удобството при четене и обработка на комбинаторни термини.

Първо, скобите за операциятаприложениесе възстановяват чрез асоцииранеleft, например:

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.

Използвайки аксиомите (K) и (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 г