Published 2020-09-20T21:30:00.006Z by Physics Derivation Graph

As an illustration of the gradations from text to Latex to CAS is provided below. In the derivation the CAS is 1-to-1 with the Latex.

*statement*

Frequency and period are inversely related.

Frequency and period are inversely related; thus T = 1/f and f = 1/T.

*statement with mathematical notation and explanation of derivation*

Frequency and period are inversely related; thus T = 1/f.

Multiple both sides by f, then divide by T to get f = 1/T.

*statement with explanation of derivation, separating expressions from text*

Multiple both sides by f, then divide by T to get f = 1/T.

Frequency and period are inversely related; thus

*statement with expressions separated from text and with bindings between math and text made **explicit*

*expression 1*: T = 1/f.

Multiple both sides of__expression 1__ by f to get __expression 2__

*expression 2*: f T=1

then divide both sides of__expression 2__ by T to get __expression 3__

*expression 3*: f = 1/T.

*statement with inference rules made **explicit*

*claim*: Frequency and period are inversely related; thus*inference rule: *declare initial expression*expression 1*: T = 1/f.

*inference rule: *Multiple both sides of __expression 1__ by f to get __expression 2__

*expression 2*: f T=1

then*inference rule: *divide both sides of __expression 2__ by T to get __expression 3__

*expression 3*: f = 1/T.

*inference rule: *declare final expression

*claim*: Frequency and period are inversely related; thus*inference rule: *declare initial expression*expression 1*: T = 1/f.

*claim*: Frequency and period are inversely related; thus*inference rule: *declare initial expression*expression 1*: T = 1/f.

*inference rule: *divide both sides of __expression 2__ by T to get __expression 3__

*expression 3*: f = 1/T.

*inference rule: *declare final expression

T = 1/f.

Multiple both sides by f to get

f T=1

then divide by T to get

f = 1/T.

Multiple both sides by f to get

f T=1

then divide by T to get

f = 1/T.

Frequency and period are inversely related; thus

Multiple both sides of

then divide both sides of

then

*use of a Computer algebra system to implement inference rules*

The following expansion requires

- conversion of Latex to SymPy
- correctly implemented inference rules

>>> **import sympy**

>>> **from sympy import ***

>>> **from sympy.parsing.latex import parse_latex
**

To confirm consistency of representations, the input Latex expression can be converted to SymPy and then back to Latex using

>>> **latex(eval(sympy.srepr(parse_latex('T = 1/f'))))**

'T = \\frac{1}{f}'

We'll work with the SymPy representation of expression 1,

>>> **sympy.srepr(parse_latex('T = 1/f'))**

"Equality(Symbol('T'), Pow(Symbol('f'), Integer(-1)))"

Rather than using the SymPy, use the raw format of expression 1

>>> **expr1 = parse_latex('T = 1/f')
**

*inference rule: *Multiple both sides of __expression 1__ by f to get __expression 2__*expression 2*: f T=1

Although we can multiply a variable and an expression,

>>> **expr1*Symbol('f')**

f*(Eq(T, 1/f))

what actually needs to happen is first split the expression, then apply the multiplication to both sides

>>> **Equality(expr1.lhs*Symbol('f'), expr1.rhs*Symbol('f'))**

Eq(T*f, 1)

Application of an inference rule (above) results in the desired result, so save that result as the second expression (below).

>>> **expr2 = Equality(expr1.lhs*Symbol('f'), expr1.rhs*Symbol('f'))
**

*inference rule: *divide both sides of __expression 2__ by T to get __expression 3__*expression 3*: f = 1/T.

>>> **Equality(expr2.lhs/Symbol('T'), expr2.rhs/Symbol('T'))**

Eq(f, 1/T)

Again, save that to a variable

>>> **expr3 = Equality(expr2.lhs/Symbol('T'), expr2.rhs/Symbol('T'))**

>>> **latex(expr3)**

'f = \\frac{1}{T}'

*inference rule: *declare final expression

*statement with inference rules** and numeric IDs for symbols*

To relate the above derivation to any other content in the Physics Derivation Graph, replace T and f with numeric IDs unique to "period" and "frequency"

>>> **import sympy**

>>> **from sympy import ***

>>> **from sympy.parsing.latex import parse_latex**

>>> expr1 = parse_latex('T = 1/f')

>>> eval(srepr(expr1).replace('T','pdg9491').replace('f','pdg4201'))

Eq(pdg9491, 1/pdg4201)

Save the result as expression 1

>>> expr1 = eval(srepr(expr1).replace('T','pdg9491').replace('f','pdg4201'))

*inference rule: *Multiple both sides of __expression 1__ by f to get __expression 2__*expression 2*: f T=1

>>> feed = Symbol('f')

>>> feed = eval(srepr(feed).replace('f','pdg4201'))

>>> Equality(expr1.lhs*feed, expr1.rhs*feed)

>>> Equality(expr1.lhs*feed, expr1.rhs*feed)

Eq(pdg4201*pdg9491, 1)

>>> expr2 = Equality(expr1.lhs*feed, expr1.rhs*feed)

>>> feed = Symbol('T')

>>> feed = eval(srepr(feed).replace('T','pdg9491'))

>>> Equality(expr2.lhs/feed, expr2.rhs/feed)

Eq(pdg4201, 1/pdg9491)

>>> expr3 = Equality(expr2.lhs/feed, expr2.rhs/feed)

Convert from numeric ID back to Latex symbols in Latex expression

>>> latex(eval(srepr(expr3).replace('pdg9491','T').replace('pdg4201','f')))

'f = \\frac{1}{T}'

*removal of text, pure Python*

The above steps can be expressed as a Python script with two functions (one for each inference rule)

from sympy import *

from sympy.parsing.latex import parse_latex

# assumptions: the inference rules are correct, the conversion of symbols-to-IDs is correct, the Latex-to-SymPy parsing is correct

def mult_both_sides_by(expr, feed):

return Equality(expr.lhs*feed, expr.rhs*feed)

def divide_both_sides_by(expr, feed):

return Equality(expr.lhs/feed, expr.rhs/feed)

# *inference rule*: declare initial expression

expr1 = parse_latex('T = 1/f')

expr1 = eval(srepr(expr1).replace('T','pdg9491').replace('f','pdg4201'))

feed = Symbol('f')

feed = eval(srepr(feed).replace('f','pdg4201'))

expr2 = mult_both_sides_by(expr1, feed)

feed = Symbol('T')

feed = eval(srepr(feed).replace('T','pdg9491'))

expr3 = divide_both_sides_by(expr2, feed)

latex(eval(

srepr(expr3).replace('pdg9491','T').replace('pdg4201','f')))

# *inference rule*: declare final expression

*How would the rigor of the above be increased?
*

To get beyond what a CAS can verify, a "proof" would relate each of the two functions to a set of axioms. Given the two arguments (an expression, a "feed" value), is the returned value always consistent with some set of axioms?

The set of axioms chosen matters. For example, we could start with Zermeloâ€“Fraenkel set theory

That would leave a significant gap between building up addition and subtraction and getting to calculus and differential equations. "Theorems of calculus derive from the axioms of the real, rational, integer, and natural number systems, as well as set theory." (source)