abstract syntax trees and inference rules

The Physics Derivation Graph is composed of inference rules and mathematical expressions. Inference rules describe how to get from one expression to another.

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.