I have been writing posts about Lifting Egraphs video as an intriguing way of adding variables and scope into an egraph. But pulling back a little, I can see that the simpler thing to talk about first is lifting terms.

Before you talk about complex things like egraphs or knuth bendix, it’s good to talk about simple terms first.

What is a “Term”?

The standard definition of term (in the second that this is what you’ll find in a textbook like TRAAT) is some kind of name and a list of ordered children.

In OCaml it’d look something like this type term = App of string * term list.

In python something like this

from dataclasses import dataclass

class Term:
    def __add__(self, other):
        assert isinstance(other, Term)
        return App("+", [self, other])

@dataclass
class App0(Term):
    f : str
    args : list[Term]

Noncontroversial right?

Actually I think there is a lot to push back on here. Yes, this is a good starting point, but there are a lot of other choices.

Many of these come from swapping out the list of children for something else or insisting on bits of extra data being available.

  • Keyword arguments type term = App of string * (string, term) dict. Keyword arguments are a very common, simple, and useful programming language feature. Why shouldn’t terms also have them? This invites the idea of subrecord patterns and record update syntax which seem to take you into a different notion of rewriting. I’ll note that swi-prolog has keyed dictionaries https://www.swi-prolog.org/pldoc/man?section=bidicts . Relatedly optional arguments. I kind of think K’s cells are keyed dictionaries https://kframework.org/k-distribution/k-tutorial/1_basic/13_rewrite_rules/ . Record update syntax and subrecord patterns is sort of a solution to the frame problem, since you don’t need to know all the keys, just the ones you wanna look at.
  • Compressed tries for 10000000000 arity functions type term = App of string * term bdd or type 'dom term = App of string * ('dom -> term) when 'dom is finite. Not strictly speaking different than a list of children or dict, but the mind goes to a different place. How many sins can be hidden in big but finite spaces? How many infinite notions can be approximated? That is often the SAT game.
  • Parametrized families of terms type 'param term = App of string * 'param * term list or perhaps type 'sym term = App of 'sym * term list See “WHAT IS ALGEBRAIC ABOUT ALGEBRAIC EFFECTS AND HANDLERS?” https://arxiv.org/abs/1807.05923 section 1.8.2
  • Fixed arity terms vs arbitrary length terms.
  • A specialization of parametrized families of terms where we insist the parameters have algebraic structure (typeclass constraint) such as a monoid or group.
  • Sets, multisets, polynomials of children. This is really more like what set theories perspective on what a tree is. But it is also useful for theories of associativity and commutativity AC ACI. The data structure holding children (the “container”) has its own algebra and notion of canonization.
  • Terms with semi-persistent proof trails
  • Typed terms should carry their types probably type term = App of string * term list * typ. Maybe alternatively symbols should be type decl = {name : string; dom : typ list; range : typ} rather than strings. type term = App of decl * term list
  • Binary application terms. Enables currying, lambda free higher order logic (LFHOL) / Hilog style thinking type term = App of term * term | Const of string
  • Terms that aren’t uniformly represented. “non-generic” / using language level generics. type term = Foo of term * term | Bar of term * term rather than using the strings “foo” and “bar” as function symbols. This is like egg’s Language style. It relies on more language level generic trickery to have a common abstraction of the concept of “term”. A typeclass, or interface or protocol of “term”.
  • abstract binding trees, which is close in spirit to what lifting terms are supporting
  • All sorts of combinations of the above

It is highly unlikely that any metatheoretical result or formalization about rewriting on one form of these terms transfers without modification to the others. I am skeptical of the idea of abstracting over all these options. Abstraction is sometimes evil.

Lifting Terms

Lifting terms are the same ideas as the liftng egraph but simplified to the term setting. We consider the “context” to be an intrinsic part of the term, always available and never implicit. Terms carry both the scope they live in and an overapproximation of the support of which variables they actually use. Thinnings are a thing that tell you both of these pieces of information. The domain is the total scope, the thinning itself tells you the support.

