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