Non-Termination of Logic Programs Using Patterns

Sintesi Tecnica: Non-Terminazione di Programmi Logici mediante Pattern

Definizione del Problema
Questo articolo affronta il rilevamento automatico della non-terminazione nei programmi logici (LP). Mentre gran parte della ricerca esistente si concentra sul rilevamento di loop (sequenze di riscrittura finite che possono essere ripetute indefinitamente), questo lavoro mira alla non-terminazione non-looping. Si tratta di sequenze di riscrittura infinite che non incorporano alcun loop, rendendole intrinsecamente non periodiche e difficili da rilevare. L'autore osserva che tali sequenze possono derivare da semplici programmi logici, eppure i metodi standard di rilevamento dei loop spesso non riescono a identificarle. La motivazione è duplice: teorica (studiare forme straordinarie di sequenze infinite) e pratica (aiutare i programmatori a identificare le query che eseguono cicli infiniti).

Metodologia
L'autore adatta un approccio originariamente introdotto per la riscrittura di termini da Emmes et al. (2012) al dominio della programmazione logica. Il nucleo della metodologia consiste nel definire una nuova tecnica di unfolding che genera "pattern" descriventi potenzialmente infiniti insiemi di sequenze di riscrittura finite.

1. Definizioni di Pattern:

   • Sostituzioni di Pattern: Definite come coppie $\theta = (\sigma, \mu)$, denotate $\sigma \star \mu$, che descrivono un insieme di sostituzioni $\{\theta(n) = \sigma^n\mu \mid n \in \mathbb{N}\}$.
   • Termini di Pattern: Coppie $(s, \theta)$ che descrivono l'insieme $\{s\theta(n) \mid n \in \mathbb{N}\}$.
   • Regole di Pattern: Coppie di termini di pattern $(p, q)$ che descrivono un insieme di regole binarie $\{(p(n), q(n)) \mid n \in \mathbb{N}\}$.

2. Correttezza e Unfolding:

   • Una regola di pattern è considerata corretta rispetto a un programma $P$ se l'insieme di regole che descrive è un sottoinsieme dell'unfolding binaria di $P$ ($binunf(P)$).
   • L'autore introduce un nuovo operatore di unfolding $T^\pi_{P,B}$ che calcola le regole di pattern da un programma $P$ e un insieme base di regole di pattern corrette $B$. Questo operatore utilizza un algoritmo di unificazione per i termini di pattern per combinare le regole, effettuando l'unfolding del programma più velocemente rispetto al tradizionale binary unfolding, catturando sottoinsiemi infiniti di $binunf(P)$ in rappresentazioni finite.

3. Pattern Semplici e Unificazione:

   • Per rendere l'approccio automatizzabile, l'autore restringe il dominio ai termini di pattern semplici, dove le sostituzioni seguono una struttura specifica che coinvolge contesti unari.
   • Viene fornito un algoritmo di unificazione per questi termini semplici. Esso mappa i termini di pattern semplici a termini su una firma specializzata $\Upsilon$ (usando simboli unari $c_{a,b}$ per rappresentare embedding ripetuti) e applica algoriti di unificazione classici (ad esempio, Robinson, Martelli-Montanari).
   • L'algoritmo è dimostrato parzialmente corretto: se termina con successo, produce un mgu (most general unifier) per le sequenze di pattern in ingresso.

4. Criteri di Non-Terminazione:

   • Criterio Generale (Teorema 3): Adattato da Emmes et al., afferma che se l'unfolding del pattern contiene una regola della forma $(u \star \sigma \star \mu, u\sigma^a \star \sigma^b\sigma' \star \mu\mu')$ dove $\sigma'$ commuta con $\sigma$ e $\mu$, allora esiste una catena infinita.
   • Criterio Speciale (Teorema 5): Una condizione più facilmente verificabile per le regole di pattern speciali (un sottoinsieme di regole semplici). Se tale regola esiste nell'unfolding, il documento dimostra l'esistenza di una catena infinita partendo da istanze specifiche del lato sinistro della regola.

Contributi Chiave
Il documento presenta quattro contributi primari:

1. Nuova Tecnica di Unfolding: Un metodo per produrre regole di pattern corrette per la programmazione logica, offrendo una presentazione più compatta rispetto alle nove regole di inferenza usate nella riscrittura di termini ed eliminando la necessità di strategie di applicazione complesse.
2. Termini di Pattern Semplici e Unificazione: La definizione di una forma ristretta di termini di pattern ("semplici") e un corrispondente algoritmo di unificazione dimostrato essere corretto.
3. Condizione Sufficiente Automatizzabile: Una condizione facilmente verificabile (Teorema 5) per rilevare la non-terminazione non-looping da regole di pattern semplici.
4. Implementazione (NTI): L'implementazione di questo approccio in uno strumento chiamato NTI.

Risultati Sperimentali
L'autore ha valutato NTI su 41 programmi logici derivati da Sistemi di Riscrittura di Termini (TRS) non-terminanti non-looping dal Termination Problem Data Base (TPDB).

• Successo: Lo strumento ha dimostrato con successo la non-terminazione per 36 dei 41 programmi. In particolare, ha avuto successo su 4 programmi (contrassegnati con † nelle tabelle) che non erano stati dimostrati non-terminanti da nessun altro analizzatore TRS nell'International Termination Competition fino al 2024.
• Fallimento: L'approccio è fallito su 5 programmi, principalmente a causa dell'incompletezza dell'algoritmo di unificazione quando viene utilizzata la "scelta naturale" per i rappresentanti dei termini (come discusso nell'Esempio 12) o della restrizione ai pattern semplici (Esempio 9).
• Prestazioni: I tempi di esecuzione sono stati generalmente bassi (sotto i 300ms per i casi di successo), sebbene alcuni casi complessi abbiano causato timeout.

Significatività e Rivendicazioni
L'autore afferma che il loro approccio è l'unico strumento partecipante alla International Termination Competition capace di confutare la terminazione di programmi logici. Nota che esiste un altro approccio, quello di Payet (2024), per provare la non-terminazione non-looping, ma esso affronta una classe diversa di non-loopingness ed è incapace di confutare la terminazione dei programmi specifici testati in questo articolo (Tabelle 1 e 2). Al contrario, l'approccio di Payet (2024) può confutare la terminazione di programmi in cui questo metodo fallisce. Pertanto, i due approcci sono presentati come complementari.

Il documento conclude con modestia, riconoscendo che l'algoritmo di unificazione è attualmente incompleto e che la restrizione ai pattern semplici ne limita l'ambito (ad esempio, fallendo su programmi che richiedono 1-context con variabili). Il lavoro futuro è pianificato per affrontare la completezza, estendere l'unfolding iniziale (Prop. 2) e adattare l'approccio ai TRS per un confronto diretto con Emmes et al. (2012).