💻 computer science

Templates in Rewriting Induction

Dit artikel presenteert een nieuwe op sjablonen gebaseerde aanpak voor het automatisch genereren van inductiehypothesen binnen Beperkte Herschrijvingsinductie voor hogere-orde Logisch Gelimiteerde Term-herschrijvingsystemen, waardoor het bewijzen van programmeer-equivalenties mogelijk wordt die eerder onbereikbaar waren door het herkennen van typische programmeerconstructies als instanties van hogere-orde functies.

Oorspronkelijke auteurs: Kasper Hagens, Cynthia Kop

Gepubliceerd 2026-04-30

📖 5 min leestijd🧠 Diepgaand

CC BY 4.0

Oorspronkelijke auteurs: Kasper Hagens, Cynthia Kop

Oorspronkelijk artikel gelicentieerd onder CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Dit is een AI-gegenereerde uitleg van het onderstaande artikel. Het is niet geschreven of goedgekeurd door de auteurs. Raadpleeg het oorspronkelijke artikel voor technische nauwkeurigheid. Lees de volledige disclaimer

Stel je voor dat je probeert te bewijzen dat twee verschillende recepten voor het bakken van een cake precies hetzelfde heerlijke dessert opleveren. Het ene recept is geschreven door een chef die van onderop werkt, ingrediënten één voor één toevoegend. Het andere is geschreven door een chef die van bovenaf werkt, lagen afpellen tot ze de basis bereiken.

In de wereld van de informatica zijn deze "recepten" programma's, en het bewijzen dat ze equivalent zijn, is een enorme uitdaging. Dit artikel, getiteld "Templates in Rewriting Induction", introduceert een slim nieuw hulpmiddel om wiskundigen en informatici te helpen bewijzen dat deze verschillende programma's hetzelfde doen, zelfs wanneer de wiskunde ongelooflijk ingewikkeld wordt.

Hier is de uiteenzetting van hun idee met behulp van eenvoudige analogieën:

Het Probleem: De "Afwijkende Paden"

De auteurs werken met een systeem genaamd Rewriting Induction (RI). Denk aan RI als een super-strenge scheidsrechter die controleert of twee programma's equivalent zijn door ze stap voor stap uit te voeren.