I do kind of believe that I am basically taking Mcbridean well-scoped style and de dependent typifying it (although this isn’t literally my process. I can’t really read agda that well). Data that would appear in indices of the types are just struct fields. This syntax is well scoped in the sense that it carries data about it’s scope and has assertions that fail if you do something wrong like apply a function symbol to two terms from a different sized scope.

I need thinnings (for more on thinnings: https://www.philipzucker.com/thin1/ )

from dataclasses import dataclass, field, replace
type Thin = list[bool]
def dom(f : Thin): # domain is big side
    return len(f)
def cod(f : Thin): # codomain is small side
    return sum(f)
def comp(f : Thin, g : Thin) -> Thin:
    assert cod(f) == dom(g)
    i = 0 
    result = []
    for a in f:
        if a:
            result.append(g[i])
            i += 1
        else:
            result.append(False)
    assert i == len(g)
    return result   


@dataclass
class App(Term):
    f : str
    args : list[Term]
    lift : Thin

    __match_args__ = ("f", "children")

    def __init__(self, f: str, args: list[Term], lift: Thin = None):
        # smart constructor. I guess this isn't strictly necessary, but I like it.
        d = dom(args[0].lift) if args else 0
        assert all(dom(arg.lift) == d for arg in args) # all args have to make sense in context d
        self.f = f
        if lift is None: # infer common lifting
            used = [False]*d
            for arg in args:
                for i in range(d):
                    used[i] |= arg.lift[i]
            args = [replace(arg, lift=[x for keep,x in zip(used, arg.lift) if keep]) for arg in args] # lower arguments into needed context
            self.args = args
            self.lift = used #id(d) if lift is None else lift
        else:
            #assert all(dom(arg.lift) == cod(lift) for arg in args)
            self.args = args
            self.lift = lift

    def do_lift(self, lift : Thin):
        assert cod(lift) == dom(self.lift)
        return App(self.f, self.args, comp(lift, self.lift))
    
    @property
    def children(self):
        """
        The "smart" deconstructor unapply. There is no reason you should ever be looking at raw args
        """
        return [replace(arg, lift=comp(self.lift, arg.lift)) for arg in self.args]
    
    def __repr__(self):
        l = "".join([str(int(keep)) for keep in self.lift])
        return f"l{l}_{self.f}({",".join(map(repr, self.args))})"

def Function(f : str):
    return lambda *args: App(f, args)

I mentioned in my talk a naive nameless well dimensioned style $var_{di}$. This is a combinator that returns those

def Vars(d : int):
    # return all variables in scope d
    return [App("var", [], [False]*i + [True] + [False]*(d-i-1)) for i in range(d)]
def Const(name, d : int):
    return App(name, [], [False]*d)

zero = Const("zero", 3)
zero # the 0-arity function zero lifted into the 3 context / to take 3 unused arguments

l000_zero()

z is $lift_{001}(var)$

x,y,z = Vars(3)
z

l001_var()

The smart constructor keeps subterms in as small a context as possible

x + zero + y

l110_+(l10_+(l1_var(),l0_zero()),l01_var())

When we match, we want to recompose the liftings so that the subterms make sense in the current context. Making custom smart __match_args__ is probably one notch too cute. __match_args__ is “unapply”, the function that undoes what smart constructors do. In this case, it is not a compressive process, so no search is required. If search was required as in AC etc, __match_args__ is not a sufficiently flexible mechanism.

def match_example(t):
    match t:
        case App(f, [t0,t1]):
            return f, (t0,t1)
        case _:
            assert False, t
print("the total term", zero + y)
print("the decomposed term", match_example(zero + y))

the total term l010_+(l0_zero(),l1_var())
the decomposed term ('+', (l000_zero(), l010_var()))

Binders

A thing I had kicked down the road was dealing with binders. I’m still not really sure the most elegant way of dealing with them and I feel like a big insight actually is that binders are not the essential thing under consideration, they are an add on. Scope and variables in the scope are the essential thing. Binders are a kind of combinator that moves

One kind of combinator is “named lambda”. In a naive named representation of lambda, one might use | Lam of string * term to represent it. This is kind of the same thing. It is a curious combination of named and nameless style. You don’t have to bind variable 0 as you do in de bruijn indices. But the “cost” of not doing so is that you shadow the outer “x”.

I think perhaps a more general form of App would also have a dump or widen field to account for all the ways functions might also destroy scope. Or maybe Binder and Var ought to be separate constructors from App because they have different fields? The whole thing doesn’t hold together that elegantly as is.

Substitution needs to be nlam aware. Also the smart deconstructor children doesn’t make sense anymore.

The achieve this named lambda action in terms of typical de bruijn lambdas we’d need an exchange move to move the variable to the front, then create the lambda, then weaken to replace the old position and shift everything to it’s original spot.

def NLam(x : App, body : App) -> App:
    assert x.f == "var"
    t = App("nlam", [x, body])
    for i in range(dom(x.lift)):
        if x.lift[i]:
            t.lift[i] = False
    return t

NLam(x,y)

l010_nlam(l10_var(),l01_var())

These are de bruijn index combinators. They aren’t that pleasant because the de bruijn index notion of variable keeps changing the total binder depth which is confusing to keep track of.

def Var(d, i):
    # a de bruijn index variable i in scope d
    assert 0 <= i < d
    t = [False]*d
    t[i] = True
    return App("var", [], t)


def Lam(body : App) -> App:
    lift = body.lift[1:] # the 0th variable is bound and not in scope outside the lambda
    body = App(body.f, body.args, [body.lift[0]] + [True]*cod(body.lift[1:])) # body's lift becomes an identity except for first slot which says if bound var is used or not
    return App("lam", [body], lift=lift)

print(Lam(Var(3,0))) # This variable is bound by the lambda
print(Lam(Var(3,2))) # This variable reaches outside the lambda

l00_lam(l1_var())
l01_lam(l01_var())

open_lam undoes the smart constructor. The action of doing so is a little weird. It isn’t clear to me that there is nice a way of undoing nlam that isn’t error prone. The clobbering is weird.

def open_lam(l : App):
    assert l.f == "lam" and len(l.args) == 1
    body = l.args[0]
    return App(body.f, body.args, lift=[body.lift[0]] + comp(l.lift, body.lift[1:]))

assert open_lam(Lam(Var(3,0))) == Var(3,0)
assert open_lam(Lam(Var(3,2))) == Var(3,2)

Substitution and Pattern Matching

We can substitute into object variables.

def subst(self, n : int, t : Term) -> Term:
    assert 0 <= n < len(self.lift) and dom(self.lift) == dom(t.lift), "subst: bad lift sizes"
    match self:
        case App("var", []):
            assert sum(self.lift) == 1
            if self.lift[n]:
                return t
            else:
                return self
        case App(f, children):
            assert f != "lam" and f != "nlam", "not handled yet"
            if self.lift[n]: # we can tell if there is something down there. I guess this is an optimization. We don't have to check it
                return App(f, [subst(arg, n, t) for arg in children])
            else:
                return self

        case _:
            raise ValueError("Unexpected case", self)
            
subst(x + zero, 0, zero + x)

l100_+(l1_+(l0_zero(),l1_var()),l0_zero())

A pattern variable (metavariable) is a very different thing from a var. var is kind of rigid and pattern variables are very flexible. An “object variable”. The scope respecting pattern matching here is kind of like Miller pattern matching. By putting a lift on PVar you can restrict whether a pattern succeeds or not by saying what variables it is allowed to use


@dataclass
class PVar(Term):
    name : str
    lift : Thin

def pmatch(t : App, pat : Term) -> dict[str, Term] | None:
    subst = {}
    todo = [(t, pat)]
    while todo:
        (t, pat) = todo.pop()
        if isinstance(pat, PVar):
            assert len(t.lift) == len(pat.lift)
            if any(used and not allowed for used,allowed in zip(t.lift, pat.lift)):
                return None
            if pat.name in subst:
                if subst[pat.name] != t:
                    return None
            else:
                subst[pat.name] = t
        elif isinstance(t, App) and isinstance(pat, App):
            if t.f != pat.f or len(t.args) != len(pat.args):
                print("Fail", t, pat)
                return None
            todo.extend(zip(t.children, pat.children))
        else:
            raise ValueError("unexpected case", t, pat)
    return subst

def PVars(names, d):
    return [PVar(name, [True]*d) for name in names.split()]

a,b,c = PVars("a b c", 3)
pmatch(zero + zero, zero + a)

{'a': l000_zero()}

pmatch(zero + x, a + b)

{'b': l100_var(), 'a': l000_zero()}

def ConstPat(name, d):
    return PVar(name, [False] *d)
p = ConstPat("p", 3)

pmatch(zero + x, p + a)


{'a': l100_var(), 'p': l000_zero()}

pmatch(zero + x, a + p) # fails because p can't match x

Bits and Bobbles

I think Lam and NLam really should be their own classes. Or maybe I need an Extend?

d is kind of the scope depth we’re at and in that sense feels connected to de Bruijn levels.

While I was pushing ahead to get my talk out, there is a simpler thing to

It is kind of interesting that there are different combinators for lambda and variables depending on whether you are interfacing with the thing in a named style or de bruijn style.

        case App("nlam", [x, body]):
            if x.lift[n]: # shadowed
                return self 
            else:
                return NLam(x, subst(body, n, t))
        case App("lam"), _):
            return Lam(self.args[0])

