representing inference rules as both LaTeX and Abstract Syntax Trees

All inference rules in the Physics Derivation Graph are written in LaTeX. See the full list at
https://github.com/allofphysicsgraph/proofofconcept/tree/gh-pages/v4_file_per_expression/inference_rules
For example, the inference rule "add X to both sides" in LaTeX is
Add $#1$ to both sides of Eq.~\ref{eq:#2}.

AST representation in plain text

https://calculem.us/abstract-binding-trees-1/
Inference rules are transformations to the abstract syntax trees that represent expressions.
For example, the "add X to both sides" (addition property of equality) does the following transform:

input:expression
op
  LHS
  RHS

input:feed
x

output:expression
op
  +
    LHS
    x
  +
    RHS
    x


Here I'm using a two space indent to show the tree structure of the AST.
The "LHS" and "RHS" are sides of the expression. The "op" is the operator relating LHS and RHS.
I wanted a format that is visually accessible and not to verbose, while capable of being converted to some other format.

Order matters

My AST representation needs to include order. The expression "a-b" is distinct from "b-a" even though a tree doesn't specify the order:

input:expression:1
op
  c
  -
    a
    b

which is distinct from
input:expression:2
op
  c
  -
    b
    a


This also applies to cross product since it's also non-commutative.
To provide clarification, I'll assume the "top-to-bottom" order in the above format corresponds to "left-to-right." With that specification, the top AST corresponds to "c=a-b" and the bottom AST is "c=b-a".

AST for integrals and derivatives

Shown here: https://tug.org/TUGboat/tb12-3-4/tb33arnon.pdf

Mentioned here (http://www.math.wpi.edu/IQP/BVCalcHist/calc5.html) but not explored explicitly.

A definite integral in Latex
\int_{low}^{high} LHS d(x) = \int_{low}^{high} RHS d(x)
can be written as an AST:

input:expression
op
  \int
    low
    high
    LHS
    x
  \int
    low
    high
    RHS
    x

Similarly, a differential equation in Latex
\frac{d}{d(x)} LHS = \frac{d}{d(x)} RHS
can be written as an AST:
input:expression
op
  dif
    LHS
    x
  dif
    RHS
    x

AST for Dirac notation

Distinguishing input and output expressions

Some inference rules act on multiple expressions, and some inference rules produce multiple expressions (ie the taking the square root). Here's the AST for "add Eq1 to Eq2":

input:expression:1
op
  LHS:1
  RHS:1

input:expression:2
op
  LHS:2
  RHS:2


output:expression
op
  +
    LHS:1
    LHS:2
  +
    RHS:1
    RHS:2

Complicated expressions as ASTs

Some expressions are more complicated than simply "LHS = RHS". Suppose we have an expression
y = {  x^2   for x>0
    {  0     for x<=0

I don't know how to represent this as an AST. Here's an attempt:

op
  y
  set
    domain
      ^
        x
        2
      >
        x
        0
    domain
      0
      <=
        x
        0


I needed to introduce two new symbols: "set" and "domain"

Related work

Mathlex thesis

http://mathlex.org/doc/how-mathlex-works