Перекрытие (переписывание терминов)

В математике , информатике и логике перекрытие пределах , как свойство правил сокращения в системе переписывания терминов , описывает ситуацию, когда ряд различных правил сокращения определяют потенциально противоречивые способы сокращения приводимого выражения, также известного как редекс, в срок .

Точнее, если несколько разных правил сокращения имеют общие функциональные символы в левой части, может произойти перекрытие. Часто мы не учитываем тривиальное перекрытие редекса и самого себя.

Примеры

Рассмотрим систему переписывания терминов, определенную следующими правилами сокращения:

$\rho _{1}\ :\ f(g(x),y)\rightarrow y$

$\rho _{2}\ :\ g(x)\rightarrow f(x,x)$

Термин $f(g(x),y)$ может быть уменьшено через ρ _1, чтобы получить y , но его также можно уменьшить через ρ _2, чтобы получить $f(f(x,x),y).$. Обратите внимание, как редекс $g(x)$ содержится в редексе $f(g(x),y)$. Результат сокращения различных редексов описывается в так называемой критической паре ; Критическая пара, возникающая в результате этой системы переписывания терминов, равна $(f(f(x,x),y),y)$.

Перекрытие может произойти при использовании менее двух правил сокращения.

Рассмотрим систему переписывания терминов, определенную следующим правилом сокращения:

$\rho _{1}\ :\ g(g(x))\rightarrow x$

Термин $g(g(g(x)))$ имеет перекрывающиеся редексы, которые можно применять либо к самому внутреннему вхождению, либо к самому внешнему вхождению $g(g(x))$ срок.