In this post I first show that expressions can be represented as abstract syntax trees. Then I show that inference rules are effectively transformations applied to abstract syntax trees.
First I'll illustrate that every expression in the Physics Derivation Graph can be represented as an abstract syntax tree. For example, the expression
a+b = c
would be represented as
An example of an inference rules in the Physics Derivation Graph is, "add 2 to both sides of the expression." In this example the value 2 is a "feed" to the inference rule and the inference rule operates against a single expression.
Writing the inference rule as a function,
<output_expression> = add_x_to_both_sides( <feed value>, <input_expression> )
Applying the inference rule "add 2 to both sides of the expression" yields
The "add __ to both sides of the expression" inference rule essentially means transform input
LHS = RHS
to
LHS + __ = RHS + __
or, in terms of transforming an abstract syntax tree,
Claim: every inference rule can be written as a transform from one abstract syntax tree to another.
