Confluence (абстрактный рерайтинг)
В информатике слияние — это свойство систем перезаписи , описывающее, какие термины в такой системе можно переписать более чем одним способом, чтобы получить один и тот же результат. В этой статье описываются свойства в наиболее абстрактной постановке абстрактной системы перезаписи .
Обычные правила элементарной арифметики образуют абстрактную систему перезаписи. Например, выражение (11 + 9) × (2 + 4) можно вычислять, начиная либо с левой, либо с правой скобки; однако в обоих случаях в конечном итоге получается один и тот же результат. Если каждое арифметическое выражение дает один и тот же результат независимо от стратегии редукции, говорят, что система арифметической перезаписи является конфлюэнтной. Системы арифметической перезаписи могут быть слитными или только слитными в зависимости от деталей системы перезаписи. [1]
Второй, более абстрактный пример получается из следующего доказательства того, что каждый групповой элемент равен обратному своему обратному: [2]
Это доказательство начинается с данных групповых аксиом A1-A3 и устанавливает пять предложений R4, R6, R10, R11 и R12, каждое из которых использует некоторые более ранние, а R12 является основной теоремой. Некоторые доказательства требуют неочевидных или даже творческих шагов, таких как применение аксиомы A2 в обратном порядке, тем самым переписывая «1» в « a −1 ⋅ a» на первом этапе доказательства R6. Одним из исторических мотивов разработки теории перезаписи терминов было стремление избежать необходимости в таких шагах, которые трудно найти неопытному человеку, не говоря уже о компьютерной программе.
Если система перезаписи терминов конфлюэнтна и завершается , существует простой метод доказательства равенства между двумя выражениями (также известными как термины ) s и t : начиная с s , применяйте равенства [примечание 1] слева направо до тех пор, пока это возможно, получение терма s′ . Получите из t терм t' аналогичным образом. Если оба термина s' и t' буквально совпадают, то s и t (что неудивительно) оказываются равными. Что еще более важно, если они не согласны, тоs и t не могут быть равны. То есть любые два члена s и t , которые вообще могут быть доказаны равными, могут быть сделаны этим методом.
Успех этого метода не зависит от определенного сложного порядка применения правил перезаписи, поскольку слияние гарантирует, что любая последовательность применения правил в конечном итоге приведет к одному и тому же результату (в то время как свойство завершения гарантирует, что любая последовательность в конечном итоге достигнет конца ). вообще). Следовательно, если для некоторой эквациональной теории может быть предоставлена конфлюэнтная и завершающая система переписывания терминов , [примечание 2] не требуется ни малейшего творческого подхода для выполнения доказательств равенства терминов; следовательно, эта задача становится доступной для компьютерных программ. Современные подходы обрабатывают более общие абстрактные системы перезаписи, а не термины.системы перезаписи; последние являются частным случаем первых.
