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".
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"