Orden de reescritura

En informática teórica , en particular en el razonamiento automatizado sobre ecuaciones formales, se utilizan órdenes 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 demostrado ser útiles en investigaciones teóricas.

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 usar 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 propiamente más corto que el término s "; aplicar cualquier regla del conjunto siempre acortará el término de forma adecuada.

Por el contrario, para establecer la terminación de la "distribución" utilizando la regla x *( y + z ) → x * y + x * z , se necesitará un orden de reducción más elaborado, ya que esta regla puede aumentar considerablemente el tamaño del término debido a la duplicación de x . La teoría de los órdenes de reescritura tiene como objetivo ayudar a proporcionar un orden apropiado en tales casos.

Formalmente, una relación binaria (→) en el conjunto de términos se denomina relación de reescritura si es 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 además irreflexiva y transitiva , entonces se denomina orden de reescritura , ^{[ 1 ]} o preorden de reescritura . Si esta última (→) es además bien fundada , 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érminos se denomina orden de simplificación . ^{[ 4 ]}

• La recíproca , el cierre simétrico , el cierre reflexivo y el cierre transitivo de una relación de reescritura es de nuevo una relación de reescritura, al igual que la unión y la intersección de dos relaciones de reescritura. ^{[ 1 ]}
• Lo contrario de una orden de reescritura es, de nuevo, una orden de reescritura.
• Si bien existen órdenes de reescritura que son totales en el conjunto de términos básicos ("total básico" para abreviar), ninguna orden de reescritura puede ser total en el conjunto de todos los términos . ^{[ nota 3 ] [ 5 ]}
• Un sistema de reescritura de términos { l ₁ ::= r ₁ ,..., l _n ::= r _n , ...} es terminante si sus reglas son un subconjunto de un ordenamiento de reducción. ^{[ nota 4 ] [ 2 ]}
• Por el contrario, para todo sistema de reescritura de términos terminante, el cierre transitivo de (::=) es un orden de reducción, ^{[ 2 ]} que, sin embargo, no tiene por qué ser extensible a uno fundamental-total. Por ejemplo, el sistema de reescritura de términos fundamental { f ( a )::= f ( b ), g ( b )::= g ( a ) } es terminante, pero se puede demostrar que lo es usando un orden de reducción solo si las constantes a y b son incomparables. ^{[ nota 5 ] [ 6 ]}
• Un ordenamiento de reescritura fundamental y bien fundamentado ^{[ nota 6 ]} contiene necesariamente la relación de subtérminos 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 fundamentado cuando el conjunto de símbolos de función es finito. ^{[ 5 ] [ nota 9 ]}
• Un sistema de reescritura de términos finitos { l ₁ ::= r ₁ ,..., l _n ::= r _n , ...} es terminante si sus reglas son un subconjunto de la parte estricta de un orden de simplificación. ^{[ 4 ] [ 8 ]}

Nachum Dershowitz ; Jean-Pierre Jouannaud (1990). «Sistemas de reescritura». En Jan van Leeuwen (ed.). Modelos formales y semántica . Manual de informática teórica. Vol.  B. Elsevier. pp. 243–320 . doi : 10.1016/B978-0-444-88074-1.50011-1 . ISBN  9780444880741.