Orden de reescritura

Reescribiendo s a t por una regla l :: = r . Si l y r están relacionados por una relación de reescritura , también lo son s y t . Un pedido simplifcation refiere siempre l y s , y de manera similar r y t .

En la informática teórica , en particular en el razonamiento automatizado sobre ecuaciones formales, los ordenamientos de reducción se utilizan para evitar bucles sin fin . Reescribir órdenes y, a su vez, reescribir relaciones , son generalizaciones de este concepto que han resultado útiles en investigaciones teóricas.

Motivación

Intuitivamente, una orden de reducción R relaciona dos formales expresiones s y t si t es propiamente "simple" que s en algún sentido.

Por ejemplo, la simplificación de términos puede ser parte de un programa de álgebra de computadora 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 probar la imposibilidad de bucles sin fin al simplificar un término, se puede utilizar el orden de reducción definido por " sRt si la expresión t es propiamente más corta que la expresión s "; la aplicación de cualquier regla del conjunto siempre acortará adecuadamente el plazo.

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

Definiciones formales

Formalmente, una relación binaria (→) en el conjunto de términos se llama 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 (→) también es irreflexivo ytransitivo , entonces se llama reescritura de orden , ^[1] o reescritura de preorden . Si el ú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 reescritura de cierre es la relación de reescritura más pequeño que contiene R . ^[3] Una relación de reescritura transitiva y reflexiva que contiene el orden de subtermo se llama orden de simplificación . ^[4]

Descripción general de las relaciones de reescritura ^{[nota 1]}

	reescribir la relación	reescribir orden	orden de reducción	orden de simplificación
cerrado bajo contexto x R y implica u [ x ] p R u [ y ] p	sí	sí	sí	sí
cerrado bajo instanciación x R y implica x σ R y σ	sí	sí	sí	sí
contiene la relación de subtermo y el subtermo de x implica x R y				sí
reflexivo siempre x R x		(No)	(No)	sí
irreflexivo nunca x R x		sí	sí	(No)
transitivo x R y y y R z implica x R z		sí	sí	sí
bien fundamentado sin cadena infinita x 1 R x 2 R x 3 R ... [nota 2]			sí	(Sí)

Propiedades

• Lo contrario , 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 inverso de un orden de reescritura es nuevamente un orden de reescritura.
• Si bien existen órdenes de reescritura que son totales en el conjunto de términos básicos ("terreno total" 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 , ...} está terminando si sus reglas son un subconjunto de un orden de reducción. ^{[nota 4] [2]}
• A la inversa, para cada sistema de reescritura de términos de terminación, el cierre transitivo de (:: =) es un orden de reducción, ^[2] que no necesita ser extensible a uno total fundamental, sin embargo. Por ejemplo, el sistema de reescritura de términos básicos { f ( a ) :: = f ( b ), g ( b ) :: = g ( a )} está terminando, pero se puede mostrar así usando un orden de reducción solo si las constantes a y b son incomparable. ^{[nota 5] [6]}
• Un ordenamiento de reescritura total y bien fundado ^{[nota 6]} contiene necesariamente la relación de subterráneos adecuada en términos básicos . ^{[nota 7]}
• A la inversa, un ordenamiento de reescritura que contiene la relación subterránea ^{[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 ₁ :: = r ₁ , ..., l _n :: = r _n , ...} está terminando si sus reglas son un subconjunto de la parte estricta de una ordenación de simplificación. ^{[4] [8]}

Notas

1. 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ío).
2. excepto que todas las x _i son iguales para todas las i más allá de alguna n , para una relación reflexiva
3. Dado que x < y implica y < x , ya que la última es una instancia de la primera, para las variables x , y .
4. es decir, si l _i > r _i para todo i , donde (>) es un orden de reducción; el sistema no necesita tener un número finito de reglas
5. Dado que, por ejemplo, a > b implicaba g ( a )> g ( b ) , lo que significa que la segunda regla de reescritura no disminuía.
6. es decir, un pedido de reducción total de terreno
7. 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]}
8. es decir, una simplificación de pedidos
9. La prueba de esta propiedad se basa en el lema de Higman o, más generalmente, en el teorema del árbol de Kruskal .

Referencias

Nachum Dershowitz ; Jean-Pierre Jouannaud (1990). "Reescribir sistemas". En Jan van Leeuwen (ed.). Modelos formales y semántica . Manual de Informática Teórica. B . Elsevier. págs. 243–320. doi : 10.1016 / B978-0-444-88074-1.50011-1 . ISBN 9780444880741.

1. Dershowitz, Jouannaud (1990), sección 2.1, p.251
2. Dershowitz, Jouannaud (1990), sección 5.1, p.270
3. Dershowitz, Jouannaud (1990), sección 2.2, p.252
4. Dershowitz, Jouannaud (1990), sección 5.2, p.274
5. Dershowitz, Jouannaud (1990), sección 5.1, p.272
6. Dershowitz, Jouannaud (1990), sección 5.1, p.271
7. David A. Plaisted (1978). Un pedido definido de forma recursiva para probar la terminación de los sistemas de reescritura de plazos (informe técnico). Univ. de Illinois, Departamento de Comp. Carolina del Sur. pag. 52. R-78-943.
8. N. Dershowitz (1982). "Pedidos para sistemas de reescritura de términos" (PDF) . Theoret. Computación. Sci . 17 (3): 279-301. doi : 10.1016 / 0304-3975 (82) 90026-3 . S2CID 6070052 .  Aquí: p. 287; las nociones se nombran ligeramente diferentes.