Реализация сетевой модели вычислений с аксиоматической и рекурсивной формами задания функций и предикатов (бакалаврская работа), страница 2

Правила вычисления схем направленных отношений1.4.1 Операция подстановки сети.Определение. Результат [S1 / e]S2 подстановки сети S1 в сеть S2′ ′′вместо элемента e ≡< R, q q > , такого, что его арность совпадает с арностью′ ′′сети S1 , есть [ I1O1 / q q ] < P1 ∪ P2 , I 2 , O2 , E1 ∪ E2 \ {e}, G1 ∪ G2 > .Выполнение операции подстановки в схематическом представлениисетей иллюстрируется на рисунке 1.4.1.Вычислениеосновываетсянадоказательстве общезначимости формул.методесетевойрезолюции–10Рис 1.4.2 Правила редукции сетей с функциональными и предикатнымисортами элементов.Используемый термин сетевая резолюция относится к процедуревывода общезначимости формул языка исчисления предикатов первогопорядка на базе сетевого представления схем направленных отношений.Основными отличиями сетевой резолюции от традиционного резолютивногологического вывода являются[2]:1) базирующаяся на сетевом представлении схемd -отношенийтехника проведения доказательства, в частности, выполнения техдействий, которые являются аналогом процедуры унификации;2) отказ при доказательстве от явного использования эрбрановскойинтерпретации и, вследствие этого, получение в ходе доказательства(возможно,неуспешного!)вкомпактнойсетевойформе11функциональных уравнений, решения которых представляют собоймодели рассматриваемой формулы при любых интерпретацияхпредикатных символов;3) использование прямого вывода истинности заданной формулы, а недоказательстватождественнойложностиинверсной,чтопотребовало применения не традиционной, а двойственной формыскулемизации;4) применениеспециальнойтехникидоказательстваформулравенством на базе сетевого представления схем d -отношений;1.5.

Схемы аксиом1. A • ( B • C ) = ( A • B ) • C .2. A<n′,n′′> •n′3.n′′= A.• A<n′,n′′> = A .4. A#(B #C) = ( A# B) #C .= A.5. A ##A= A .6.7. ( A′# B′) • ( A′′# B′′) = ( A′ • A′′) # ( B′ • B′′) .8.n′Bn′A• ( A <n′A ,n′A′ > # B < n′B ,n′B′ > ) •9.•=.10.•=.11.• (12. (##)•)== (n′A′n′B′•(#= B # A.#)•)..с1213. (#)•=14. (#)•(15.∩= 1 ∅1 .16..∪=1.#117. ( A ∩ A) = A.18. A < n′ ,n′′> ≤n′n ′′.19. A ∪ B = B ∪ A .20.

( A ∪ B) ∪ С = A ∪ (B ∪ C) .21. A ∪ A = A .22. n′ ∅ n • A < n ,n′′> = n′ ∅ n′′ .23. A < n′,n > • n ∅ n′′ = n′ ∅ n′′ .24. n′ ∅ n′′ ≤ A < n′,n′′> .25. A < n′A ,n′A′ > # n′ ∅ n′′ =n′A + n′26. n′ ∅ n′′ # A <n′A ,n′A′ > =∅ n′A′ + n′′ .n′A + n′∅ n′A′ + n′′ .27. ( A ∪ B) • C = A • C ∪ B • C .28. A • (B ∪ C) = A • B ∪ A • C .29. ( A ∪ B) #C = A#C ∪ B #C .30.

A# (B ∪ C) = A# B ∪ A#C .Правила вывода:П1.A ≤ B, B ≤ C.A≤CП2.A≤ B.E ≤ [ B / A] E)=•.13Здесь[B / A]E – результат замены в схеме E некоторого вхождениясхемы A на схему B .Истинность аксиом и непротиворечивость правил вывода поддаютсянепосредственной проверке[1].2. Различные представления схем направленных отношений2.1. Схематическое представлениеСхематическое представление является самым наглядным способомизображения направленных отношшений.Первое из рассматриваемых представлений, так называемое "лоскутное"( rag )представление(сокращенно,r -представление) связано сособенностями базисных операций последовательной и параллельнойкомпозиции d -отношений и, как нам кажется, поясняет выбор их названий.Вr -представлении адекватно отражаются как собственные свойства этихопераций (см. аксиомы 1,4),так и их связь между собой (аксиома 7) и сконстантами?(аксиомы 2,3,5,6).Рис 2.1 Пример схематического изображения сети140Определим два подмножества элементарных сетей – безэлементных S(не зависящее от выбора базиса B ) и одноэлементных S 1B ≅ {S1x | x ∈ B} .

