Lifting Terms: Making Well Scoped Syntax Dumber | Hey There Buddo!

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:<br>def __add__(self, other):<br>assert isinstance(other, Term)<br>return App("+", [self, other])

@dataclass<br>class App0(Term):<br>f : str<br>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....