Om beta-substitutie op een object @lam term te modelleren, wordt de volgende regel gebruikt:

%%file /tmp/beta.sexp
(insert [(@lam x x) 42])
(rewrite  [(@lam x {?body x}) ?e] {?body ?e}) ; beta substitution. Matches app(lam,e) basically.
(run 10)
(extract [(@lam x x) 42])

! lambda-microegg /tmp/beta.sexp
; inserted e3
; rewrite 1 added
; ran 1 rounds, 1 unions: 3 classes, 4 e-nodes
; match 6.092µs, apply 4.989µs, rebuild 5.892µs
42

Wat ik feitelijk heb toegevoegd, is de mogelijkheid voor patroonvariabelen om meer context te hebben dan de basiscontext.

In dit eerste voorbeeld wordt een substitutie geretourneerd in een context van grootte 1, waarbij ?b de vrije variabele in die context is:

%%file /tmp/ctx.sexp
(insert (@lam x (@lam y (+ 3 y))))
(match (+ ?a ?b))

! lambda-microegg /tmp/ctx.sexp
; inserted e4
; match 1: ctx1 |-> {?a = 3, ?b = $0}

In dit zeer vergelijkbare voorbeeld bevindt de context van de substitutie zich in context 0 (de lege context). ?b verwijst naar een extra gebonden variabele. Dit is in zekere zin een lambda, maar dan een meta-lambda.

%%file /tmp/ctx2.sexp
(insert (@lam x (@lam y (+ 3 y))))
(match (@lam y (+ ?a {?b y})))

! lambda-microegg /tmp/ctx2.sexp
; inserted e4
; match 1: {?a = 3, ?b = ctx1 |-> $0}

Ik heb besloten om ctx0 |-> annotaties te onderdrukken omdat ze te veel ruis veroorzaken. Conceptueel is ctx0 |-> echter prior aan "context-loze" termen; context-loze termen bestaan niet, ze zijn simpelweg een shorthand voor ctx0. Constanten zijn in feite functies met een ariteit van 0.

Alpha-equivalentie en Thinning

Alpha-equivalente termen worden via hash consing naar hetzelfde object gekoppeld. De l_10 annotaties zijn de lifting annotaties, die worden bewaard in een byte die is afgenomen van de u32 Id.

%%file /tmp/alpha.egg
(insert (@lam x (@lam y (+ x y))))
(insert (@lam a (@lam b (+ a b))))
(print-egraph)

! lambda-microegg /tmp/alpha.egg
; inserted e3
; inserted e3
; egraph: 4 classes, 4 e-nodes
; e0 = ctx1 |-> $0
;   e0 <- var
; e1 = ctx2 |-> (+ $0 $1)
;   e1 <- (+ l_10(e0) l_01(e0))
; e2 = ctx1 |-> (@lam x0 (+ $0 x0))
;   e2 <- (@lam e1)
; e3 = ctx0 |-> (@lam x0 (@lam x1 (+ x0 x1)))
;   e3 <- (@lam e2)

Interessanter is dat er geheugendeling plaatsvindt tussen termen die niet alpha-equivalent zijn, maar wel sterk gerelateerd via thinning. De diepere termen in (@lam z (@lam w (@lam v x))) en (@lam z (@lam w (@lam v y))) maken gebruik van hash consing naar dezelfde vorm. Een naïve De Bruijn-index benadering zou dit niet doen. In feite betaal je alleen voor het geheugen van variabelen die daadwerkelijk worden gebruikt, niet voor alle variabelen die in scope zijn.

%%file /tmp/thin.sexp
(insert (@lam x (@lam y (@lam z (@lam w (@lam v x))))))
(insert (@lam x (@lam y (@lam z (@lam w (@lam v y))))))
(print-egraph)

! lambda-microegg /tmp/thin.sexp
; inserted e5
; inserted e7
; egraph: 8 classes, 8 e-nodes
; e0 = ctx1 |-> $0
;   e0 <- var
; e1 = ctx1 |-> (@lam x0 $0)
;   e1 <- (@lam l_10(e0))
; e2 = ctx1 |-> (@lam x0 (@lam x1 $0))
;   e2 <- (@lam l_10(e1))
; e3 = ctx1 |-> (@lam x0 (@lam x1 (@lam x2 $0)))
;   e3 <- (@lam l_10(e2))
; e4 = ctx1 |-> (@lam x0 (@lam x1 (@lam x2 (@lam x3 $0))))
;   e4 <- (@lam l_10(e3))
; e5 = ctx0 |-> (@lam x0 (@lam x1 (@lam x2 (@lam x3 (@lam x4 x0)))))
;   e5 <- (@lam e4)
; e6 = ctx0 |-> (@lam x0 (@lam x1 (@lam x2 (@lam x3 x0))))
;   e6 <- (@lam e3)
; e7 = ctx0 |-> (@lam x0 (@lam x1 (@lam x2 (@lam x3 (@lam x4 x1)))))
;   e7 <- (@lam l_0(e6))