Could refactor the lift field to be in Term superclass. Not sure this saves much or is less confusing.

Lam and NLam should

@dataclass
class Lam(Term):
    _body : Term
    lift : Thin

    __match_args__ = ("body",)
    def __init__(self, body):

    @property
    def body(self):
        return body([self._body.lift[0]] + comp(self.lift, self._body.lift[1:])_

@dataclass
class NLam(Term):
    clobber : int
    body : Term
    lift : Thin

    #__match_args__ = # ?? It isn't clear how to make this non confusing
    def __init__(self, x : Term, body):
        assert x.f == "var" and sum(x.lift) == 1

    def

Substitution of pattern variables

def subst_pat(pat : Term, subst : dict[str, Term]) -> Term:
    match pat:
        case App(f, []):
            return self
        case App(f, children):
            return App(f, [subst_pat(a, subst) for a in children])
        case PVar(name, lift):
            if name in subst:

            else:
                return self
            

def rule(t, lhs, rhs):
    subst = pmatch(t, lhs)
    if subst is not None:

Typed terms and untyped can be intermixed. Typed ~ synth terms, untyped ~ check terms? Both carry thinnings

synth terms don’t have to have a data field persay of sort, but a @property(sort) that computes on demand is fine too

https://github.com/msp-strath/TypOS https://www.youtube.com/watch?v=bcjq9Y0JVYE

Extend?

class TyTerm:
    f : str
    args : list[TyTerm]
    sort : str

class TyTerm:
    f : Decl
    args : 

class App: # app is synth
    f : TyTerm
    x : Term
    sort : str

class Const(Term):
    f : str

class TyConst(TyTerm):
    f : str
    sort : str

class Annot(TyTerm):
    t : Term
    sort : str

class Forget(Term):
    t : TyTerm

I actually don’t really understand how typed thinnings work.

Dependent context = partially commutative. Exchange really requires dignification. Context is a DAG not list. Recipe to extract subdag is more complex data than recipe to extract sublist. Mapping of codomain dag to “index” of domain dag? index being path?

type Type = str

class Term:
    f : str
    lift : Thin
    tyctx : list[Type] # same length as codomain (?) of lift since the stuff it doesn't use really should be irrelevant / parametric
    # In the opposite representation of lift  [(int dom index, Type)]