Unification of Deterministic Higher-Order Patterns (Full Version)

Technische Samenvatting: Unificatie van Deterministische Hogere-orde Patronen

Probleemstelling
Dit artikel behandelt het unificatieprobleem voor een specifieke klasse van eenvoudig getypeerde $\lambda$-termen, bekend als Deterministische Hogere-orde Patronen (DHP's). Waar standaard hogere-orde unificatie onbeslisbaar en infinitair is (potentieel oneindig veel onvergelijkbare unificatoren opleverend), en eerste-orde unificatie beslisbaar en unitair is, nemen DHP's een unieke tussenpositie in. DHP's, geïntroduceerd door Yokoyama et al., zijn zodanig gedefinieerd dat hun matching-probleem deterministisch is (er bestaat ten hoogste één substitutie). Echter, in tegenstelling tot Millers hogere-orde patronen of Libal en Millers Unificatie van Functies als Constructoren (FCU), is het unificatie-probleem voor DHP's niet unitair; minimale complete verzamelingen van unificatoren (MCSU's) kunnen oneindig zijn. De kernuitdaging bestaat erin een correcte en volledige unificatieprocedure voor deze klasse te ontwikkelen die de potentiële infinitaire aard van de oplossingsruimte hanteert, terwijl de structurele eigenschappen die matching deterministisch maken, behouden blijven.

Methodologie
De auteurs stellen een correcte en volledige inferentiesysteem voor het berekenen van complete verzamelingen van unificatoren (CSU's) voor DHP's voor. De methodologie steunt op de volgende technische fundamenten:

1. Termrepresentatie: De procedure werkt op eenvoudig getypeerde $\lambda$-termen in $\beta\eta$-lange normaalvorm, waarbij gebruik wordt gemaakt van een $\beta\eta$-vrije formulering om de toepassing van substituties te vereenvoudigen en expliciete $\beta$-reductie tijdens bewijzen te vermijden.
2. Definitie van DHP's: Een term is een DHP als, voor elke subterm van de vorm $x_n.y(t_m)$ waarbij $y$ een vrije variabele is:
   • Elk argument $t_i$ minstens één gebonden variabele uit $x_n$ bevat (wat deterministische matching garandeert).
   • Argumenten "uitgebreid" zijn (hun $\eta$-normaalvormen zijn geen abstrcties).
   • Argumenten verschillend zijn onder de "uitgebreide subterm"-relatie (lokale restrictie), waardoor voorkomen wordt dat één argument een hogere-orde subterm van een ander is.
3. Inferentiesysteem: De unificatieprocedure is een niet-deterministisch inferentiesysteem dat werkt op paren van DHP's. Het breidt het raamwerk van volledige hogere-orde unificatie (Huet) uit, maar introduceert specifieke optimalisaties voor DHP's:
   • Flex-Flex-resolutie: In tegenstelling tot volledige hogere-orde unificatie, waarbij partiële bindingen vereist zijn voor flex-flex-paren (paren waarbij beide hoofden vrije variabelen zijn), lost het DHP-systeem deze op een "meest algemene manier" op. Regels (ff=) en (ff̸=) construeren unificatoren door respectievelijk alleen gelijke argumenten te behouden of argumenten te combineren zonder vrije variabelen in te voeren.
   • Projectie en Imitatie: Het systeem gebruikt imitatie- en projectieregels, maar beperkt deze om ervoor te zorgen dat de resulterende termen binnen de DHP-klasse blijven. Opmerkelijk is dat projecties in DHP's moeten resulteren in hoofden die functiesymbolen of gebonden variabelen zijn, en geen vrije variabelen.
   • Strategie voor Minimaliteit: Om ervoor te zorgen dat de berekende verzameling unificatoren minimaal (orthogonaal) is, definiëren de auteurs strategieën die prioriteit geven aan (rem)- en (var)-regels en deterministisch nieuwe variabele namen berekenen.

Belangrijkste Bijdragen en Resultaten

• Correctheid en Volledigheid: Het artikel bewijst dat het inferentiesysteem correct is (succesvolle afleidingen produceren geldige unificatoren) en volledig is (voor elke unificator $\delta$ bestaat er een afleiding die een unificator $\theta$ produceert zodanig dat $\theta$ algemener is dan $\delta$).
• Minimaliteit: De auteurs tonen aan dat onder specifieke strategieën (lokaal optimaal en deterministisch voor nieuwe variabelen) het inferentiesysteem een Minimale Complete Verzameling van Unificatoren (MCSU) produceert. Dit is significant omdat, bij algemene hogere-orde unificatie, minimale verzamelingen niet gegarandeerd orthogonaal of eindig zijn.
• Oneindige Oplossingsruimten: Het artikel levert voorbeelden (bijvoorbeeld Voorbeeld 10 en 13) die aantonen dat MCSU's voor DHP's oneindig kunnen zijn. Bijgevolg is het inferentiesysteem niet gegarandeerd terminerend, en blijft de beslisbaarheid van het DHP-unificatieprobleem een open vraag.
• Generalisatie van FCU: De methode generaliseert Libal en Millers FCU door de "globale restrictie" te verwijderen (die voorkomt dat een argument met een vrije variabele een subterm is van een variabelenargument in het gehele probleem). Door deze te laten vallen, behandelt het systeem een strikt grotere verzameling termen, maar verliest het de unitaire eigenschap van FCU.

Betekenis en Aanspraken
De auteurs positioneren dit werk als een noodzakelijk onderzoek naar een klasse termen waarbij matching deterministisch blijft, maar unificatie de unitaire eigenschap verliest en direct overschakelt naar infinitaire problemen. De betekenis ligt in:

1. Praktische Subroutines: DHP's zijn gedefinieerd als een klasse termen in plaats van een probleemafhankelijke restrictie (zoals FCU's globale restrictie). Dit maakt DHP's eenvoudiger te gebruiken als subroutine in geautomatiseerd stellingenbewijzen of logisch programmeren, aangezien men geen globale constraints hoeft te verifiëren om te bepalen of een term binnen het toepassingsgebied valt.
2. Theoretisch Inzicht: Het werk verduidelijkt de grens tussen deterministische matching en unitaire unificatie, en toont aan dat de overgang van unitaire naar infinitaire unificatie kan plaatsvinden zonder een eindige fase te doorlopen.
3. Simulatie van FCU: De auteurs beweren dat hun aanpak FCU kan simuleren; als een FCU-probleem een meest algemene unificator heeft, zal het inferentiesysteem deze vinden via een eindige, deterministische afleiding.

Het artikel concludeert met de vaststelling dat, hoewel het inferentiesysteem eindig vertakkend is, de niet-terminatie een bewijs van beslisbaarheid verhindert. Toekomstig werk zou slimme representaties van oneindige verzamelingen unificatoren vereisen (bijvoorbeeld met behulp van reguliere grammatica's) om de scenario's met oneindige vertakking effectief te hanteren.