Студопедия

КАТЕГОРИИ:


Архитектура-(3434)Астрономия-(809)Биология-(7483)Биотехнологии-(1457)Военное дело-(14632)Высокие технологии-(1363)География-(913)Геология-(1438)Государство-(451)Демография-(1065)Дом-(47672)Журналистика и СМИ-(912)Изобретательство-(14524)Иностранные языки-(4268)Информатика-(17799)Искусство-(1338)История-(13644)Компьютеры-(11121)Косметика-(55)Кулинария-(373)Культура-(8427)Лингвистика-(374)Литература-(1642)Маркетинг-(23702)Математика-(16968)Машиностроение-(1700)Медицина-(12668)Менеджмент-(24684)Механика-(15423)Науковедение-(506)Образование-(11852)Охрана труда-(3308)Педагогика-(5571)Полиграфия-(1312)Политика-(7869)Право-(5454)Приборостроение-(1369)Программирование-(2801)Производство-(97182)Промышленность-(8706)Психология-(18388)Религия-(3217)Связь-(10668)Сельское хозяйство-(299)Социология-(6455)Спорт-(42831)Строительство-(4793)Торговля-(5050)Транспорт-(2929)Туризм-(1568)Физика-(3942)Философия-(17015)Финансы-(26596)Химия-(22929)Экология-(12095)Экономика-(9961)Электроника-(8441)Электротехника-(4623)Энергетика-(12629)Юриспруденция-(1492)Ядерная техника-(1748)

Умолчания




Аксиомы комбинаторной логики

После определения алфавита и порядка построения допустимых комбинаторных выражений посредством операции аппликации, перечислим аксиомы комбинаторной логики.

Отметим, что символ "=" понимается в комбинаторной логике как обозначение отношения конвертируемости, которым связываются соединенные этим значком комбинаторные термы. Конвертируемость двух комбинаторных термов означает, что один комбинаторный терм может быть преобразован к другому. Отношение конвертируемости моделирует переобозначения и во многих отношениях, как отмечалось ранее, напоминает процесс программирования.

Следующие аксиомы задают свойства отношения конвертируемости:

Аксиома (I) Ix = x существования комбинатора (функции) тождества, т.е. наличие тождественного преобразования, при котором любой аргумент отображается сам в себя
Аксиома (K) Kxy = x существование комбинатора (функции) взятия первой проекции, т.е. первого элемента упорядоченной пары или первого элемента списка*
Аксиома (S) Sxyz = xz(yz) попарного связывания третьего элемента с первыми двумя

* Аксиома (K) близка языкам функционального программирования, оперирующим списками, и соответствует фундаментальной операции взятия головного (первого) элемента списка.

 

Перечислим правила вывода комбинаторных термов, которые задают характеристики отношения конвертируемости и их свойства:

(μ) если a=b, то ca=cb  
(ν) если a=b, то ac=bc  
(ρ) a=a рефлексивность - конвертируемость произвольного комбинаторного выражения к самому себе
(σ) если a=b, то b=a симметричность - двунаправленность вывода комбинаторных выражений посредством конверсии
(τ) если a=b и b=c, то a=c транзитивность - возможность опускать промежуточные этапы конверсии для цепочек вывода

Как видно, отношение конвертируемости обладает, в частности, свойствами рефлексивности, симметричности и транзитивности.

К сожалению, относительная простота описания предыдущих этапов формальной теории комбинаторной логики (алфавита, аксиом и правил вывода) порождает довольно громоздкие выкладки при моделировании вычислений.

В этой связи из соображений экономии пространства для вывода соотношений принимаются следующие умолчания, позволяющие значительно сократить запись и увеличить удобство прочтения и обработки комбинаторных термов.

1. Скобки для операции аппликации восстанавливаются по ассоциации влево, например:

XY = (XY), XYZ = ((XY)Z),...

2. Избыточные скобки могут опускаться, например:

(XY) = XY, ((XY)Z) = XYZ,...

6.2.4. Синтаксис выражений комбинаторной логики

Определение 6.2. Под синтаксисом понимают раздел описания формального математического языка или языка программирования, исследующий вид, форму и структуру конструкций, без учета их значения (или, иначе, семантики) или практической применимости (или, иначе, прагматики).

Задать синтаксис языка возможно, перечислив описание его конструкций с использованием метаязыка, например, с помощью форм Бэкуса-Наура или БНФ. БНФ созданы в 60-х годах Дж. Бэкусом (John Backus) и развиты П. Науром (Peter Naur) как метаязык для формализации синтаксиса языка программирования ALGOL 60. Впоследствии БНФ получили широкое распространение и в настоящее время являются основной нотацией для формализации синтаксиса языков программирования (мы будем пользоваться БНФ для формализации синтаксиса языка программирования SML).

В нотации БНФ символ "::=" интерпретируется словами "может иметь вид", а символ "|" - словом "или". Определяемое понятие записывается слева от значка "::=", а определяющие понятия записываются в угловых скобках справа от значка "::=".

Формализуем синтаксис выражений комбинаторной логики (или комбинаторов).

БНФ -описание комбинатора имеет вид:

<комбинатор>::= K | S | (<комбинатор> <комбинатор>)

БНФ -описание терма комбинаторной логики, возможно, содержащего переменные, имеет вид:

<комбинаторный терм>::= K | S | <переменная> |

(<комбинаторный терм> <комбинаторный терм>)

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

(I) I a = a комбинатор тождества
(K) К ab = a комбинатор первой проекции (иначе именуемый канцелятором, т.е. "отменяющим" "выполнение" всех "инструкций", кроме первой)
(S) S abc = ac(bc) комбинатор - коннектор - определяет порядок "связывания" "инструкций" программы таким образом, что третья "инструкция" "распределяется" по паре из двух первых
(B) B abc = a(bc) комбинатор композиции - образует последовательность комбинаторных термов и служит для объединения более элементарных "инструкций" в более сложные, а в итоге - в "программы"
(C) C abc = acb пермутация (перестановка)
(W) W xy = xyy дублирование аргументов

 

6.2.5. Редукция комбинаторных термов

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

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

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

Пример моделирования механизма редукции следующим

Рассмотрим комбинаторный терм вида

SKKx.

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

SKKx = (по правилу S) Kx(Kx) = (по правилу K) x.

В результате получаем, что SKKx = x, откуда, с учетом аксиом и правила (I), I = SKK.

Как видно из предыдущего примера, одни комбинаторы можно выразить через другие.

 




Поделиться с друзьями:


Дата добавления: 2014-01-07; Просмотров: 313; Нарушение авторских прав?; Мы поможем в написании вашей работы!


Нам важно ваше мнение! Был ли полезен опубликованный материал? Да | Нет



studopedia.su - Студопедия (2013 - 2024) год. Все материалы представленные на сайте исключительно с целью ознакомления читателями и не преследуют коммерческих целей или нарушение авторских прав! Последнее добавление




Генерация страницы за: 0.011 сек.