Упорядочение путей (переписывание терминов)
В теоретической информатике , в частности в переписывании терминов , порядок путей — это хорошо обоснованный строгий общий порядок (>) на множестве всех терминов такой, что
- f (...) > g ( s 1 ,..., s n ), если f . > g и f (...) > s i для i =1,..., n ,
где ( . >) — заданный пользователем общий порядок приоритета в наборе всех функциональных символов .
Интуитивно понятно, что терм f (...) больше, чем любой терм g (...), построенный из термов s i меньших, чем f (...), с использованиемкорневой символ с более низким приоритетом g .В частности, по структурной индукции терм f (...) больше, чем любой терм, содержащий только символы, меньшие, чем f .
Упорядочение путей часто используется в качестве редукционного порядка при переписывании терминов, в частности, в алгоритме завершения Кнута-Бендикса .Например, система переписывания терминов для « умножения » математических выражений может содержать правило x *( y + z ) → ( x * y ) + ( x * z ). Чтобы доказать завершение , необходимо найти порядок приведения (>), относительно которого терм x *( y + z ) больше, чем терм ( x * y )+( x * z ). Это нетривиально, поскольку первый термин содержит меньше функциональных символов и меньше переменных, чем второй. Однако установка приоритета (*) . > (+) можно использовать упорядочение путей, поскольку как x *( y + z ) > x * y , так и x *( y + z ) > x * z легко достичь .
Также могут существовать системы для некоторых общерекурсивных функций , например система для функции Аккермана может содержать правило A( a + , б + ) → А( а , А( а + , б )), [1] где б + обозначает преемника b .
Учитывая два термина s и t с корневым символом f и g соответственно, для определения их отношения сначала сравниваются их корневые символы.
- Если f < . g , то s может доминировать над t только в том случае, если это делает один из подтермов s .
- Если ж . > g , то s доминирует над t, если s доминирует над каждым из подтермов t .
- Если f = g непосредственные подчлены s t и , то необходимо сравнивать рекурсивно. В зависимости от конкретного метода существуют различные варианты упорядочения путей. [2] [3]
Последние варианты включают в себя:
- упорядочение мультимножеств путей ( mpo ), первоначально называемое рекурсивным упорядочением путей ( rpo ) [4]
- путей порядок лексикографических ( lpo ) [5]
- комбинация mpo и lpo, названная рекурсивным упорядочением путей. Дершовицем, Жуанно (1990) [6] [7] [8]
Дершовиц, Окада (1988) перечисляют дополнительные варианты и соотносят их с Аккермана системой порядковых обозначений . В частности, верхняя граница, заданная для типов порядка рекурсивных упорядочений путей с n функциональными символами, равна φ( n ,0) с использованием функции Веблена для больших счетных ординалов. [7]
Формальные определения
[ редактировать ]( Порядок путей мультимножества >) можно определить следующим образом: [9]
| s знак равно ж ( s 1 ,..., s м ) > т знак равно грамм ( т 1 ,..., т п ) | если | ||||||||
| ж | . > | г | и | с | > | т дж | для каждого | j ∈ {1,..., n }, | или |
| и я | ≥ | т | для некоторых | i ∈ {1,..., m }, | или | ||||
| ж | = | г | и | { s 1 ,..., s m } >> { t 1 ,..., t n } | |||||
где
- (≥) обозначает рефлексивное замыкание МПО (>),
- { s 1 ,..., s m } обозначает мультимножество подтермов s , аналогичное для t , и
- (>>) обозначает расширение мультимножества (>), определяемое формулой { s 1 ,..., s m } >> { t 1 ,..., t n }, если { t 1 ,..., t n } можно получить из { s 1 ,..., s m }
- удалив хотя бы один элемент, или
- путем замены элемента мультимножеством строго меньших (по отношению к mpo) элементов. [10]
В более общем смысле, порядка функционал — это функция O, отображающая один порядок в другой и удовлетворяющая следующим свойствам: [11]
- Если (>) транзитивно , то транзитивно и O (>).
- Если (>) иррефлексивно , то иррефлексивно и O (>).
- Если s > t , то f (..., s ,...) O (>) f (..., t ,...).
- O непрерывен R в отношениях, т. е. если 0 , R 1 , R 2 , R 3 , ... является бесконечной последовательностью отношений, то O (∪ ∞
я знак равно 0 р я ) знак равно ∪ ∞
я знак равно 0 О ( р я ).
Расширение мультимножества, отображающее (>) выше на (>>) выше, является одним из примеров функционала порядка: (>>)= O (>).Другой функционал порядка — это лексикографическое расширение, приводящее к упорядочиванию лексикографического пути .
Ссылки
[ редактировать ]- ^ Н. Дершовиц, « Прекращение » (1995). п. 207
- ^ Нахум Дершовиц , Жан-Пьер Жуанно (1990). Ян ван Леувен (ред.). Переписать системы . Справочник по теоретической информатике. Том. Б. Эльзевир. стр. 243–320. Здесь: разд.5.3, стр.275
- ^ Жерар Юэ (май 1986 г.). Формальные структуры для вычислений и дедукции . Международная летняя школа по логике программирования и расчетам дискретного проектирования. Архивировано из оригинала 14 июля 2014 г. Здесь: глава 4, стр.55-64.
- ^ Н. Дершовиц (1982). «Заказы на системы переписывания терминов» (PDF) . Теория. Вычислить. Наука . 17 (3): 279–301. дои : 10.1016/0304-3975(82)90026-3 . S2CID 6070052 .
- ^ С. Камин, Ж.-Ж. Леви (1980). Два обобщения рекурсивного упорядочения путей (технический отчет). унив. Иллинойс, Урбана/Иллинойс.
- ^ Kamin, Levy (1980)
- ^ Перейти обратно: а б Н. Дершовиц, М. Окада (1988). «Теоретико-доказательные методы теории переписывания терминов». Учеб. 3-й симпозиум IEEE. по логике в информатике (PDF) . стр. 104–111.
- ^ Мицухиро Окада, Адам Стил (1988). «Структуры упорядочения и алгоритм завершения Кнута – Бендикса». Учеб. Аллертонской конференции. по связи, управлению и вычислениям .
- ^ Huet (1986), разд.4.3, определение 1, стр.57
- ^ Huet (1986), раздел 4.1.3, стр.56
- ^ Huet (1986), раздел 4.3, с. 58