Историки об Елизавете Петровне: Елизавета попала между двумя встречными культурными течениями, воспитывалась среди новых европейских веяний и преданий...
Автоматическое растормаживание колес: Тормозные устройства колес предназначены для уменьшения длины пробега и улучшения маневрирования ВС при...
Топ:
Комплексной системы оценки состояния охраны труда на производственном объекте (КСОТ-П): Цели и задачи Комплексной системы оценки состояния охраны труда и определению факторов рисков по охране труда...
Особенности труда и отдыха в условиях низких температур: К работам при низких температурах на открытом воздухе и в не отапливаемых помещениях допускаются лица не моложе 18 лет, прошедшие...
Эволюция кровеносной системы позвоночных животных: Биологическая эволюция – необратимый процесс исторического развития живой природы...
Интересное:
Подходы к решению темы фильма: Существует три основных типа исторического фильма, имеющих между собой много общего...
Что нужно делать при лейкемии: Прежде всего, необходимо выяснить, не страдаете ли вы каким-либо душевным недугом...
Искусственное повышение поверхности территории: Варианты искусственного повышения поверхности территории необходимо выбирать на основе анализа следующих характеристик защищаемой территории...
Дисциплины:
2021-03-18 | 79 |
5.00
из
|
Заказать работу |
|
|
Декартово замкнутая категория подразумевает наличие:
1) аппликации арр,
2) каррирования (Λ),
3) точечной пары (х,у).
Так как есть пара, то есть и функции доступа к элементам:
Fst(x,y) = x
Snd(x,y) = y
ККЛ представляется следующей совокупностью комбинаторов:
App - аппликация,
Λ - абстрактор,
<, > - комбинационные пары,
(,) - совокупность,
○ - композиция.
Заявим, что 0 = Snd D=λr.rxy
N = Snd○Fstn ↑ комбинатор точечной пары.
(ass): (x○y)z = x(yz) – композиция
(fst): Fst(x,y) = x Fst = CIK
(snd): Snd(x,y) = y Snd = CI(KI)
(dpair): <x,y>z = (xz,yz)
Для вычисления композиции в среде предлагается ввести:
[(M,N)] ρ = <[M],[N]> ρ
(dΛ): Λ(x)yz = x(yz) - операция каррирования.
(app): App(x,y) = xy S = CIS
(quote): (’x)y = x λxy.x
(ac): App(Λ(x)y,z) = x(yz) # App(Λ(x)y,z) = Λ(x)yz = x(yz)#
Пример
Λ(x○Snd)yz = (x○Snd)(y,z) = xz
(’x)yz = xz
> quote = Λ(x○Snd) - правило quote является избыточным.
Пример. (из λ-исчисления в код Де Брейна).
(λх.х4((λх.х)3))+
(λ.0 4 ((λ. 0)3))+
S(Λ (S(S(0,’4),S(Λ (0),’3))),’+)
↑Snd ↑Snd
1 2 3 4 4 3 2 1
S(x,y) = App○<x,y>
0 заменяем на Snd и получаем выражение:
App○< Λ (App○< App○< Snd,’4>, App○< Λ(Snd),’3>>),’+>
На основе ККЛ можно построить абстрактную машину.
Общие свойства абстрактных машин.
Определение.
Абстрактная машина (АМ) - способ формализованного задания алгоритма для математически строго описываемых языков.
(АМ) - характеризуется множеством регистров, множеством состояний регистров и правилами перехода от состояния к состоянию.
|
два регистра памяти
быстрого доступа
Три стека
Правила перехода из состояния в состояние задаются кодом АМ.
Информация о состоянии регистров может быть представлена в некоторой структуре данных.
Структура [исходное состояние] => Структура [итоговое состояние]
<Новое состояние>=<Функция перехода>(старое состояние).
Функция, описывающая действие оператора кода АМ, имеет в качестве своих аргументов регистры этой машины с содержащимися в них данными, при этом переход машины из
одного состояния в другое соответствует шагу редукции дерева программы исходного языка.
Определение.
Верификация - способ проверки правильности программ на основе теоретических знаний.
Категориальная абстрактная машина (КАМ).
КАМ состоит из трех регистров: два стека (код и стек) и регистр терм.
Код Стек
Терм
И элементы стека, и элементы терма - символьные выражения, в них могут размещаться структуры символьных данных.
В начале программа в виде кода содержится в стеке ''кода'', ''стек'' пуст.
В конце «код» пуст, в “ терме ” содержится результат. Правила перехода из состояния в состояние определяются набором инструкций машины.
Определение.
Состоянием машины называется тройка <T,C,S>, где T -терм как структурированное значение, например граф; C - код; S - стек или дамп (вспомогательная память).
Закон функционирования КАМ изменяет старую тройку на новую: <T, C, S>→<T|,C|,S|>.
Входной язык КАМ: <,>;Fst; Snd; Λ; ’; (,); app
|
КАМ – это вариант КЛ, вовлекающий ДЗК, а также техническое устройство, вычисляющее значение выражений.
Средства КЛ имеют категориальный характер, т.е. в категориях используются композиции и тождества, в декартовых категориях дополнительно вводят произведение с использованием спаривания <, >, а также проекции Snd и Fst. Декартовы замкнутые категории дополнительно содержат каррирование Λ, апплицирование и средства экспонирования, т.е. средства построения функциональных правил.
Цикл работы КАМ
1) Выбор категориального терма, построенного из комбинаторов.
2) Означивание этого терма производится путем его аппликации к среде.
Начальное состояние | Конечное состояние | ||||
Терм | Код | Стек | Терм | Код | Стек |
(S,t) | car:C | A | S | C | А |
(S,t) | cdr:C | A | T | C | А |
S | (quoteB)C | A | B | C | А |
S | (cur C) C1 | A | [C:S] | C1 | А |
([C:S], t) | app. C1 | A | (S,t) | C:C1 | А |
T | cons C | S:A | (S,t) | C | А |
S | push.C | A | S | C | S:A |
T | swap.C | S:A | S | C | T:A |
А - вектор содержимого стека,
”:” - разделитель,
[C:S] - совокупность.
В языке ДЗК (декартово замкнутые категории) использовано 8 символов, которым ставятся в соответствие инструкции КАМ:
Сar = Fst - получает терм (s,t) и заменяет его на s.
Cdr = Snd - получает терм (s,t) и заменяет его на t.
Quote = ’ - получает терм s и оставляет его без изменений
Cur = Λ - замещает терм s на С:s, где C - код, инкапсулированный в Λ.
Cons = > - строит совокупность из вершины стека и терма, заменяет терм на эту
совокупность и проталкивает стек.
app = App - получает терм (C:s,t), замещает его на (s,t), а оставшейся части кода
устанавливает префикс C.
swap =, - меняет содержимое терма и вершины стека местами.
push = < - берет терм и помещает его в вершину стека.
Стек Код
А С Вместо рор используется пара из swap и cons.
App○<x,y> Term
App(<x,y>Term)
Код: push,[x],swap,[y],cons,app
Пример КАМ кода: сложение 2 и 3
((+2)3) –это аппликация (+ к 2) →(+2) к 3
push push quote + swap quote 2 cons app swap quote 3 cons app
<<’+,’2>App,’3>App
Оптимизация кода КАМ
Два вида оптимизации:
переход к многоместным операциям, т.е. вместо функции “+”, которая будет брать аргументы по очереди, рассмотрим двуместный “+”.
|
а) App○< App○<’+,x>,y> = +<x,y>
б) Воспользуемся категориальным равенством для β-редукции.
App○<Λ(х)○у, z> = x○<y,z>
{(λx.y)z→[z/x]y – соответствующее категориальное равенство.}
|
|
Своеобразие русской архитектуры: Основной материал – дерево – быстрота постройки, но недолговечность и необходимость деления...
Биохимия спиртового брожения: Основу технологии получения пива составляет спиртовое брожение, - при котором сахар превращается...
Состав сооружений: решетки и песколовки: Решетки – это первое устройство в схеме очистных сооружений. Они представляют...
Типы оградительных сооружений в морском порту: По расположению оградительных сооружений в плане различают волноломы, обе оконечности...
© cyberpedia.su 2017-2024 - Не является автором материалов. Исключительное право сохранено за автором текста.
Если вы не хотите, чтобы данный материал был у нас на сайте, перейдите по ссылке: Нарушение авторских прав. Мы поможем в написании вашей работы!