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

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

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

Примеры

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

${displaystyle ho _ {1}: f (g (x), y) ightarrow y}$

${displaystyle ho _ {2}: g (x) ightarrow f (x, x)}$

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

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

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

${displaystyle ho _ {1}: g (g (x)) ightarrow x}$

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

Рекомендации

Этот математическая логика-связанная статья является заглушка. Вы можете помочь Википедии расширяя это. v т е