2
$\begingroup$

I was reading the HOList paper that applies Graph Neural Networks (GNNs) to the HOL Light (HOList) data set and benchmark for ML for theorem proving. They describe their results etc but there is no code I can find or even pseudocde (algorithmic description) of how to transform an AST -> ABT. How does one do this?

This seemed like a solved problem obviously so I wanted to avoid re-inventing the wheel - especially if something already existed that is probably optimized or takes care of nuanced of the process.


References:

$\endgroup$
4
  • $\begingroup$ Do they describe how to do the transformation in their paper? If yes, what prevents you from re-implementing it based on their description? If not, can you provide some background on what an ABT is? $\endgroup$
    – D.W.
    May 18 at 19:02
  • $\begingroup$ @D.W. I cannot implement an algorithm that is not described. ABT is the graph representation of a logical formula where the variables point to the binders they are bound to. I added the paper link to make sure these questions would be easy to answer given the reference. Should I have added more details? $\endgroup$ May 18 at 22:08
  • 2
    $\begingroup$ I must be missing some context. I can't find anywhere in the paper that mentions ABT after a quick search. It sounds like you believe they are converting AST -> ABT, but I'm not clear on where that came from, or what ABT is, or what that transformation is supposed to be. I think it would be helpful to provide more background: a self-contained specification of what is ABT and what the semantics of that transformation should be; and some explanation of how that is connected to the paper you read. $\endgroup$
    – D.W.
    May 18 at 22:29
  • $\begingroup$ @D.W. I think you might be right. I promise to come back later read through my question more carefully and edit the question and remove this comment. Thanks for the feedback! :) $\endgroup$ May 19 at 16:28
1
$\begingroup$

Your referenced paper doesn't define the term "abstract binding trees"; where did you get that phrase? (I did not look at your other references; this paper was interesting enough by itself).

The paper does define a variety of transformations on ASTs by examples, but IMHO those examples are sufficient to define or least lookup the necessary algorithms.

What I interpret the paper as saying is, "(for our GNN-based theorem prover), you can use pure ASTs, or you can use a variety of variants which perform better because they take context into account".

If you work on compiling code, you already know the value of (semantic) context over a pure context-free parsing in validating program source text (and logical formulas are just a kind of programming text). I make this point brutally obvious here: Life After Parsing

They seem to define context in three different ways:

  • bidirectional links between parent and child nodes. Having links going both directions allows context to be computed bottom up, and to have context flow from some children of a node, to be passed as context to other children. This sounds like the value one obtains by having an attribute grammar, which has synthesized properties and inherited properties. I didn't read the paper carefully enough to understand what information was being propagated up, or what was being propagated down, or even how their GNN accomplished this effect. Implementing this is rather trivial: one needs child links and parent links in the nodes.

  • joining nodes in the AST that represent the same variable. What this is doing is taking into account scoping rules in the language, and amounts to replacing variable names by symbol table references. They argue that the type information associated with the symbols should be included, which you get for "free" if your symbol table includes type information, which any serious symbol table does. Implementing this requires that your AST processing machinery be augmented with symbol tables, and that the AST is processed to replace identifier nodes with symbol table entries (well, with the content of the appropriate symbol table entry). This is hard to do if your langauge is complex (e.g, symbol tables for C++ will make your head explode) you need an extremely organized attack to build/use these; this is part of the reason that building compiler front ends is hard. But for the HOL representations being used by the authors, the "symbol" tables are pretty simple and you can probably do this in an ad hoc way with a tree-scanning procedure.

  • Merging common subtrees honoring variable type information into single trees. This is classically what common sub-expression elimination does. Its apparent value in this paper is that it can dramatically shrink the size of the tree and therefore the implied amount of work it takes to process the tree. (You can get an overly compressed tree for free if you use a GLR parser which produces maximally shared subforests which happen to also include expression trees, but you have to split out shared subtrees based on type information after the fact). I note this looks to me not so much as context usage but "merely" size reduction.

TLDR: The authors appear to implementing classic compiler front end building techniques and algorithms to convert ASTs into what amounts to Directed Acyclic Graphs that encode type information for different variables.

[FWIW, a generalized AST-processing engine I build called DMS has: a) bidirectional links between parent and child nodes, b) shared subtrees via GLR parsing c) symbol table definition methods, d) attribute-grammar definition/execution which is easily used to scan ASTs to link leaves to symbol table entries. AFAICT, DMS sort of does everything this paper suggests doing. This is because you pretty much always need at least the results of all this to process any kind of AST in a semantically sensible way].

HTH.

$\endgroup$
4
  • $\begingroup$ Thanks for the great answer. I wasn't clear on what "common subtrees honoring variable type information" means - what is the meaning of "honoring" here? I wondered if that was a typo, but I couldn't figure out what it might be a typo for. $\endgroup$
    – D.W.
    May 24 at 17:46
  • $\begingroup$ Imagine you have two different scopes each containing a variable "s" in Java. In one scope, s is defined as a string. In another scope, s is defined as an integer. Now consider the expression "s+1" occuring twice, once in each scope. You can naively treat the two expression as identical (and that's what a context-free parser like GLR does) and use only a single common subexpression to represent them both. But they don't mean the same thing! "s+1" in the context of the string declaration of s means "concatenate"; "s+1" in the context of the integer declaration means "add" .... $\endgroup$
    – Ira Baxter
    May 24 at 17:51
  • $\begingroup$ .... so you don't want to make a common subexpression based only on syntax. You want the variables mentioned in the common subexpression to all refer to the same type, so the common subexpression has only one meaning. That means you don't want to make a CSE for the two different defintions of "s". Thus, sub-expressions that honor the types of the variables. Does that help? $\endgroup$
    – Ira Baxter
    May 24 at 17:52
  • $\begingroup$ Ahh, yes, that's very clear, and now I understand what you mean by "honoring". Thank you for the explanation! $\endgroup$
    – D.W.
    May 24 at 17:56

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.