Currently every step in the PDG has a set of Latex expressions. These expressions are provided by the user, converted to SymPy, and then the step is validated using SymPy. There is a one-to-one mapping of "what the user sees" to "what the CAS checks."

In a derivation there is a sequence like

f = \int_a^b x dx

*inference rule*: carry out definite integration

f = (x^2/2)|_a^b

*inference rule*: simplify

f = 1/2 (b^2 - a^2)

It seems that SymPy doesn't support the middle expression and instead goes directly from the first to the last expression. That means there is an intermediary Latex expression that cannot be converted to Sympy, breaking the assumption of "what the human reads is one-to-one with what the CAS checks."

Accounting for the mismatch between Latex steps and CAS steps would make the already-messy graph structure more complicated. Some steps that are included for human readability would not be able to be specified to the CAS, nor would those steps be checked.

## No comments:

## Post a Comment