Рерайтинг (математика)

Матеріал з Вікіпедії — вільної енциклопедії.
Перейти до: навігація, пошук

У математиці, комп'ютерній науці та в логіці термін рерайтинг означає широкий діапазон способів (потенційно не детермінованих) заміни елементів формули таким чином, що зміст не міняється.

У самому базовому вигляді системи рерайтинга складаються з набору об'єктів, плюс відносин про те, як перетворити ці об'єкти.

Рерайтинг може бути не детермінованим. Одне правило рерайтинга терму може застосовуватися багатьма різними способами до цього терму, або може бути застосовано більше одного правила. Тоді системи рерайтинга не забезпечують алгоритм зміни одного терміна на інший, але забезпечують набір можливих правил програми. Проте у поєднанні з відповідним алгоритмом системи рерайтинга можуть розглядатися як комп'ютерні програми, на рерайтингу термів засновано декілька систем доведення теорем[1] та декларативних мов програмування.[2][3]

Інтуїтивні приклади[ред.ред. код]

Логіка[ред.ред. код]

У логіці, процедура одержання формули кон'юнктивної нормальної форми (КНФ) може бути зручно написана за допомогою системи рерайтинга.[4] Правила такої системи будуть:

(Подвійне заперечення)
(Закон де Моргана)
(Дістрибутивність)
,

де символ () вказує на те, що зміст лівої частини може бути поданий як рерайтинг у правій частині.

Лінгвістика[ред.ред. код]

У лінгвістиці правила рерайтинга, які також називаються правилами фразової структури, використовуються в деяких системах генеративної граматики, як засіб генерування граматично правильних речень мови. Таке правило зазвичай приймає форму A → X, де A є міткою синтаксичної категорії, наприклад, іменником або реченням, а X є послідовністю таких міток або морфем, що виражає той факт, що A може бути замінений на X при генеруванні складової структури речення. Наприклад, правило S → NP VP означає, що пропозиція може складатися з іменника, що супроводжується дієсловом; подальші правила вказують, з яких субкомпонентів можуть складатися іменник та дієслово, і так далі.

Типи систем рерайтинга[ред.ред. код]

Абстрактні системи рерайтинга[ред.ред. код]

З наведених вище прикладів зрозуміло, що ми можемо думати про переписування систем абстрактно. Потрібно вказати набір об'єктів та правила, які можуть бути застосовані для їх перетворення. Найбільш загальна (однозначна) установка цього поняття називається абстрактною системою скорочення (англ. ARS), хоча останнім часом автори використовують абстрактну систему рерайтинга.[5]

ARS — це просто набір A, елементи якого називаються об'єктами та разом з бінарним відношенням на A, традиційно позначаються →, і називаються відношенням зменшення, відношенням рерайтинга[6] або просто зменшення.[7]

Приклад. Припустимо, що набір об'єктів T = {a, b, c} і бінарне співвідношення задано правилами a → b, b → a, a → c, і b → c. Зауважте, що ці правила можуть бути застосовані як до a, так і до b, щоб отримати термін c. Така властивість явно важлива. Зауважте також, що c є, в певному сенсі, «найпростішим» терміном у системі, оскільки нічого не може бути застосовано до c, щоб перетворити його далі. Цей приклад веде нас до визначення деяких важливих понять у загальному налаштуванні ARS.[8]

Рядкові системи рерайтинга[ред.ред. код]

Рядкова система рерайтинга (англ. SRS), також відома як система semi-Thue, використовує вільну моноїдну структуру рядків (слів) над алфавітом, щоб розширити відношення рерайтинга  для всіх рядків у алфавіті, що містять ліву і відповідно праву сторону деяких правил як підрядка. Формально semi-Thue системи це пара , де  — (найчастіше кінцевий) алфавіт, а це бінарне відношення між деякими (фіксованими) строками в алфавіті, що називаються правилами рерайтинга. Однокрокове відношення рерайтинга відносини викликаної  на  визначається так: для будь-яких строк  якщо і тільки якщо є такі, що , , і . Так як  є відношенням на , пара  підходить до визначення абстрактної системи рерайтинга. Очевидно, що  є підмножиною з . Якщо відношення  є симетричним, тоді система називається системою Thue.

У SRS, відношення скорочення сумісне з моноїдною операцією, що означає, що з витікає для усіх рядків . Аналогічним чином, рефлексивне транзитивне симетричне замикання , позначене , є конгруентність, тобто вона є відношенням еквівалентності (за визначенням), і також сумісна з конкатенацією рядків. Відношення називається конгруентністю Thue що породжується з . У системі Thue, тобто якщо iє симетричним, переписане відношення збігається з конгруентністю Thue .

Поняття системи semi-Thue по суті збігається з представленням моноїда.Так як це конгруентність, ми можемо визначити фактор моноїд вільного моноїда за допомогою конгруентністі Thue звичайним чином. Якщо моноїд ізоморфний з , то система semi-Thue називається моноїдним представленням .

Ми відразу отримуємо деякі дуже корисні зв'язки з іншими областями алгебри. Наприклад, алфавіт {a, b} з правилами { ab → ε, ba → ε }, де ε це порожній рядок, є представленням вільної групи на одному генераторі. Якщо замість цих правил є лише { ab → ε }, то ми отримуємо уявлення про біциклічний моноїд. Таким чином, системи Thue є природною основою для вирішення проблеми слів для моноїдів та груп. По суті, кожен моноїд має представлення форми , тобто він завжди може бути представлен системою semi-Thue, можливо, над нескінченним алфавітом.

Проблема слів для системи semi-Thue в цілому нерозв'язна; цей результат іноді називають теоремою Пост-Маркова.[9]

Системи рерайтинга термінів[ред.ред. код]

Система рерайтинга термінів (TRS) - це система рерайтинга, де об'єктами є терміни або вирази з вкладеними підвиразами. Наприклад, система, показана у розділі Логіка вище, є системою рерайтинга термінів. Умови в цій системі складаються з бінарних операторів і і універсального оператора . Також у правилах є змінні, кожна з яких представляє будь-який можливий термін (хоча одна змінна завжди представляє один і той же термін в одному правилі).

На відміну від рядкової системи рерайтинга, об'єктами якої є плоскі послідовності символів, об'єкти, на яких працює система переписування, тобто терміни, утворюють термінову алгебру. Термін можна візуалізувати як дерево символів, набір прийнятих символів фіксується даним підписом.

Примітки[ред.ред. код]

  1. Hsiang, Jieh, et al. "The term rewriting approach to automated theorem proving." The Journal of Logic Programming 14.1-2 (1992): 71-99.
  2. Frühwirth, Thom. "Theory and practice of constraint handling rules." The Journal of Logic Programming 37.1 (1998): 95-138.
  3. Clavel, Manuel, et al. "Maude: Specification and programming in rewriting logic." Theoretical Computer Science 285.2 (2002): 187-243.
  4. Kim Marriott; Peter J. Stuckey (1998). Programming with Constraints: An Introduction. MIT Press. с. 436–. ISBN 978-0-262-13341-8. 
  5. Bezem et al., p. 7,
  6. Bezem et al., p. 7,
  7. Book and Otto, p. 10
  8. Baader and Nipkow, pp. 8-9
  9. Martin Davis et al. 1994, p. 178
Сигма Це незавершена стаття з математики.
Ви можете допомогти проекту, виправивши або дописавши її.