Meestal werkt dit prima. Maar soms raakt de scheidsrechter vast. Stel je voor dat de twee chefs (programma's) een faculteit berekenen (getallen vermenigvuldigen zoals 1×2×3...).

Chef A begint bij 1 en vermenigvuldigt tot 10.
Chef B begint bij 10 en vermenigvuldigt tot 1.

Terwijl de scheidsrechter probeert ze stap voor stap te vergelijken, worden de getallen enorm en verschillend. De scheidsrechter ziet:

"Chef A heeft 6!"
"Chef B heeft 24!"
"Chef A heeft 24!"
"Chef B heeft 120!"

De scheidsrechter blijft nieuwe, verschillende getallen krijgen en kan geen patroon vinden om te zeggen: "Oké, ze zijn hetzelfde." Ze blijven steken in een lus van divergentie. Om dit op te lossen, heeft de scheidsrechter meestal een "Lemma" nodig (een hulpregel of een afkorting) die zegt: "Hé, ook al zien de getallen er nu anders uit, ze volgen eigenlijk hetzelfde verborgen patroon."

De Vangst: Het vinden van deze verborgen patronen (lemmata) is moeilijk. Bestaande methoden zijn als het proberen het patroon te raden door naar de specifieke getallen te kijken (2, 6, 24, 120). Als het patroon te complex is of ingewikkelde beperkingen omvat (zoals "doe dit alleen als het getal positief is"), falen de oude methoden.

De Oplossing: De "Template"

De auteurs stellen een nieuwe aanpak voor: Templates.

In plaats van naar de specifieke getallen te kijken, kijken ze naar de vorm van het recept. Ze zeggen: "Laten we even de specifieke ingrediënten negeren en gewoon naar de structuur kijken."

Ze hebben vier "Meesterblauwdrukken" (Templates) gemaakt die de meeste veelvoorkomende programmeerlussen dekken:

Upward Tail Recursie: Klein beginnen en opbouwen.
Downward Tail Recursie: Groot beginnen en afbreken.
Upward General Recursie: Opbouwen maar een stapel taken bijhouden.
Downward General Recursie: Afbreken maar een stapel taken bijhouden.

Denk aan deze templates als universele adapters. Net zoals een universele stroomadapter in elk stopcontact past, ongeacht het land, kunnen deze templates in veel verschillende programma's passen.

Hoe Het Werkt: De "Recursor"

Het artikel introduceert "Recursors". Deze zijn als universele robots die elk van de vier blauwdrukken kunnen uitvoeren.

Als je een programma hebt dat omhoog telt, herkent het systeem dit als een voorbeeld van de "Omhoog Robot".
Als je een programma hebt dat omlaag telt, herkent het de "Omlaag Robot".

Zodra het systeem heeft geïdentificeerd dat Programma A een "Omhoog Robot" is en Programma B een "Omlaag Robot", hoeft het niet meer naar de specifieke getallen te kijken. Het controleert gewoon het wiskundige bewijs dat "Omhoog Robot" en "Omlaag Robot" equivalent zijn.

De auteurs bewijzen dat deze robots onder bepaalde voorwaarden equivalent zijn. Zodra dat hoog-niveau bewijs is voltooid, kan het systeem dit direct toepassen op elk specifiek programma dat de vorm overeenkomt.

Waarom Dit Een Grote Zaal Is

Het artikel beweert dat eerdere methoden waren als het proberen een puzzel op te lossen door naar elk stukje afzonderlijk te kijken. Als de puzzel te complex was (niet-polynomiale invarianten), gaf de solver het op.

Deze nieuwe methode is als een stap terugzetten en zeggen: "Ik hoef niet naar elk stukje te kijken; ik kan de afbeelding op de doos zien."

Oude Manier: "Is 24 gelijk aan 24? Is 120 gelijk aan 120? Is 720 gelijk aan 720?" (Raakt vast in complexe beperkingen).
Nieuwe Manier: "Beide programma's zijn gewoon 'Omhoog Tellen' en 'Omlaag Tellen' lussen. We hebben al bewezen dat die twee lusstypes equivalent zijn. Daarom zijn deze programma's equivalent."

De "Magie" van Beperkingen

Het artikel richt zich specifiek op Logically Constrained Term Rewriting Systems (LCSTRS).
Stel je een recept voor dat zegt: "Als de oven warmer is dan 350 graden, doe X; anders doe Y."
Oude methoden hadden moeite met het hanteren van deze "Als/Dan" voorwaarden bij het proberen equivalentie te bewijzen. De nieuwe template-methode behandelt ze natuurlijk omdat de "Blauwdrukken" de logica van de voorwaarden bevatten. Het stelt het systeem in staat te bewijzen dat twee programma's hetzelfde zijn, zelfs als ze complexe "Als/Dan" regels hebben, zolang de algehele vorm van de lus overeenkomt met een van de templates.

Samenvatting

De auteurs hebben een set universele vormen (templates) gebouwd voor veelvoorkomende programmeerlussen. Door te herkennen dat twee verschillende programma's gewoon verschillende versies van dezelfde vorm zijn, kunnen ze gebruikmaken van eerder bewezen wiskundige regels om ze equivalent te verklaren. Dit lost problemen op die eerder onmogelijk te bewijzen waren omdat de specifieke getallen of beperkingen te rommelig waren om direct te analyseren.

Kortom: Stop met het tellen van de appels; kijk naar de mand. Als de manden dezelfde vorm hebben, zijn de appels erin equivalent.

1. Probleemstelling

Het artikel behandelt een kritieke bottleneck in Rewriting Induction (RI), een formeel systeem dat wordt gebruikt om programmeer-equivalentie (inductieve stellingen) te bewijzen in Term Rewriting Systems (TRS). Hoewel RI krachtig is, faalt de praktische toepassing op real-world code vaak vanwege de moeilijkheid van automatische lemma-generatie.

Het Divergentie-probleem: Bij het bewijzen van de equivalentie van twee programma's (bijvoorbeeld verschillende implementaties van een faculteitsfunctie) komt het bewijsproces vaak een reeks vergelijkingen tegen die niet overeenkomen. Standaard RI-technieken (casusanalyse en herschrijving) genereren nieuwe vergelijkingen, maar kunnen eerdere vergelijkingen niet gebruiken als inductiehypothese omdat de termen structureel divergeren.
Beperkingen van bestaande methoden:
- Op beperkingen gebaseerde methoden (bijv. [9, 12]): Deze methoden proberen lus-invarianten te ontdekken (bijv. $z = a \times j$ ) om vergelijkingen te generaliseren. Hoewel ze effectief zijn voor eenvoudige rekenkunde, falen ze wanneer de relatie tussen variabelen niet-polynomiaal is of wanneer de lusstructuur complex is.
- Focus op laag niveau: Bestaande methoden opereren op het niveau van specifieke variabelewaarden en beperkingen, in plaats van hoog-niveau programmeerconstructen te herkennen (zoals tail-recursie versus algemene recursie).
Context: De auteurs richten zich op Logically Constrained Simply-typed Term Rewriting Systems (LCSTRSs), die real-world programmeercode modelleren met primitieve datatypes (gehele getallen, booleans) en logische beperkingen (guards). Dit maakt ze geschikter voor programmeerverificatie dan standaard TRS.

2. Methodologie

De auteurs stellen een Template-gebaseerde Lemma-generatie aanpak voor die hoog-niveau programmeerpatronen integreert in het Bounded RI-bewijsstelsel.

A. Het Concept van Templates

In plaats van te zoeken naar specifieke rekenkundige invarianten, definiëren de auteurs Templates: herschrijfschema's die veelvoorkomende programmeerconstructen vastleggen (bijv. opwaartse/afwaartse tail-recursie, algemene recursie).

Vier Kern-Templates:
1. TailUp ( $T^+$ ): Opwaartse tail-recursie (index neemt toe).
2. TailDown ( $T^-$ ): Afwaartse tail-recursie (index neemt af).
3. RecUp ( $R^+$ ): Opwaartse algemene recursie.
4. RecDown ( $R^-$ ): Afwaartse algemene recursie.
Hoger-orde Recursoren: Deze templates worden geformaliseerd als hoger-orde recursoren (bijv. tailup, recdn). Een specifiek programma wordt aan een template gekoppeld door een contextfunctie $F$ (de bewerking uitgevoerd in de lus) en grenzen ( $l, u$ ) te identificeren.

B. De Bewijsstrategie

De methodologie vertrouwt op een tweestaps bewijsproces binnen Bounded RI:

Template-Recursor Equivalentie: Bewijzen dat een concrete programma-implementatie equivalent is aan de corresponderende hoger-orde recursor (bijv. facTU $\approx$ tailup). Dit gebeurt door structurele inductie op de lusindex.
Recursor Equivalentie: Bewijzen van equivalenties tussen de abstracte recursoren zelf (bijv. tailup $\approx$ $\approx$ recdn).
- Eenzijdige Matching: Transformeer één kant van de doelvergelijking naar een recursor, pas vervolgens een bekende recursor-equivalentie toe om de andere kant te vereenvoudigen.
- Tweezijdige Matching: Transformeer beide kanten naar hun respectievelijke recursoren en pas direct een algemeen equivalentiestelling toe.

C. Conditionele Equivalenties

Voor gevallen waar eenvoudige equivalentie niet geldt (bijv. tailup versus taildn), introduceren de auteurs Conditionele Bounded Inductieve Stellingen. Deze bewijzen vertrouwen op axioma's (bijv. commutativiteit en associativiteit van de bewerking $F$ ) en specifieke ordeningseisen om terminatie en correctheid te waarborgen.

3. Belangrijkste Bijdragen

Nieuwe Heuristiek voor Lemma-generatie: Het artikel introduceert een methode die generaliseert over lusstructuren in plaats van specifieke variabelewaarden. Dit maakt het mogelijk om equivalenties te bewijzen die voorheen buiten bereik waren van op beperkingen gebaseerde invariantengeneratoren.
Integratie met LCSTRS: De aanpak is specifiek ontworpen voor Logically Constrained Simply-typed Term Rewriting Systems, wat directe modellering van gehele-getalrekenkunde en booleaanse guards mogelijk maakt zonder complexe coderingen.
Hoger-orde Abstractie: Door gebruik te maken van hoger-orde recursoren kan het systeem willekeurige bewerkingen (zoals vermenigvuldiging in faculteiten of functietoepassing in hoger-orde voorbeelden) als parameters behandelen, waardoor de templates herbruikbaar zijn over verschillende domeinen.
Formeel Bewijsstelsel: De auteurs definiëren de specifieke afleidingsregels (Vereenvoudigen, Casus, Verwijderen, Inductie, Hypothese) en ordeningseisen die nodig zijn om deze templates te integreren in het Bounded RI-kader.
Demonstratie van Kracht: Het artikel bewijst succesvol equivalenties tussen verschillende faculteitsimplementaties (Opwaarts versus Afwaarts, Tail versus Recursief) en hoger-orde varianten, inclusief gevallen waar de vereiste invarianten niet-polynomiaal zijn.

4. Resultaten

Succes met Faculteitsimplementaties: Het systeem bewees succesvol de equivalentie van vier verschillende faculteitsimplementaties (Iteratief Op/Af, Recursief Op/Af) onder de beperking $x \ge 1$ $x \geq 1$ .
- Kernprestatie: Het bewijzen van facTU $\approx$ facTD (Tail Up versus Tail Down) was onmogelijk voor eerdere methoden ([9, 12]) omdat de benodigde invarianten niet-polynomiaal waren. De template-aanpak loste dit op door de structurele gelijkenis van de lussen te herkennen.
Hoger-orde Uitbreidingen: De methode werd uitgebreid naar hoger-orde functies (bijv. funfacTU), waarbij equivalentie werd bewezen tussen implementaties die een functie $h$ toepassen op de lusindex voordat er wordt vermenigvuldigd.
Conditionele Bewijzen: Het systeem behandelde gevallen die axioma's vereisten (associativiteit/commutativiteit) om equivalenties tussen verschillende recursierichtingen te bewijzen (bijv. tailup $\approx$ taildn als de bewerking commutatief is).

5. Betekenis

Overbruggen van de Kloof: Dit werk overbrugt de kloof tussen geautomatiseerd stellingbewijzen op laag niveau (dat worstelt met complexe lussen) en programmeerverificatie op hoog niveau. Het verlegt de focus van "de juiste invariant vinden" naar "het juiste patroon herkennen".
Schaalbaarheid: Door specifieke rekenkundige waarden te abstraheer, schaalt de methode naar complexere computationele gedragingen waar polynoom-invarianten falen.
Automatiseringspotentieel: Hoewel momenteel geïmplementeerd als een handmatig/semi-automatisch proces in het hulpmiddel Cora, betogen de auteurs dat template-herkenning grotendeels syntactisch is, wat wijst op groot potentieel voor volledige automatisering in toekomstige hulpmiddelen.
Fundamenteel voor Programmeerverificatie: De aanpak biedt een robuust kader voor het verifiëren van programma-transformaties (bijv. het optimaliseren van een recursieve functie naar een tail-recursive versie) in aanwezigheid van logische beperkingen, wat essentieel is voor het verifiëren van moderne softwaresystemen.

Samenvattend presenteren Hagens en Kop een paradigmaschift in Rewriting Induction: een verschuiving van invariant-ontdekking naar structurele patroonmatching, waardoor de verificatie van programmeer-equivalenties mogelijk wordt die voorheen onbewijsbaar waren vanwege de complexiteit van hun inductieve invarianten.