more checks to perform in the Physics Derivation Graph
Published 2020-05-01T11:16:00.002Z by Physics Derivation Graph
Up until now I've only considered a single check throughout the Physics Derivation Graph: the validation of a derivation step. This validation is made by verifying that changes to the per-expression ASTs are consistent with the inference rule and feeds.
There are other checks that can be performed.
Symbolic consistency within an expression. For a given latex symbol in an expression, there can be only one numeric ID. This could manifest within one side of an expression or across both sides.
If there are multiple instances of "a" on the LHS, are they all the same numeric ID?
Is the symbol "a" used on the LHS the same "a" used on the RHS? For example, in the expression "a + b = a * 2", both "a" symbols must have the same numeric ID.
Symbolic consistency within a step. A step involving more than one expression must have consistent symbols. For example, given "a + b" and the inference rule "add X to both sides" where the feed is 2, the output is "a + 2 = b + 2". Is the "a" in "a + b" the same as the "a" in "a + 2 = b + 2"? Changes of variable are feasible but must be explicit
Symbolic consistency within a derivation. A a given latex symbol has multiple numeric IDs in a derivation, is the change documented in an explicit inference rule or do the two cases not intersect? For example, the symbol "c" could appear as both a constant and a variable in the same derivation, but not in the same step.