Компасқа тапсырыс беру - Encompassment ordering

Екі мүшенің үшбұрышы с ≤ т қоршауға алдын ала тапсырыс беруге байланысты.

Жылы теориялық информатика, атап айтқанда автоматтандырылған теорема және мерзімді қайта жазу, ұстау,[1] немесе қоршау, алдын ала берілетін тапсырыс (≤) жиынтығында шарттар, арқылы анықталады[2]

с ≤ т егер а субтерма туралы т Бұл ауыстыру данасы туралы с.

Ол қолданылады, мысалы. ішінде Knuth – Bendix аяқтау алгоритмі.

Қасиеттері

Ескертулер

  1. ^ екеуінен бастап f(х) ≤ f(ж) және f(ж) ≤ f(х) үшін айнымалы белгілер х, ж және а функция белгісі f
  2. ^ екеуінен де а ≤ б не б ≤ а нақты үшін тұрақты белгілер а, б
  3. ^ яғни рефлексивті емес, өтпелі және негізделген екілік қатынас R осындай sRt білдіреді сен[сσ ]б R сен[тσ]б барлық шарттар үшін с, т, сен, әр жол б туралы сенжәне әрқайсысы ауыстыру  σ

Әдебиеттер тізімі

  1. ^ Жерар Хуэт (1981). «Кнуттың дұрыстығының толық дәлелі - Бендикс аяқталу алгоритмі». Дж. Компут. Сист. Ғылыми. 23 (1): 11–21. дои:10.1016/0022-0000(81)90002-7.
  2. ^ Н.Дершовиц, Дж. Джуанно (1990). Ян ван Ливен (ред.). Қайта жазу жүйелері. Теориялық информатиканың анықтамалығы. B. Elsevier. 243–320 бб. Мұнда: секция.2.1, б. 250
  3. ^ Дершовиц, Джуанно (1990), тариқат.5.4, б. 278; біршама салақ, R сол жерде «аяқталатын қайта жазу қатынасы» болуы керек.