Non-Termination of Logic Programs Using Patterns

Technische Samenvatting: Niet-terminatie van Logische Programma's met behulp van Patronen

Probleemstelling
Dit artikel behandelt de automatische detectie van niet-terminatie in logische programma's (LP). Terwijl veel bestaand onderzoek zich richt op het detecteren van lussen (eindige herschrijfsequenties die oneindig herhaald kunnen worden), richt dit werk zich op niet-lusvormige niet-terminatie. Dit zijn oneindige herschrijfsequenties die geen enkele lus bevatten, waardoor ze inherent niet-periodiek en moeilijk te detecteren zijn. De auteur merkt op dat dergelijke sequenties kunnen voortkomen uit eenvoudige logische programma's, terwijl standaard methoden voor lusdetectie deze vaak niet kunnen identificeren. De motivatie is tweeledig: theoretisch (het bestuderen van opmerkelijke vormen van oneindige sequenties) en praktisch (programmeurs helpen bij het identificeren van queries die eeuwig blijven draaien).

Methodologie
De auteur past een benadering aan die oorspronkelijk door Emmes et al. (2012) voor term herschrijfsystemen werd geïntroduceerd, toe aan het domein van logische programmering. De kernmethodologie bestaat uit het definiëren van een nieuwe unfolding-techniek die "patronen" genereert die potentieel oneindige verzamelingen van eindige herschrijfsequenties beschrijven.

1. Patroondefinities:

   • Patroon-substituties: Gedefinieerd als paren $\theta = (\sigma, \mu)$, aangeduid als $\sigma \star \mu$, die een verzameling substituties beschrijven: $\{\theta(n) = \sigma^n\mu \mid n \in \mathbb{N}\}$.
   • Patroon-termen: Paren $(s, \theta)$ die de verzameling $\{s\theta(n) \mid n \in \mathbb{N}\}$ beschrijven.
   • Patroonregels: Paren van patroortermen $(p, q)$ die een verzameling binaire regels beschrijven: $\{(p(n), q(n)) \mid n \in \mathbb{N}\}$.

2. Correctheid en Unfolding:

   • Een patroonregel wordt als correct beschouwd met betrekking tot een programma $P$ als de verzameling regels die het beschrijft een deelverzameling is van de binaire unfolding van $P$ ($binunf(P)$).
   • De auteur introduceert een nieuwe unfolding-operator $T^\pi_{P,B}$ die patroonregels berekent vanuit een programma $P$ en een basisset van correcte patroonregels $B$. Deze operator gebruikt een unificatie-algoritme voor patroortermen om regels te combineren, waardoor het programma effectiever "unfolds" dan traditionele binaire unfolding door oneindige deelverzamelingen van $binunf(P)$ in eindige representaties te vangen.

3. Eenvoudige Patronen en Unificatie:

   • Om de benadering automatiseerbaar te maken, beperkt de auteur het domein tot eenvoudige patroortermen, waarbij de substituties een specifieke structuur volgen met behulp van unaire contexten.
   • Er wordt een unificatie-algoritme geleverd voor deze eenvoudige termen. Dit algoritme brengt eenvoudige patroortermen in kaart naar termen over een gespecialiseerde signatuur $\Upsilon$ (gebruikmakend van unaire symbolen $c_{a,b}$ om herhaalde embeddings te representeren) en past klassieke unificatie-algoritmen toe (bijv. Robinson, Martelli-Montanari).
   • Het algoritme is gedeeltelijk correct bewezen: als het succesvol termineert, produceert het een meest algemene unifier (mgu) voor de invoerpatroonsequenties.

4. Niet-terminatie Criteria:

   • Algemeen Criterium (Stelling 3): Geadapteerd van Emmes et al., stelt dit dat als de patroon-unfolding een regel bevat van de vorm $(u \star \sigma \star \mu, u\sigma^a \star \sigma^b\sigma' \star \mu\mu')$ waarbij $\sigma'$ commuteert met $\sigma$ en $\mu$, er een oneindige keten bestaat.
   • Speciaal Criterium (Stelling 5): Een gemakkelijker te controleren conditie voor speciale patroonregels (een deelverzameling van eenvoudige regels). Als een dergelijke regel in de unfolding voorkomt, bewijst het artikel het bestaan van een oneindige keten beginnend bij specifieke instanties van de linkerzijde van de regel.

Belangrijkste Bijdragen
Het artikel presenteert vier primaire bijdragen:

1. Nieuwe Unfolding-techniek: Een methode om correcte patroonregels te produceren voor logische programmering, die een compactere presentatie biedt dan de negen inferentie-regels gebruikt in term herschrijving en de noodzaak voor complexe applicatiestrategieën elimineert.
2. Eenvoudige Patroortermen en Unificatie: De definitie van een beperkte vorm van patroortermen ("eenvoudig") en een bijbehorend unificatie-algoritme dat correct is bewezen.
3. Automatiseerbare Voldoende Voorwaarde: Een gemakkelijk te controleren conditie (Stelling 5) om niet-lusvormige niet-terminatie te detecteren vanuit eenvoudige patroonregels.
4. Implementatie (NTI): De implementatie van deze benadering in een tool genaamd NTI.

Experimentele Resultaten
De auteur heeft NTI geëvalueerd op 41 logische programma's afgeleid van niet-lusvormig niet-terminerende Term Herschrijfsystemen (TRS) uit de Termination Problem Data Base (TPDB).

• Succes: De tool bewees succesvol de niet-terminatie van 36 van de 41 programma's. Opvallend genoeg slaagde het voor 4 programma's (gemarkeerd met † in de tabellen) die niet door een andere TRS-analyzer in de International Termination Competition tot en met 2024 als niet-terminerend waren aangetoond.
• Falen: De benadering faalde bij 5 programma's, voornamelijk door de incompletheid van het unificatie-algoritme bij het gebruik van de "natuurlijke keuze" voor term-representanten (zoals besproken in Voorbeeld 12) of de beperking tot eenvoudige patronen (Voorbeeld 9).
• Prestaties: De executietijden waren over het algemeen laag (onder de 300ms voor succesvolle gevallen), hoewel sommige complexe gevallen leidden tot time-outs.

Betekenis en Claims
De auteur claimt dat hun benadering de enige tool die deelneemt aan de International Termination Competition in staat is om de terminatie van logische programma's te weerleggen. Er wordt opgemerkt dat er wel een andere benadering van Payet (2024) bestaat voor het bewijzen van niet-lusvormige niet-terminatie, maar dat deze een andere klasse van niet-lusvormigheid behandelt en niet in staat is de specifieke programma's die in dit artikel zijn getest (Tabellen 1 en 2) te weerleggen. Omgekeerd kan de Payet (2024) benadering de terminatie weerleggen van programma's waar deze methode faalt. De twee benaderingen worden dus gepresenteerd als complementair.

Het artikel sluit bescheiden af door te erkennen dat het unificatie-algoritme momenteel incompleet is en dat de beperking tot eenvoudige patronen de reikwijdte beperkt (bijv. falen op programma's die 1-contexten met variabelen vereisen). Toekomstig werk is gepland om de volledigheid aan te pakken, de initiële patroongeneratie (Prop. 2) uit te breiden en de benadering aan te passen aan TRS voor een directe vergelijking met Emmes et al. (2012).