La procedura di completamento Knuth -Bendix o completamento di Knuth-Bendix (detto anche algoritmo di Knuth-Bendix ) trasforma, in caso di successo, un insieme finito di identità (in termini ) descrive un algebrica struttura in una riscrittura sistema di termini confluente e che termina (quindi detto convergente ). Il processo di completamento è stato inventato da Donald Knuth con l' aiuto di uno studente di nome Peter Bendix per l'implementazione.
In caso di successo, il completamento fornisce un mezzo efficace per risolvere la parola problema per l'algebra in questione, come è stato dimostrato da Gérard Huet . Ad esempio, per la teoria dei gruppi equazionali (vedi diagramma a destra), il completamento fornisce un sistema per riscrivere i termini che sono confluenti e terminanti. Possiamo quindi decidere se un'equazione t 1 = t 2 è vera in tutti i gruppi (anche se decidere se una formula del primo ordine è vera in tutti i gruppi è indecidibile ).
Sfortunatamente, la parola problema è indecidibile in generale, la procedura di completamento non si concluderà sempre con successo. Può funzionare indefinitamente o fallire quando incontra un'identità non orientabile (che non può trasformare in una regola di riscrittura senza essere sicuri di non mettere in pericolo la terminazione).
Esiste una variante della procedura di completamento che non fallisce sulle identità non orientabili. Fornisce una procedura semi-decisiva per la parola problema, in altre parole, permette di dire se una data identità è deducibile dalle identità che descrivono l'algebra in questione, in tutti i casi in cui lo è sì, ma non può mai finire.
Per garantire la cessazione dei sistemi di riscrittura che intervengono durante il processo, ma anche per garantire la correttezza del metodo, il completamento di Knuth-Bendix prende come input un ordine <ai termini. La relazione deve essere irriflessiva, transitiva e ben fondata , chiusa dal contesto (se a <b allora x [a] p <x [b] p dove x [a] p e x [b] p sono i termini x dove abbiamo sostituito il sottotermine in posizione p rispettivamente con a e b), chiuso per istanziazione (se a <b, allora a [σ] <b [σ] per ogni sostituzione σ). Una relazione che soddisfi queste proprietà è un ordine di riduzione .
L' ordine lessicografico sui percorsi è un esempio di ordine di riduzione. È un ordine pratico perché è dato solo a partire da un ordine sui simboli delle funzioni. Dato un ordine sui simboli di funzione è definito da:
Alcuni lavori presentano prima la procedura di completamento sotto forma di una procedura ingenua che è lontana dall'attuazione pratica ma che consente di comprendere l'idea generale. La procedura di completamento di Knuth-Bendix prende come input un insieme finito di identità e un ordine di riduzione <sui termini. Produce come output un sistema di riscrittura delle identità che è allo stesso tempo confluente, terminante e compatibile con l'ordine. La procedura può anche dire esplicitamente che non riesce a costruire un tale sistema di riscrittura o che può divergere.
La procedura parte da un sistema di riscrittura ottenuto orientando le identità mediante l'ordine < (se esiste una regola che non è orientabile con l'ordine <, allora l'algoritmo dice che tale sistema di riscrittura non esiste). Ad esempio, se la voce del problema è:
1 * x = x ( 1 è un elemento neutro a sinistra) x -1 * x = 1 (x -1 è un inverso a sinistra di x ) (x * y) * z = x * (y * z) ( * è associativo)e l'ordine lessicografico sui cammini come ordine di riduzione> dove -1 > * > 1, l'algoritmo parte con il seguente sistema di riscrittura:
1 * x → x
x -1 * x → 1
(x * y) * z → x * (y * z)
Quindi la procedura completa il sistema di riscrittura aggiungendo regole aggiuntive nel tentativo di rendere il sistema confluente. Il completamento si basa sul comando <per garantire che il sistema venga sempre completato.
Durante il completamento, consideriamo le coppie critiche . Per ogni coppia critica (s, t), calcoliamo le forme normali s' e aggiungiamo s' → t 'o t' → s' con l'aiuto dell'ordine <. Ad esempio, 1 * z e x -1 * (x * z) formano una coppia critica irraggiungibile e sono già forme normali. Come x -1 * (x * z) > 1 * z , la procedura di completamento aggiunge la regola:
x -1 * (x * z) → 1 * z
Pertanto, il completamento aggiunge nuove regole al sistema di riscrittura e quindi appaiono nuove coppie critiche. Dobbiamo quindi continuare a completare il sistema di riscrittura. La procedura viene terminata con successo se non ci sono più nuove coppie critiche non raggiungibili. La procedura fallisce se è presente una coppia critica che non può essere resa raggiungibile con il comando <.
Pseudo-codice della procedura ingenua Entrée : un ensemble fini d'équations E un ordre < Sortie : un système de réécriture R qui termine, qui est confluent correspondant à E, et compatible avec l'ordre < s'il en existe un "non" ou alors boucle, s'il n'existe pas de tel système de réécriture R completionKnuthBendixVersionNaïve(E, <) si il existe une équation s = t dans E où s ≠ t et ni s < t, ni t < s retourner "non" sinon Soit R l'ensemble des règles G → D où G = D ou D = G est une équation de E et D < G répéter pour toute paire critique s, t de R s' := une R-forme normale de s t' := une R-forme normale de t si s' ≠ t' si t' < s' ajouter s' → t' à R sinon si s' < t' ajouter t' → s' à R sinon retourner "non" tant que R a été modifié par la boucle retourner RPossiamo presentare il completamento in modo sintetico usando regole di inferenza che trasformano sia il sistema di equazioni che il sistema di riscrittura. Sono scritti nella forma in cui il numeratore dà il sistema di equazioni e il sistema di riscrittura prima dell'applicazione della regola e il denominatore dà il sistema di equazioni e il sistema di riscrittura dopo l'applicazione della regola. Applicando le regole (in qualsiasi ordine e il più a lungo possibile), speriamo di trasformare lo stato iniziale dove ci sono le equazioni date come input e un sistema di riscrittura vuoto in uno stato finale dove non ci sono più equazioni da affrontare e un sistema di confluenza e riscrittura finale.
Diamo prima un insieme minimo di regole:
Nome della regola | Regola | Spiegazione |
---|---|---|
Orientare un'identità |
se s> t |
Trasforma un'identità in una regola usando l'ordine di riduzione < |
Dedurre un'identità |
se esiste u che si riscrive in s e che si riscrive in t |
Aggiunge un'identità dedotta dal sistema di riscrittura. La regola qui proposta è molto generale. Un caso speciale della regola consiste nell'aggiungere l'identità s = t per ogni coppia critica (s, t) di R. |
Rimuovere un'identità banale | Rimuove un'identità banale in cui i termini su entrambi i lati sono sintatticamente gli stessi. | |
Semplificare un'identità |
se s viene riscritto in s 'oppure t viene riscritto in t' |
Semplificare un'identità utilizzando il sistema di riscrittura. |
Indichiamo il seguente invariante: l'applicazione di una regola preserva le uguaglianze che possono essere dimostrate combinando le uguaglianze di E o le regole di riscrittura di R, il sistema di riscrittura finisce sempre. Le trasformazioni fanno solo crescere il sistema di riscrittura R.
Le quattro trasformazioni precedenti creano un sistema di riscrittura in cui sono presenti regole di riscrittura ridondanti e che, dato un ordine di terminazione, non è univoco. Per questo usiamo anche le due regole seguenti che sono delle ottimizzazioni per ottenere un sistema di riduzione con meno regole, unico per l'ordine che abbiamo dato e più efficiente per calcolare le forme normali.
Comporre |
se t viene riscritto come u |
Aggiunge una regola al sistema di riscrittura che compone la riscrittura s in t e t in u |
Crollo |
se s → u usando una regola G → D dove G non può essere ridotto di s → t |
Rimuove una regola con un lato sinistro semplificato, senza farla scomparire completamente |
Queste trasformazioni giocano un ruolo chiave nel dimostrare la correttezza della procedura di completamento.
In questa sezione, eseguiremo la procedura Knuth-Bendix su alcuni esempi per illustrare quando il completamento riesce, fallisce o si ripete.
Cerchiamo un sistema di riscrittura confluente che termini per il sistema di identità per semigruppi idempotenti dato da:
(x * y) * z = x * (y * z)
x * x = x
La figura a destra mostra le applicazioni delle regole dal sistema di identità (e un sistema di riscrittura vuoto) a un sistema di identità vuoto e un sistema di riscrittura confluente e terminante. Ci sono due prime applicazioni delle regole di orientamento. Poi una deduzione di un'identità perché x * z e x * (x * z) sono coppie critiche. Il sistema di riscrittura confluente che termina è:
(x * y) * z → x * (y * z)
x * x → x
x * (x * z) → x * z
Se il sistema di equazioni contiene:
x * y = y * x
quindi la procedura di completamento fallisce perché non riesce ad orientare l'equazione.
Considera l'esempio:
a * b = b * a
a * c = c * a = b * d = d * b = 1
Con l'ordine lessicografico sui cammini dati da 1 <a <c <b <d, il completamento termina. Ma con l'ordine lessicografico sui cammini dati da 1 <a <b <c <d, il completamento non finisce.
Esiste un'implementazione del completamento Knuth-Bendix per scopi didattici con un'interfaccia grafica. Ci sono varianti del completamento Knuth-Bendix in cui l'ordine di completamento non è dato a priori ma costruito durante il processo del processo di completamento.
Il Waldmeister Prover è un'implementazione di completamento. Ha vinto le sessioni dal 1997 al 2011 e la sessione 2014 del concorso CASC nella categoria UEQ (per logica del primo ordine equazionale unitaria).
Il completamento di Knuth-Bendix è implementato in strumenti di calcolo formali ad esempio Magma che utilizza il pacchetto kbmag.