A proof-theoretic approach to abstract interpretation

Technische Samenvatting: Een Bewijstheoretische Aanpak van Abstracte Interpretatie

Probleemstelling
Abstracte interpretatie is een fundamentele theorie voor formele programma-verificatie, ontworpen om geluidse approximaties van programmasemantiek te genereren om onbeslisbare of computationeel onhandelbare problemen op te lossen. Traditioneel relateert deze theorie een complex concreet model (bijvoorbeeld de machtsverzameling $P(\Sigma)$ van programmalexecuties) aan een eindig abstract rooster $A$ via een geadjungeerd paar afbeeldingen: een concretisatieafbeelding $\gamma$ en een abstractieafbeelding $\alpha$. Hoewel de connectie tussen abstracte interpretatie en logica sinds het ontstaan van de theorie is erkend, is deze pas recentelijk systematiserend. Eerdere werken (bijvoorbeeld [5], [3]) introduceerden het concept van een "interne logica" voor een abstractie en identificeerden logica's die ten grondslag liggen aan specifieke abstracties. Een algemene, procedurale methode om de interne logica van een willekeurige abstractie te genereren, samen met een corresponderend bewijssysteem, blijft echter een open uitdaging.

Methodologie
De auteurs stellen een algemene procedure voor om een logica $L_A$ te genereren die correspondeert met een eindige abstractie $A = (A, \sqsubseteq, Op_A)$ met een concretisatieafbeelding $\gamma: A \to (P(\text{Struct}), \subseteq, Op_c)$. De methodologie construeert de logica zodanig dat haar Lindenbaum-Tarski-algebra isomorf is met de abstracte algebra $A$. De constructie verloopt via de volgende stappen:

1. Verbindingsmiddelen: De logische verbindingsmiddelen van $L_A$ worden gedefinieerd als die bewerkingen die door de concretisatieafbeelding $\gamma$ worden behouden. Als $A$ een eindig distributief rooster is, is het een bi-Heyting-algebra, waardoor implicatie en co-implicatie beschikbare kandidaten zijn.
2. Predicaten: Voor elk element $a \in A$ wordt een unair predikaatsymbool $a(x)$ aan de taal toegevoegd.
3. Introductieregels: Voor elke door $\gamma$ behouden connectief worden passende introductieregels aan het bewijssysteem toegevoegd.
4. Axiomatische Regels:
   • Voor binaire connectieven $\star$ waarbij $a \star b = c$, wordt de regel $a(x) \star b(x) \dashv\vdash c(x)$ toegevoegd.
   • Voor unaire connectieven $\star$ waarbij $\star a = b$, wordt de regel $\star a(x) \dashv\vdash b(x)$ toegevoegd.
   • Voor orde-relaties waarbij $a \leq b$, wordt de regel $a(x) \vdash b(x)$ toegevoegd.

De auteurs erkennen dat deze procedure "naïef" en computationeel inefficiënt is vanwege potentiële redundantie in axioma's, maar benadrukken de toepasbaarheid ervan op elk eindig rooster en elke concretisatieafbeelding.

Belangrijkste Resultaten en Theoretische Bevindingen
Het artikel stelt drie primaire lemma's vast met betrekking tot de geconstrueerde logica $L_A$:

• Geluidheid (Lemma 1): De logica $L_A$ is geluid met betrekking tot de concretisatie $\gamma$. Dit wordt bewezen door inductie op de bewijsdiepte, gebaseerd op het feit dat $\gamma$ de connectieven behoudt en dat de axioma's de relaties in de concrete algebra weerspiegelen.
• Isomorfisme (Lemma 2): De Lindenbaum-Tarski-algebra $L$ van $L_A$ is isomorf met de abstracte algebra $A$. De afbeelding $e: A \to L$ gedefinieerd door $e(a) = [a(x)]$ (de equivalentieklasse van het predikaat) wordt aangetoond een surjectieve, injectieve orde-inbedding en een homomorfisme te zijn.
• Volledigheid (Lemma 3): Als $\gamma$ een orde-inbedding is, is $L_A$ volledig met betrekking tot de concretisatie. Dit resultaat versterkt eerdere bevindingen (specifiek [5, Proposition 5]) door de voorwaarde te versoepelen van $\gamma$ als een injectieve rechteradjunct tot simpelweg een orde-inbedding.

Casestudies en Uitbreidingen
Het artikel past dit kader toe op specifieke scenario's:

• Cartesische Producten: De methodologie generaliseert naar $n$ variabelen. Wanneer predicaten worden gevormd door conjuncties van enkelvoudige variabele predicaten ($\phi_i(x) = \bigwedge \psi^i_k(x_k)$), is het resulterende rooster een cartesisch product van roosters met één variabele. De concretisatieafbeelding correspondeert met de toewijzing van verzamelingen aan $n$-dimensionale rechthoeken.
• Logica van Octagonen: De auteurs analyseren predicaten van de vorm $\pm x \pm y \geq c$. Zij observeren dat, hoewel $\gamma$ negatie behoudt, het geen conjunctie of disjunctie behoudt (aangezien de doorsnede van dergelijke predicaten vaak resulteert in geometrische vormen die niet representeerbaar zijn door een enkel predikaat in het rooster). Bijgevolg is een logica die uitsluitend vertrouwt op klassieke negatie zwak. Om dit aan te pakken, stellen de auteurs voor om conjunctie en disjunctie te gebruiken als meta-connectieven om sequenten te behandelen, terwijl zij erop wijzen dat de roosterstructuur van octagonen bestaat uit meet- en join-irreducibele elementen (exclusief top en bottom), wat toelaat voor een involutieve negatie.

Betekenis en Aanspraken
Het artikel positioneert zichzelf als een verzameling voorlopige resultaten en observaties uit lopend werk. De primaire betekenis ligt in:

1. Generalisatie: Het uitbreiden van de resultaten van [3] om een algemene procedure te bieden voor het genereren van de interne logica van elke eindige abstractie.
2. Systematische Constructie: Het bieden van een concreet, zij het naïef, algoritme om een bewijssysteem te genereren waarbij de algebraïsche structuur van de logica gegarandeerd isomorf is met het abstracte domein.
3. Verfijning van Theorie: Het versterken van de theoretische link tussen orde-theoretische eigenschappen van concretisatieafbeeldingen en de volledigheid van de bijbehorende logica.

De auteurs stellen expliciet dat de huidige procedure inefficiënt is en computationele beperkingen negeert, en schetsen het werk als een fundamentele stap richting het karakteriseren van welke eigenschappen "percoleren" van niet-cartesiaanse abstracties naar cartesiaanse gevallen, in plaats van een kant-en-klaar verificatietool te presenteren.