Ортогональность (переписывание термина)

Ортогональность как свойство систем переписывания терминов (TRS) описывает, когда все правила сокращения системы являются леволинейными, то есть каждая переменная встречается только один раз в левой части каждого правила сокращения, и нет перекрытия между ними . т.е. TRS не имеет критических пар . Например $D(x,x)\to E$ не является леволинейным. ^[1]

Ортогональные TRS обладают следующим свойством: все приводимые выражения (редексы) внутри термина полностью не пересекаются, то есть редексы не имеют общего функционального символа.

Например, ИВВ с правилами сокращения ${\begin{array}{lrcl}\rho _{1}:\ &f(x,y)&\rightarrow &g(y)\\\rho _{2}:\ &h(y)&\rightarrow &f(g(y),y)\end{array}}$ ортогональна — легко заметить, что каждое правило сокращения является леволинейным, а левая часть каждого правила сокращения не имеет общего функционального символа, поэтому перекрытия нет.

Ортогональные TRS сливаются .

Слабая ортогональность

TRS является слабо ортогональной, если она леволинейна и содержит только тривиальные критические пары, т. е. если $(t,s)$ тогда это критическая пара $t=s$ . ^[1] Слабо ортогональные TRS конфлюэнтны. ^[2]

TRS является почти ортогональным, если он слабо ортогонален и имеет дополнительное свойство, заключающееся в том, что перекрытие между вхождениями редексов происходит только в корне вхождений редексов. ^[3]

Ссылки

^ Перейти обратно: ^а ^б Клоп, Дж.В. «Системы переписывания терминов» (PDF) . Статьи Нахума Дершовица и его студентов . Тель-Авивский университет. п. 69 . Проверено 14 августа 2021 г.
^ Тереза (20 марта 2003 г.). Системы переписывания терминов . Издательство Кембриджского университета. п. 140. ИСБН 978-0-521-39115-3 .
^ Раамсдонк, Фемке ван (2 апреля 1997 г.). «Самое честное переписывание». Материалы Третьей Международной конференции по типизированным лямбда-исчислениям и их приложениям . Спрингер-Верлаг: 284–299. CiteSeerX 10.1.1.36.8258 .

Эта по информатике статья незавершена . Вы можете помочь Википедии, расширив ее .

\Gamma \!\vdash

Эта теории языков программирования или теории типов, статья, посвященная незавершена . Вы можете помочь Википедии, расширив ее .

[Klop-1] Перейти обратно: ^а ^б Клоп, Дж.В. «Системы переписывания терминов» (PDF) . Статьи Нахума Дершовица и его студентов . Тель-Авивский университет. п. 69 . Проверено 14 августа 2021 г.

[2] Тереза (20 марта 2003 г.). Системы переписывания терминов . Издательство Кембриджского университета. п. 140. ИСБН 978-0-521-39115-3 .

[3] Раамсдонк, Фемке ван (2 апреля 1997 г.). «Самое честное переписывание». Материалы Третьей Международной конференции по типизированным лямбда-исчислениям и их приложениям . Спрингер-Верлаг: 284–299. CiteSeerX 10.1.1.36.8258 .

[1]

[2]

[3]