Reescribiendo s en t mediante una regla l ::= r . Si l y r están relacionados mediante una relación de reescritura , también lo están s y t . Un ordenamiento de simplificación siempre relaciona l y s , y de manera similar r y t .
En la informática teórica , en particular en el razonamiento automático sobre ecuaciones formales, se utilizan ordenamientos de reducción para evitar bucles infinitos . Los órdenes de reescritura y, a su vez, las relaciones de reescritura son generalizaciones de este concepto que han resultado útiles en las investigaciones teóricas.
Motivación
Intuitivamente, un orden de reducción R relaciona dos términos s y t si t es propiamente "más simple" que s en algún sentido.
Por ejemplo, la simplificación de términos puede ser parte de un programa de álgebra computacional y puede estar usando el conjunto de reglas { x + 0 → x , 0+ x → x , x * 0 → 0, 0* x → 0, x * 1 → x , 1* x → x }. Para demostrar la imposibilidad de bucles infinitos al simplificar un término usando estas reglas, se puede usar el orden de reducción definido por " sRt si el término t es apropiadamente más corto que el término s "; aplicar cualquier regla del conjunto siempre acortará apropiadamente el término.
Por el contrario, para establecer la terminación de la "distribución" utilizando la regla x * ( y + z ) → x * y + x * z , será necesario un orden de reducción más elaborado, ya que esta regla puede hacer que el tamaño del término se dispare debido a la duplicación de x . La teoría de los órdenes de reescritura apunta a ayudar a proporcionar un orden apropiado en tales casos.
Definiciones formales
Formalmente, una relación binaria (→) sobre el conjunto de términos se denomina relación de reescritura si está cerrada bajo incrustación contextual y bajo instanciación ; formalmente: si l → r implica u [ l σ ] p → u [ r σ] p para todos los términos l , r , u , cada camino p de u , y cada sustitución σ. Si (→) es también irreflexiva y transitiva , entonces se denomina orden de reescritura , [1] o preorden de reescritura . Si este último (→) está además bien fundado , se denomina orden de reducción , [2] o preorden de reducción . Dada una relación binaria R , su cierre de reescritura es la relación de reescritura más pequeña que contiene a R . [3] Una relación de reescritura transitiva y reflexiva que contiene el orden de subtérmino se denomina orden de simplificación . [4]
Propiedades
El cierre inverso , el cierre simétrico , el cierre reflexivo y el cierre transitivo de una relación de reescritura es nuevamente una relación de reescritura, al igual que la unión y la intersección de dos relaciones de reescritura. [1]
El reverso de una orden de reescritura es nuevamente una orden de reescritura.
Si bien existen órdenes de reescritura que son totales en el conjunto de términos fundamentales ("total fundamental" para abreviar), ninguna orden de reescritura puede ser total en el conjunto de todos los términos . [nota 3] [5]
Por el contrario, para cada sistema de reescritura de términos terminales, el cierre transitivo de (::=) es un ordenamiento de reducción, [2] que, sin embargo, no necesita ser extensible a uno total-fundamental. Por ejemplo, el sistema de reescritura de términos terminales { f ( a )::= f ( b ), g ( b )::= g ( a ) } es terminal, pero puede demostrarse que lo es utilizando un ordenamiento de reducción solo si las constantes a y b son incomparables. [nota 5] [6]
Un orden de reescritura total y bien fundado [nota 6] necesariamente contiene la relación de subtérmino adecuada en los términos fundamentales. [nota 7]
Por el contrario, un ordenamiento de reescritura que contiene la relación de subtérmino [nota 8] está necesariamente bien fundado, cuando el conjunto de símbolos de función es finito. [5] [nota 9]
Un sistema de reescritura de términos finitos { l 1 ::= r 1 ,..., l n ::= r n , ...} es terminante si sus reglas son un subconjunto de la parte estricta de un ordenamiento de simplificación. [4] [8]
Notas
^ Las entradas entre paréntesis indican propiedades inferidas que no forman parte de la definición. Por ejemplo, una relación irreflexiva no puede ser reflexiva (en un conjunto de dominios no vacíos).
^ excepto que todos los x i son iguales para todos los i más allá de algún n , para una relación reflexiva
^ Dado que x < y implica y < x , ya que el último es una instancia del primero, para las variables x , y .
^ es decir, si l i > r i para todo i , donde (>) es un ordenamiento de reducción; el sistema no necesita tener un número finito de reglas
^ Dado que, por ejemplo, a > b implicaba g ( a )> g ( b ) , lo que significa que la segunda regla de reescritura no era decreciente.
^ es decir, un orden de reducción total del terreno
^ En caso contrario, t | p > t para algún término t y posición p , lo que implica una cadena descendente infinita t > t [ t ] p > t [ t [ t ] p ] p > ... [6] [7]
^ ab Dershowitz, Jouannaud (1990), sección 5.2, p.274
^ ab Dershowitz, Jouannaud (1990), sección 5.1, p.272
^ ab Dershowitz, Jouannaud (1990), sección 5.1, p.271
^ David A. Plaisted (1978). Un ordenamiento definido recursivamente para demostrar la terminación de sistemas de reescritura de términos (informe técnico). Univ. de Illinois, Departamento de Ciencias Computacionales, pág. 52. R-78-943.
^ N. Dershowitz (1982). "Ordenamientos para sistemas de reescritura de términos" (PDF) . Theoret. Comput. Sci . 17 (3): 279–301. doi :10.1016/0304-3975(82)90026-3. S2CID 6070052.Aquí: p.287; las nociones tienen nombres ligeramente diferentes.
