Кіріспе
Компьютерлік ғылымда конфлюенция – қайта жазу жүйелерінің қасиеті, мұндағы терминдерді бірнеше түрлі жолмен қайта жазу арқылы бірдей нәтиже алу мүмкіндігін сипаттайды. Бұл мақалада абстрактілі қайта жазу жүйесінің ең абстрактілі деңгейіндегі қасиеттері қарастырылады.
Жалпы жағдай және теория
Қайта жазу жүйесі бағытталған граф ретінде бейнеленеді, онда түйіндер өрнектерді, ал қабырғалар қайта жазуларды көрсетеді. Мысалы, егер a өрнегі b-ға қайта жазылса, онда b, a-ның қысқартылуы (редукциясы) деп айтылады (әлтернативті түрде, a, b-ға дейін қысқартылады немесе a, b-ның кеңейтілген түрі). Бұл жебе белгісімен көрсетіледі; a → b, a-ның b-ға дейін қысқаруын білдіреді. Интуитивті тұрғыдан алғанда, бұл сәйкес графтың a-дан b-ға бағытталған қабырғасы бар екенін көрсетеді. Егер графтың екі түйіні c мен d арасында жол болса, онда ол қысқарту тізбегін құрайды. Мысалы, егер c → c′ → c′′ → → d′ → d болса, онда c d деп жазуға болады, бұл c-ден d-ге дейінгі қысқарту тізбегінің бар екенін көрсетеді. Формальды түрде, →-ның рефлексивті транзитивті жабылуы болып табылады. Алдыңғы абзацтағы мысалды пайдалану арқылы, (11+9)×(2+4) → 20×(2+4) және 20×(2+4) → 20×6, сондықтан (11+9)×(2+4) 20×6. Бұл анықталғаннан кейін, конфлюенцияны келесідей анықтауға болады. a ∈ S, егер S жиынындағы барлық b, c жұптары үшін a b және a c болса, онда b d және c d болатын d ∈ S элементінің болуы керек ( деп белгіленеді). Егер S жиынындағы әрбір a конфлюентті болса, онда → конфлюентті деп айтылады. Бұл қасиет кейде оң жақта көрсетілген диаграмманың пішініне байланысты алмаздық қасиет деп те аталады. Кейбір авторлар алмаздық қасиет терминін диаграмманың әр жерде бір редукциялы түріне сақтап алады; яғни, егер a → b және a → c болса, онда b → d және c → d болатын d болуы керек. Бір редукциялы түр, көп редукциялы түрге қарағанда қатаң түрде күшті.
Жер бетіндегі құйылу
Терминді қайта жазу жүйесі, егер барлық айнымалысы жоқ термин конфуэнтті болса, негізгі конфуэнтті болып саналады.
Жергілікті жиналыс
[[File:Жергілікті түрде циклдік емес, бірақ жаһандық түрде конфлюентті қайта жазу жүйесі емес. gif|thumb|Сурет 4: Шеңберлі емес, жергілікті түрде конфлюентті, бірақ жаһандық түрде конфлюентті емес қайта жазу жүйесі, сондықтан қасиеттің атауы осылай берілген. (Ламбда-есептеудің осы қасиетке ие екендігі Чирч-Россер теоремасы ретінде белгілі.) Чирч-Россер қасиетіне ие қайта жазу жүйесінде сөздік мәселе ортақ мұрагерді табуға дейін тоғытылуы мүмкін. Чирч-Россер жүйесінде объектінің ең көп дегенде бір нормальды түрі болады; яғни, егер ол бар болса, объектінің нормальды түрі бірегей болады, бірақ ол болмауы да мүмкін. Мысалы, Ламбда-есептеуде (λx. xx)((λx. xx) нормальды түрге ие емес, себебі β-редукциялардың шексіз тізбегі бар: (λx. xx)((λx. xx) → (λx. xx)((λx. xx) → ...
Қайта жазу жүйесі Чирч-Россер қасиетіне ие болу үшін міндетті түрде конфлюентті болу керек. Осы теңдестікке байланысты әдебиетте анықтамалардың әртүрлілігіне жиі кездесесіз. Мысалы, "Terese" кітабында Чирч-Россер қасиеті мен конфлюенция бірдей анықтама ретінде берілген, мұнда ұсынылған конфлюенция анықтамасына синоним ретінде қарастырылады; мұнда анықталған Чирч-Россер қасиетіне есім берілмейді, бірақ эквивалентті қасиет ретінде ұсынылады; басқа мәтіндерден бұл айырмашылық қасақана жасалған.
Жартылай қосылу
Жергілікті конфуенцияның анықтамасы жаһандық конфуенциядан соңғысынан өзгеше, себебі тек бір қайта жазу қадамында берілген элементтен қол жеткізілген элементтер ғана ескеріледі. Бір қадамда қол жеткен бір элементті және кез келген тізбек арқылы қол жеткен басқа элементті қарастыра отырып, біз жартылай конфуенция деген аралық ұғымға жетеміз: a ∈ S жартылай конфуентті деп аталады, егер барлық b, c ∈ S үшін a → b және a ⇒ c болса, онда d ∈ S бар, сонда b ⇒ d және c ⇒ d болады; егер әрбір a ∈ S жартылай конфуентті болса, онда → жартылай конфуентті деп айтамыз. Жартылай конфуентті элементтің конфуентті болуы міндетті емес, бірақ жартылай конфуентті қайта жазу жүйесі қажетті түрде конфуентті, ал конфуентті жүйе тривиальды түрде жартылай конфуентті болады.
Қатты қосылу
Күшейтілген конфузия – бұл жергілікті конфузияның бір түрі, ол қайта жазу жүйесінің жаһандық конфузияға ие екенін қорытуға мүмкіндік береді. Егер кез келген b, c ∈ S үшін a → b және a → c болса, онда d ∈ S элементінің b → d және c → d немесе c = d болатыны айтылса, a ∈ S элементі күшті конфузиялық деп аталады; егер әрбір a ∈ S күшті конфузиялық болса, онда → күшті конфузиялық деп айтамыз. Конфузиялық элемент күшті конфузиялық болуы міндетті емес, бірақ күшті конфузиялық қайта жазу жүйесі міндетті түрде конфузиялық болады.
Құйылатын жүйелердің мысалдары
Идеал бойынша көпмүшелерді қысқарту, егер Грёбнер негізімен жұмыс істелсе, конfluent қайта жазу жүйесі болып табылады. Мацумото теоремасы өрім қатынастарының конfluentтігінен туындайды. λ-термдердің β-редукциясы Черч-Россер теоремасы бойынша конfluentті.