Par crítico (reescritura de términos)

Diagrama triangular de un par crítico obtenido a partir de dos reglas de reescritura s  →  t (fila superior, izquierda) y l → r (derecha). La sustitución σ unifica el subtérmino s | _p con l . El término superpuesto resultante s σ[ lσ ] _p (fila inferior, medio) puede reescribirse como el término tσ y s σ[ rσ' ] _p (filas inferior, izquierda y derecha), respectivamente. Los dos últimos términos forman el par crítico. Pueden reescribirse eventualmente como un término común, si el conjunto de reglas de reescritura es confluente . (Para detalles de notación, vea Término (lógica) § Operaciones con términos .)

Un par crítico surge en un sistema de reescritura de términos cuando dos reglas de reescritura se superponen para producir dos términos diferentes. En más detalle, ( t ₁ , t ₂ ) es un par crítico si hay un término t para el cual dos aplicaciones diferentes de una regla de reescritura (ya sea la misma regla aplicada de forma diferente o dos reglas diferentes) producen los términos t ₁ y t ₂ .

Definiciones

La definición real de un par crítico es un poco más compleja, ya que excluye los pares que se pueden obtener a partir de pares críticos por sustitución y orienta el par en función de la superposición. Específicamente, para un par de reglas superpuestas y , donde la superposición es que para algún contexto no vacío , y el término (que no es una variable) coincide bajo algunas sustituciones que son más generales, el par crítico es . ^[1] ${\displaystyle \rho _{0}:l_{0}\to r_{0}}$ ${\displaystyle \rho _{1}:l_{1}\to r_{1}}$ ${\displaystyle l_{0}=D[s]}$ ${\displaystyle D[\;]}$ ${\displaystyle s}$ ${\displaystyle l_{1}}$ ${\displaystyle s\sigma =l_{1}\tau }$ ${\displaystyle (D\sigma [r_{1}\tau ],r_{0}\sigma )}$

Cuando ambos lados del par crítico pueden reducirse al mismo término, el par crítico se denomina convergente . Cuando un lado del par crítico es idéntico al otro, el par crítico se denomina trivial .

Ejemplos

Por ejemplo, en el término sistema de reescritura con reglas

el único par crítico es ⟨ g ( x , z ), f ( x , z )⟩. Ambos términos pueden derivarse del término f ( g ( x , y ), z ) aplicando una única regla de reescritura.

Como otro ejemplo, considere el sistema de reescritura de términos con una regla única.

Aplicando esta regla de dos maneras diferentes al término f ( f ( x , x ), x ), vemos que ( f ( x , x ), f ( x , x )) es un par crítico (trivial).

Lema del par crítico

La confluencia implica claramente pares críticos convergentes: si surge cualquier par crítico ⟨ a , b ⟩, entonces a y b tienen un reduct común y, por lo tanto, el par crítico es convergente. Si el sistema de reescritura de términos no es confluente , el par crítico puede no converger, por lo que los pares críticos son fuentes potenciales donde la confluencia fallará.

El lema del par crítico establece que un sistema de reescritura de términos es débilmente confluente (es decir, localmente) si y solo si todos los pares críticos son convergentes. Por lo tanto, para averiguar si un sistema de reescritura de términos es débilmente confluente, basta con probar todos los pares críticos y ver si son convergentes. Esto permite averiguar algorítmicamente si un sistema de reescritura de términos es débilmente confluente o no, dado que se puede comprobar algorítmicamente si dos términos convergen.

Véase también

• Compleción de Knuth-Bendix , un algoritmo basado en pares críticos para calcular un sistema de reescritura de términos confluente y terminal equivalente a uno dado

Enlaces externos

• Weisstein, Eric W. "Par crítico". MathWorld .

Referencias

1. Terese (2003). Sistemas de reescritura de términos . Cambridge, Reino Unido: Cambridge University Press. p. 53. ISBN 0-521-39115-6.

• Franz Baader y Tobias Nipkow , Term Rewriting and All That , Cambridge University Press, 1998 (enlace web del libro)