Wednesday, May 25, 2016

addressing the rendering versus verifiability challenge

For the Physics Derivation Graph, the primary output is visual. Thus rendering expressions should be beautiful. Latex is a natural choice and the entry is intuitive and straightforward.

In addition to rendering, the other task is to verify that the content is correct. This means using a computer algebra system (ie Mathematica, Octave). Latex is not amenable to CAS input because Latex can be mathematically ambiguous -- resolution depends on context.

One way to resolve this would be to stick with Latex, then convert to a CAS format for verifying correctness.

Sage

As an example, suppose I want to check that the expression "multbothsidesby" was correctly entered for input T/f=1, output T=f, with feed f. The Sage syntax looks like

T,f=var('T,f')
input_expr = T/f==1
expected_output_expr= T==f
expected_output_expr == input_expr*f

The above Sage returns true, building confidence that the step is valid. More simply,

T,f=var('T,f')
(T==f) == ((T/f==1)*f)

If Latex is to be used as the input, then we need to convert it to Sage syntax.
  • declare each variable in Sage
  • replace "=" in Latex with "=="
  • convert the inference rule to something that can be checked
In addition to using a Sage notebook (https://cloud.sagemath.com), there's a one-time eval option -- http://sagecell.sagemath.org/
Calling a local installation of Sage is possible from Python, see http://ask.sagemath.org/question/8215/using-sage-in-a-python-cgi-script/

No comments:

Post a Comment