💻 computer science

Work-in-Progress: A Tactic for Pattern Matching in Autosubst

Dit werk in uitvoering introduceert een automatische patroonmatchings-tactiek voor Autosubst die de huidige beperkingen in het afhandelen van typeringregels, reductierelaties en niet-unieke oplossingen aanpakt, zoals aangetoond door evaluaties op de POPLMark en POPLMark Reloaded uitdagingen.

Oorspronkelijke auteurs: Mathews George (Heriot-Watt University Edinburgh), Kathrin Stark (Heriot-Watt University Edinburgh)

Gepubliceerd 2026-07-15

📖 5 min leestijd🧠 Diepgaand

CC BY 4.0

Oorspronkelijke auteurs: Mathews George (Heriot-Watt University Edinburgh), Kathrin Stark (Heriot-Watt University Edinburgh)

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 een gigantische, magische puzzel probeert op te lossen waarbij elk stukje een verborgen label heeft. In de wereld van de informatica worden deze labels "De Bruijn-indices" genoemd. Het is een slimme manier om variabelen in code bij te houden, maar ze zijn berucht lastig. Denk aan het als een spelletief stoelen dansen waarbij de stoelen (variabelen) steeds van naam wisselen telkens wanneer er iemand gaat zitten. Als je probeert een puzzelstukje (een regel) te matchen met een gat (een doel) in dit spel, zien de stukjes er vaak anders uit, zelfs als ze eigenlijk hetzelfde zijn, alleen dragen ze een ander hoedje.

Lama tijd was een hulpmiddel genaamd Autosubst de held van dit verhaal. Het is als een superintelligente robot die direct kan vertellen of twee puzzelstukjes hetzelfde zijn, zelfs als hun labels door elkaar zijn gehusseld. Dit doet het door een set magische regels (de $\sigma$ -calculus) te gebruiken om de stukjes te normaliseren totdat ze identiek zijn. Als je alleen maar wilt controleren of twee dingen gelijk zijn, is deze robot perfect.

Het Probleem: De "Apply"-valstrik
Er is echter een addertje onder het gras. Wanneer je deze puzzelstukjes probeert te gebruiken om een probleem op te lossen door een regel toe te passen (zoals een "Apply"-knop gebruiken in een videogame), loopt de robot vast. Hij is erg goed in zeggen: "Ja, deze zijn gelijk," maar hij is erg slecht in zeggen: "Hier is hoe je dit stukje in dit specifieke gat past."

Waarom? Omdat een regel soms op meerdere manieren in een gat kan passen, en de robot niet weet welke manier de "juiste" is zonder hulp. In het verleden moesten menselijke programmeurs het zware werk doen. Ze moesten hun regels op vreemde, indirecte manieren herschrijven of handmatig de ontbrekende labels raden om de robot te laten werken. Het was alsof je probeerde een vierkant blokje in een rond gat te duwen door het blokje zelf bij te schuren, in plaats van gewoon de juiste tool te vinden.

Het Nieuwe Idee: Een Slimme Goktactiek
Dit paper introduceert een nieuw hulpmiddel genaamd as_apply. Denk aan dit als een nieuwe, iets avontuurlijkere robotarm die ontworpen is om die puzzelstukjes te pakken en ze in de gaten te duwen, zelfs wanneer de labels niet in eerste instantie perfect overeenkomen.

In plaats van op te geven of de mens te vragen alles te herschrijven, gebruikt deze nieuwe tactiek een set heuristieken (wat in feite geïnformeerde gissingen zijn op basis van patronen die het eerder heeft gezien). Het kijkt naar het gat, kijkt naar de regel en zegt: "Ik wed dat als ik deze labels slechts een klein beetje verschuif, ze zullen passen!"

Hoe het Werkt (De Magische Truc)
Het proces vindt plaats in twee stappen:

Voorbereiding: De robot maakt de puzzelstukken eerst netjes met de oude, betrouwbare Autosubst-regels om ze zo ordelijk mogelijk te maken.
Het Gokspel: Vervolgens probeert de robot de stukjes te matchen. Als de stukjes niet perfect matchen, raakt hij niet in paniek. In plaats daarvan probeert hij een paar specifieke trucs:
- Het controleert of de mismatch slechts een eenvoudige "verschuiving" is (zoals een variabele één plek omhoog bewegen).
- Het controleert of het ontbrekende stukje slechts een "identiteit" is (niets doen).
- Het zoekt naar veelvoorkomende patronen die meestal in deze puzzels voorkomen.

Als een van deze gissingen werkt, vult het de ontbrekende labels aan en gaat het verder. Als het mislukt, gaat het terug (backtracken) en probeert het een andere gok.