Для0обозначения сетей из S используются те же символы, что и дляэлементарных комбинаторных d -отношений (констант); далее будеточевидна их связь и, следовательно, станет понятен сам выбор такихсимволов.Рис 2.2 Элементарные сетиРассмотрим простые схемы d -отношений, полученные (•, #) -композицией констант и переменных. r -Представление таких схем определиминдуктивно:1)элементарные схемы – константы и переменные – изображаютсяпрямоугольниками, внутри которых помещаются соответствующиесимволы – констант или переменных; для всех случаев, кромеnконстант,произвольныеr -представления элементарных схем имеютненулевые значения размеров представляющих ихпрямоугольников; для константn* длина, а при n = 0 и высотамогут быть равны нулю, более того, всякий раз, когда это возможно,будем выбирать для них именно нулевые размеры;2)если A ≡ A′ • A′′ и известны r -представления схем A′ и A ′′ свнешнимиграницамивформепрямоугольников,топутемсоответствующей трансформации (сжимания или растягивания) в15вертикальном направлении они приводятся к одинаковой, в общемслучаеA′ = A′′ ≡ненулевойвысотесоставляет(исключение), после чего правая границаслучайr -представленияA′совмещается с левой границей r -представления A ′′ (рис.

2.1a);еслиA ≡ A′# A′′ , то путем трансформации r -представлений A′ и A ′′ вгоризонтальном направлении они приводятся к одинаковой, в общемслучае, ненулевой (кроме случая A′ = A′′ ≡нижняя границаграницейпример(A •r -представленияr -представленияr• A#)•A′n) длине, после чегосовмещается с верхнейA ′′ (рис. 2.1b).На рис. 2.1c показан-представления•B#B•• (A #) , где A имеетарность < 1,1 > , а B – арность < 1, 2 > .Рис. 2.2.-Представление:а) последовательная композиция:b) параллельная композиция:c) пример r-представления.,,схемы16Соответствияэлементарныхконстантиихсхематическихпредставлений(Рис 2.3).Рис 2.3 Соответствие схематического представления констант и их алгебраическихи графических представленийПример схематического представления операции (рис 2.4) сложениянатуральных чисел.Натуральное число – число, порожденное конструктором типанатуральных чисел.<0,1> Null– Конструктор нуля.<1,1> Succ – Конструктор перехода к следующему числу<2,1> Add – Сложение двух чисел.Рис 2.4 Пример схематического представления сети172.2.

Алгебраическое представлениеЕще один тип представления. Смысл заключается в построенииалгебраического представления, эквивалентного схематическому. Вся сетьделится на прямоугольные области, затем каждая область заменяется своималгебраиеским представлением. Алгебраическое представления областей,находящихсяна одной вертикали объединяются символом параллельнойкомпозиции, А на одной горизонтали – последовательной(рис 2.5).Рис 2.5 Визуализация композиций схем НО18Пример.Для приведенных выше примеров соответствующие алнгебраическиепредставления будут такими3 41 = 3677 ∙ 86993 42 = 3677 ∙ 8699 ∙ 8699Рис 2.6 Пример представления функции в алгебраическом представлении2.3. Графическое представление.Графическое представление содержит в себе информацию о входах ивыходах сети, а также о зависимостях от других сетей.Идея построения заключается в присваивании имен точкам сети, ипостроении зависимостей между этими точками через другие функции.19Пример:Add = {a,c:e? b = Succ(a), e = Succ(d), d = Add(b,c)}ИлиAdd = {a,c: Succ(Add(Succ(a), c))}Все 3 представления направленных отношений эквивалентны3.

Реализация программыЦель программы – производить вычисление схем направленныхотношений основываясь на принципе сетевой резолюции.Входные данные берутся из файла с определениями функций в однойиз форм (алгебраической или графической). Затем составляется списокфункций во внутреннем представлении программы.По запросу пользователя происходит процесс подстановки однойфункции в другую. Тем самым порождая новые определения второйфункции.Программа реализована на языке C# в среде Visual Studio 2010.Программа состоит из 2х логических частей:1.

Построение по входному файлу списка лексем.2. Построение внутреннего представления функций.Разбор файла происходит согласно заданной грамматике. Сначалаопределяется сама правосторонняя грамматика, по ней строится графпереходов и начальное состояние. Затем входной файл построчноразбирается, согласно заданной грамматике.20Описание грамматики находится в приложении.3.1. Построение графа переходов для грамматикиАлгоритм построения графа переходов достаточно прост. Каждаявершина графа содержит указатель на ребро, которое из нее выходит.

Ребрабывают взвешенные строкой или эпсилон-ребра.Помимо указателя на ребро вершина содержит указатель на другойнетерминал. Если указатель на ребро отсутствует, то вершина конечная дляопределения нетерминала.class TVertex { //вершина графаinternal TEdge edges = null; //Исходящие дугиinternal NTerm nterm = null;//Указатель на определяющийнетерминал}class TEdge {internalinternalnext}}//эпсилон дугаTVertex next; //Указатель на следуующую вершинуTEdge(TVertex vertex) {= vertex;class TWEdge:TEdge { //Взвешенная дугаpublic string c;public TWEdge(string c, TVertex vertex): base(vertex) {this.c = c;}}Разбираяпострочнофайлсграмматикой,строитсясписокнетерминальных вершин графа.После разбора все нетерминальные символы отображаются в вершины,а терминальные – во взвешенные ребра.Процесс разбора файла с кодом программы на реализованном языкесводится к проверке порождения заданной грамматикой каждой строки.Процесс разбора заключается в последовательном уменьшении входнойстроки, при переходе к каждой следующей вершине.21static List<Result> Rec(TVertex v, string str) {List<Result> bk = new List<Result>();if(v.nterm != null) {foreach(TVertex def in v.nterm.def)bk = bk.Concat(Rec(def, str)).ToList();if(bk.Count == 0) {return new List<Result>();} else...}} else {bk.Add(new Result(str, new List<Pair>()));}if(v.edges == null) {return bk;} else {List<Result> result = new List<Result>();TWEdge w = v.edges as TWEdge;if(w == null) {foreach (Result res in bk){List<Result> restmp = Rec(v.edges.next,res.s);foreach (Result rr in restmp)rr.lst=res.lst.Concat(rr.lst).ToList();result = result.Concat(restmp).ToList();}} else {foreach(Result res in bk) {if(res.s.Length >= w.c.Length)if(res.s.Substring(0, w.c.Length) == w.c) {...}}}return result;}}Если нетерминал на определенном этапе зависит от другогонетерминала (v.Nterm), делается проверка оставшейся части строки дляv.Nterm.