Упорядочивание путей (переписывание терминов)
В теоретической информатике , в частности при переписывании терминов , упорядочение путей - это хорошо обоснованный строгий общий порядок (>) на множестве всех терминов, такой, что
- 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 * ( y + z )> x * y , и x * ( y + z )> x * z легко достичь.
Для двух членов s и t с корневым символом f и g , соответственно, чтобы определить их связь, сначала сравниваются их корневые символы.
- Если f < . г , то ев может доминировать т только тогда , когда один из S' подтермов S делает.
- Если f . > Г , то ей доминирует т , если ы доминирует над каждым из T» s подтермы.
- Если F = г , то непосредственные подтермы из й и т необходимости можно сравнить рекурсивно. В зависимости от конкретного метода существуют разные варианты упорядочения путей. [1] [2]
К последним вариантам относятся:
- упорядочение путей мультимножества ( mpo ), первоначально называвшееся рекурсивным упорядочением путей ( rpo ) [3]
- лексикографическое упорядочение путей (lpo ) [ 4 ]
- комбинация mpo и lpo, названная Dershowitz, Jouannaud (1990) [5] [6] [7] рекурсивным порядком путей .
Дершовиц, Окада (1988) перечисляют больше вариантов и соотносят их с системой порядковых чисел Аккермана .
Формальные определения
Порядок путей мультимножества (>) можно определить следующим образом: [8]
| s = f ( s 1 , ..., s m )> t = g ( t 1 , ..., t n ) | если | ||||||||
| ж | . > | г | и | s | > | t j | для каждого | j ∈ {1, ..., n }, | или |
| с я | ≥ | т | для некоторых | i ∈ {1, ..., m }, | или | ||||
| ж | знак равно | г | и | { s 1 , ..., s m } >> { t 1 , ..., t n } | |||||
где
- (≥) обозначает рефлексивное замыкание mpo (>),
- { s 1 , ..., s m } обозначает мультимножество подтермов s , аналогичных для t , и
- (>>) обозначает расширение мультимножества (>), определяемое как { s 1 , ..., s m } >> { t 1 , ..., t n } , если { t 1 , ..., t n } можно получить из { s 1 , ..., s m }
- удалив хотя бы один элемент, или
- путем замены элемента мультимножеством строго меньших (по сравнению с mpo) элементов. [9]
Более общо, порядок функционала является функция вывода отображения упорядочения к другому, и удовлетворяющему следующим свойствам: [10]
- Если (>) транзитивен , то O (>) тоже.
- Если (>) иррефлексивно , то O (>) - тоже .
- Если s > t , то f (..., s , ...) O (>) f (..., t , ...).
- О является непрерывной на отношения, то есть , если R 0 , R 1 , R 2 , R 3 , ... представляет собой бесконечную последовательность отношений, то O (∪∞
я = 0 R i ) = ∪∞
я = 0 О ( R i ).
Расширение мультимножества, отображение (>) выше на (>>) выше, является одним из примеров функционала порядка: (>>) = O (>). Другой функционал порядка - это лексикографическое расширение, ведущее к упорядочиванию лексикографических путей .
использованная литература
- ^ Nachum Дершоуиц , Жан Пирр Джоуаннод (1990). Ян ван Леувен (ред.). Системы перезаписи . Справочник по теоретической информатике. B . Эльзевир. С. 243–320. Здесь: раздел 5.3, с.275
- ^ Gerard Huet (май 1986). Формальные структуры для вычислений и дедукции . Международная летняя школа по логике программирования и исчислениям дискретного проектирования. Архивировано из оригинала на 2014-07-14. Здесь: глава 4, с.55-64
- ↑ Н. Дершовиц (1982). "Заказы для систем перезаписи терминов" (PDF) . Теорет. Comput. Sci . 17 (3): 279–301. DOI : 10.1016 / 0304-3975 (82) 90026-3 . S2CID 6070052 .
- ^ С. Камин, Ж.-Дж. Леви (1980). Два обобщения рекурсивного упорядочивания путей (Технический отчет). Univ. Иллинойс, Урбана / Иллинойс.
- ^ Камин, Леви (1980)
- ^ Н. Дершовиц, М. Окада (1988). "Теоретико-доказательные методы теории перезаписи терминов". Proc. 3-й симпозиум IEEE. по логике в компьютерных науках (PDF) . С. 104–111.
- ^ Мицухиро Окада, Адам Стил (1988). «Структуры упорядочения и алгоритм завершения Кнута – Бендикса». Proc. конференции Allerton Conf. по связи, управлению и вычислениям .
- ↑ Huet (1986), раздел 4.3, определение 1, стр.57
- ↑ Huet (1986), раздел 4.1.3, стр.56
- ↑ Huet (1986), раздел 4.3, стр. 58
- Системы перезаписи
- Теория порядка