Wat het Paper Zegt (en Niet Zegt)
De auteurs zijn zeer voorzichtig om niet te veel te overdrijven. Ze geven toe dat dit geen toverstaf is die elke mogelijke puzzel oplost.

Het is niet perfect: Het paper stelt expliciet dat een puzzel soms meerdere oplossingen kan hebben, en dat deze robot de verkeerde kan kiezen. Het is mogelijk om een lastig voorbeeld te construeren waarbij de robot fout gokt, zelfs als er een juist antwoord bestaat.
Het is een "Work-in-Progress": De auteurs beschrijven dit als een methode in uitvoering ("work-in-progress"). Ze beweren niet de volledige theorie van het matchen voor altijd te hebben opgelost.
De Resultaten: Ze hebben deze nieuwe tactiek getest op twee beroemde, moeilijke uitdagingen genaamd POPLMark en POPLMark Reloaded. Dit zijn als de "Olympische Spelen" voor het bewijzen van zaken over programmeertalen.
- In de POPLMark-uitdaging (642 regels code) hebben ze de nieuwe tactiek 15 keer gebruikt.
- In de POPLMark Reloaded-uitdaging (683 regels code) hebben ze het 10 keer gebruikt.
- In elk van deze gevallen heeft de tactiek het doel succesvol opgelost.

Het Oordeel
Het paper suggereert dat hoewel deze nieuwe tactiek theoretische limieten heeft (het kan in de war raken door zeer vreemde, vijandige puzzels), het verrassend goed werkt in de echte wereld. Het stelt programmeurs in staat om te stoppen met het op vreemde, indirecte manieren herschrijven van hun regels en ze gewoon natuurlijk te schrijven.

De auteurs zijn hoopvol maar voorzichtig. Ze suggereren dat deze aanpak de oude, logge manier van doen in veel praktische gevallen kan vervangen, maar ze weten dat er nog werk te doen is om te garanderen dat de robot nooit, ooit, de verkeerde oplossing kiest. Ze werken momenteel aan het uitzoeken van precies welke soorten puzzels deze robot met 100% zekerheid kan oplossen, en welke er mogelijk nog steeds menselijke controle vereisen.

Kortom: het is een slim, behulpzaam nieuw hulpmiddel dat de rommelige taak van het matchen van puzzelstukjes veel gemakkelijker maakt, ook al is het nog niet klaar om de enige tool in de gereedschapskist te zijn.

Technische Samenvatting: Een tactiek voor patroonherkenning in Autosubst