Beperkingen in Miller-patronen

Een nuance is dat ik momenteel alleen "geordende Miller-patronen" ondersteun. Dit wordt alleen zichtbaar in niet-lineaire patronen waar een variabele twee keer wordt gebruikt. Om dit volledig op te lossen, zou ik termcreatie in patronen moeten toestaan of thinnings moeten uitbreiden om ook exchange te ondersteunen.

Dit betekent dat variabelen in het patroon moeten worden toegepast in dezelfde volgorde waarin ze zijn gebonden. (lam x (lam y (?a x y))) is toegestaan, maar (lam x (lam y (?a y x))) is dat niet.

%%file /tmp/nogood.sexp
(rewrite (@lam x (@lam y (pair {?a x y} {?a y x}))) wontwork)

! lambda-microegg /tmp/nogood.sexp
/tmp/nogood.sexp:2:41: error: Miller metavariable '?a' arguments are out of order; write {?a x y} on the match left-hand side, then permute its arguments on the rewrite right-hand side if needed

Toekomstige Plannen en Reflecties

Ontwikkelingsideeën

• Ondersteuning voor complexere patronen door termcreatie in patronen toe te staan.
• Het verwijderen van FOApp ten gunste van een uniformere benadering, ondanks mogelijke prestatieverliezen.
• Ondersteuning voor meer dan 7 variabelen via "ephemeral enodes".
• Integratie van Buchberger, multiset, string en semiring completion.
• Ontwikkeling van bewijssystemen (proof logs) in de stijl van Lean.

Toepassingsgebieden

• Relationele calculus
• Integratieregels
• Programma-interpreters
• Type checkers
• Fixpoint reasoning
• $\forall \exists$ reasoning (calc mode)

Technische details over implementatie

Ik gebruik momenteel een "Fat Id" door 1 byte van de u32 Id te gebruiken voor thinnings. Met een slimme encoding-truc (waarbij een sentinel 1 aangeeft waar de thinning-bitvector begint) kunnen maximaal 7 variabelen in de context worden ondersteund.

Er is een ingebouwde routine voor capture-avoiding substitution die in de rechterzijde kan worden gebruikt. Deze kopieert recursief de e-graph of is equivalent aan het extraheren van termen, substitueren en opnieuw invoegen. De Lifting techniek zorgt ervoor dat een term altijd wordt versterkt naar zijn minimale vereiste context.

Reflectie op AI en Ontwikkeling

Ik heb AI intensief gebruikt bij de ontwikkeling. Hoewel de code door AI soms "losser" aanvoelt en ik niet elke detail van de index-manipulatie wiskundig heb gecontroleerd, werkt het op basis van tests. AI bleek vooral nuttig voor lokale implementatiedetails en het versnellen van het proces, aangezien ik meer ideeën heb dan programmeervaardigheid.

Over Binders en Contexten

Een belangrijke les is dat binders zelf niet het essentiepunt zijn, maar dat contexten een integraal onderdeel zijn van wat termen zijn ([[ctx |- t]]). De waardevolle functionaliteiten zijn de manipulaties van deze contexten, zoals weakening en exchange. Liftings en thinnings zijn manieren om dit te implementeren.

Het complexe aan binders is dat ze meerdere contexten binnen één patroon creëren. Posities in een patroon kunnen verschillende variabelencontexten hebben, en men moet specificeren hoe termen tussen deze contexten bewegen.

In een patroon zoals (map (lam x ?b) ?l) dat matcht tegen 7 |-> e4, bevindt de top van het patroon en ?l zich in context 7, terwijl ?b zich in context 8 bevindt. De substitutie die wordt overgedragen naar de rechterzijde moet zich in de topcontext van het patroon bevinden.

Ten slotte herhaal ik dat de restrictie op de volgorde van variabelen in Miller-patronen de complexiteit aanzienlijk heeft verminderd, zonder veel kracht te verliezen, aangezien argumenten simpelweg kunnen worden omgewisseld in de rechterzijde van een rewrite.