Probleemstelling
Het artikel behandelt een specifieke beperking in het Autosubst-framework, een code-generator voor de Rocq (voorheen Coq) bewijsassistent die redeneren over de bruijn-termen en substitutie via de $\sigma$ -calculus automatiseert. Hoewel Autosubst succesvol de gelijkheidscontrole voor aannamevrije doelen automatiseert via de asimpl-tactiek, faalt het wanneer gebruikers aannames (bijv. typeringregels of lemma's) op een doel proberen toe te passen via standaard tactieken zoals apply of eapply.

In deze scenario's moet de gebruiker een doel verenigen met een aanname modulo $\sigma$ -equivalentie. De automatisering van Autosubst is echter niet ontworpen voor het matchen tegen aannames. Hierdoor worden gebruikers gedwongen om omslachtige werkwijzen te gebruiken, zoals:

Het formuleren van regels in indirecte vormen (met behulp van verse meta-variabelen in plaats van directe substitutie-termen).
Het introduceren van hulp-lemma's om de kloof tussen het doel en de aanname te overbruggen.
Het handmatig transformeren van doelen of het expliciet instantiëren van existentiële variabelen tijdens bewijzen.

De kern van de moeilijkheid ligt in het feit dat $\sigma$ -matching (matchen modulo $\sigma$ -equivalentie) niet uniek is; één enkel matching-probleem kan meerdere oplossingen toelaten, waarvan niet allemaal voldoen aan de premissen van de context. Bovendien is second-order matching voor de volledige $\lambda\sigma$ -calculus onbeslisbaar, en zelfs zonder $\beta$ -reductie zijn oplossingen niet noodzakelijkerwijs uniek.

Methodologie
De auteurs stellen een heuristische tactiek voor in ontwikkeling genaamd as_apply, geïmplementeerd in de Ltac-taal van Rocq, om patroonherkenning modulo $\sigma$ -equivalentie te automatiseren. De tactiek werkt in twee primaire fasen:

Preprocessing:
- Zowel het doel als de conclusie van de doel-aanname worden genormaliseerd met betrekking tot de $\sigma$ -calculus met behulp van de bestaande asimpl-tactiek.
- Gekwantificeerde variabelen in de aanname worden vervangen door existentiële variabelen (evars).
- De premissen van de aanname worden omgezet in subdoelen die na de matching-fase opgelost moeten worden.
- De tactiek handelt conversies af tussen expliciete hernaamingsoperaties (bijv. $s\langle\xi\rangle$ ) en instantiatie-operaties ( $s[\xi]$ ) met behulp van substify en renamify.
Matching-fase:
- De tactiek construeert een set matching-vergelijkingen $M = \{s_i =_\sigma t_i\}$ tussen de doel-termen en de geïnstancieerde aanname-termen.
- Het verwerkt vergelijkingen van links naar rechts met een partiële procedure, $\sigma_{min}$ , die probeert te matchen modulo het $\sigma_{min}$ -fragment (een subset van $\sigma$ -regels die instantiatie en compositionaliteit karakteriseert).
- Heuristieken: Als $\sigma_{min}$ $σ_{min}$ faalt om een match te vinden, past de tactiek een set heuristieken toe die veelvoorkomende patronen in formele ontwikkelingen vangen. Deze omvatten:
  - Het afhandelen van vergelijkingen van de vorm $s[t \cdot \sigma] =_\sigma ?s[t \cdot id]$ door de onbekende te instantiëren met een gelifte substitutie ( $?s \mapsto s[\Uparrow\sigma]$ ).
  - Het afhandelen van gevallen die betrokkenheid van identiteits-substituties of specifieke variabele-structuren hebben.
- Na het toepassen van substituties normaliseert de tactiek de aanname opnieuw. Succes wordt bepaald als het doel en de aanname syntactisch gelijk worden.

De tactiek is gegeneraliseerd om de volledige inputtaal van de Autosubst-compiler te ondersteunen, inclusclusief meerdere wederzijds inductieve sorts, vector-substituties en first-class hernamingen.

Kernbijdragen

Introductie van as_apply: Een heuristische tactiek ontworpen om apply/eapply in Autosubst-gebaseerde ontwikkelingen te vervangen, wat matching modulo $\sigma$ -equivalentie mogelijk maakt in de aanwezigheid van aannames.
Generalisatie: Uitbreiding van de matching-logica om de volledige door Autosubst ondersteunde syntaxis te dekken, inclusief complexe binders en hernamingsoperaties.
Empirische Evaluatie: Toepassing van de tactiek op standaard benchmarks, specifiek de POPLMark en POPLMark Reloaded uitdagingen.

Resultaten
De auteurs evalueerden as_apply op de POPLMark (642 regels) en POPLMark Reloaded (683 regels) uitdaging-oplossingen.

Frequentie van gebruik: De tactiek werd 15 keer gebruikt in de POPLMark B-oplossing en 10 keer in de POPLMark Reloaded-oplossing.
Effectiviteit: In alle geteste gevallen loste as_apply de beoogde doelen succesvol op.
Vereenvoudiging: Het gebruik van de tactiek elimineerde de noodzaak voor de indirecte regel-formuleringen, hulp-lemma's en handmatige doel-transformaties die de eerdere oplossingen kenmerkten.
Beperkingen: De auteurs erkennen dat as_apply niet $\sigma$ -compleet is en geen beslisser is. Omdat $\sigma$ -matching meerdere oplossingen kan hebben, betekent het heuristische karakter van de tactiek dat deze theoretisch een onjuiste oplossing zou kunnen selecteren wanneer een correcte oplossing bestaat, hoewel dergelijke fouten niet zijn waargenomen in de casestudies.

Betekenis en Claims
Het artikel beweert dat hoewel het theoretische probleem van $\sigma$ -matching inherent moeilijk is (niet-unieke oplossingen, onbeslisbaarheid in volledige $\lambda\sigma$ ), een pragmatische, heuristische aanpak in de praktijk een hoog niveau van automatisering kan herstellen. De betekenis ligt in het verminderen van de handmatige last voor gebruikers die werken met de Bruijn-syntax, waardoor zij typeringregels en lemma's in hun directe, natuurlijke vormen kunnen formuleren in plaats van in indirecte vormen die zijn afgestemd op de beperkingen van de unificatie-engine van de bewijsassistent.

De auteurs blijven bescheiden over de huidige staat van het werk en bestempelen het als "Work-in-Progress". Ze merken op dat de huidige tactiek vertrouwt op heuristieken vanwege de potentie voor oneindige of meerdere oplossingen. Toekomstig werk is gericht op het identificeren van het grootste fragment $\sigma'$ waarvoor een uniciteitscriterium geldt, wat potentieel kan leiden tot een matching-tactiek met bewezen garanties.

Meer zoals dit