Use of MathJax for expressions

Now that I've migrated my interface to Flask web page hosted in a Docker container, I could use MathJax to display LaTeX expressions.

http://localhost:5000/list_all_expressions could use MathJax

Automated web interface testing

https://robotframework.org/ is better than Selenium because it produce reports

UML to Python Flask and WTForms

UML to Python Flask and WTForms rather than iterative form development

lesson learned for model-view-controller: form workflows

Model-view-controller (MVC) is a way to separate presentation from the backend computation and data transformation.

For my application, "model" = compute.py; "view" = a collection of webpages; "controller" = controller.py

MVC nuances with Flask and WTForms --

• The business logic workflow is captured exclusively in controller.py
• Upon form submission the workflow should return back to controller.py rather than linking to next page. The controller.py uses redirect(url_for()) to transition between pages.
• Form data extraction occurs in the controller; manipulations to the form data are made in compute.py (the model). 

Using OCaml to identify equivalent expressions

OCaml: simplify expressions to basis for equivalence class
LaTeX --> OCaml AST, then compare against all other OCaml ASTs

Scope is for +, -, * for integers
Next steps would be expand to real, then complex

Use case: find other equivalent expressions

Use case: validation

This requires typed variables (eg int, real, constant, real, complex, matrix, vector

Rules:

• addition rule of equality
• multiplication rule of equality
• substitution property of equality
• associative property
• commutative property
• transitive property
• symmetric property
• additive inverse property

when to use a dropdown menu versus list of links in the web interface

For the web interface, there are multiple pages that have a list from which a user can select. One way to render the list would be a set of hyperlinks; another way would be a dropdown menu.

Suppose the user needs to select an inference rule for a step. They should only chose one, so a dropdown is the preferred method.
--> when the user should be restricted to one option, use a dropdown menu.

Suppose the user is presented with a list of derivations to view. They could chose one or more (to open in new tabs), so a list is the preferred method.
--> when the user can chose one or more options, use a dynamically generated list of hyperlinks.

SQL vs CSV vs PKL for data storage

The CSV files are sufficient to build a proof of concept. Given that sufficiency, and my lack of familiarity with SQL, perhaps I shouldn't focus on using sqlite for the MVP.
(See https://physicsderivationgraph.blogspot.com/2019/12/mvp-for-pdg-with-sql.html)

CSVs feel hacky and don't enable enforcement of consistency checks. However, they are easier to view and decrease the dependencies.

The easiest solution might be using Pickle (PKL) files rather than converting from Python variables in-memory to a distinct off-line representation. A Pickle file is enables consolidation.

mathematical bases for inference rules

"add x to both sides" = addition property of equality
"multiply both sides by x" = multiplication property of equality
"divide both sides by x" = division property of equality

abstract syntax trees for expressions

https://tug.org/TUGboat/tb12-3-4/tb33arnon.pdf

https://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.32.5712&rep=rep1&type=pdf

https://pdfs.semanticscholar.org/7214/d4805660042521d4b825eb3324742b215072.pdf

http://mathlex.org/doc/how-mathlex-works

https://calculem.us/abstract-binding-trees-1/
https://semantic-domain.blogspot.com/2015/03/abstract-binding-trees.html
https://arxiv.org/abs/1601.06298

MVP for PDG with SQL

Currently I have a Docker container that runs flask on Ubuntu to present a web interface that uses forms to enter information.
sandbox/docker_images/flask_ubuntu/web
A Python script on the backend handles conversion from string LaTeX to PNG using dvipng, with graphviz generating the static graph PNG.

The other major component of the backend is an sqlite3 database that holds the data when the container is offline. I don't have experience with SQL, so I need a plan to get to the minimum viable product.

The purpose of the sqlite3 file is to store the multiple tables offline.  I could use a Python Pickle file, but that would be specific to Python; the sqlite approach seems more portable and generic.

The only actions I need are

• write data structure from memory (in Python) to sqlite
• read data structure from sqlite into Python

Summary:
SQL tables <--> Python data structures <--> graph structure <--> graph viz, website generation, UI web


On startup, read data into Python from sqlite.
After that, every time there is a change to the structure in Python, write to sqlite.
This approach is not elegant compared to "write only diff" or "write at end of session" but it eliminates any possibility of inconsistency.
This approach doesn't scale for large databases or multiple users, but those aren't problems I need to solve right now (I'm intentionally incurring technical debt).

If I'm using SQL to store data structures from Python, I'll need to enumerate the table schemas. See
https://allofphysicsgraph.github.io/proofofconcept/site/how_to_build_the_physics_derivation.html
which shows the tables

• per derivation
• edge list (expression local ID to inference local ID)
• expression identifiers (expression ID to local ID)
• feeds (latex to local ID)
• inference rule identifiers (inference rule to local ID)
• global expression latex to expression ID
• global inference rule to latex, description, CAS representation

Reviewing the options described on
https://stackoverflow.com/questions/695752/how-to-design-a-product-table-for-many-kinds-of-product-where-each-product-has-m
I don't know which is applicable.

Motives for SQLite use:

• enforce column consistency (each row has N columns)
• enforce column types (e.g., string, integer)
• enforce entry length (e.g., local ID must be an integer with M digits)

SQLite options

From the perspective of file management, having one file feels cleaner than a file per derivation. 

5 tables in 1 SQLite file

One option is to implement 5 table schemas:

• expression latex to expression ID. Columns:
• expression_latex (string)
• expression ID (integer)
• inference rule to latex, description, CAS representation
• inference rule (string)
• inference rule latex (string)
• inference rule description (string)
• CAS representation (string)
• derivation edges. Columns:
• derivation name (string)
• from local ID (integer)
• to local ID (integer)
• derivation feeds. Columns:
• derivation name (string)
• latex (string)
• local ID (integer)
• derivation expressions. Columns:
• derivation name (string)
• expression ID (integer)
• local ID (integer)
• derivation inference rules. Columns:
• derivation name (string)
• inference rule (string)
• local ID (integer)

I suspect this layout of tables is suboptimal -- having the "derivation name" repeating in a column is an indicator that the table count should be 2+3*D to eliminate duplication (rather than 5). This 2+3*D (where "D" is the number of derivations) design is also apparent in the "dict of derivations" structure described below. My motive for using 5 is that if I use 2+3*D, the table names are not static.

2+3*D tables in 1 SQLite file

Two tables are independent of derivations:

• expression latex to expression ID. Columns:
• expression_latex (string)
• expression ID (integer)
• inference rule to latex, description, CAS representation
• inference rule (string)
• inference rule latex (string)
• inference rule description (string)
• CAS representation (string)

And 3 tables are needed per derivation. Problem with this is that the name of the tables isn't known in advance.

2 tables in 1 SQLite file; 3 tables in D SQLite files

Same as previous option, except instead of a single SQLite file, the derivations are in separate files.

SQLite to Python

These tables in SQL are equivalently stored in Python as three data structures:

• list of inference rules = [{'inf rule':'inf rule 1','in':1, 'out': 0},{'inf rule':'inf rule 2', 'in':2, 'out': 3}]
• list of expressions = [{'expr 1':59285924, 'expr 2': 954849, 'expr 3': 948299}]
• dict of derivations = {'derivation name 1':[<step1>, <step2>, <step3>]}

where each <step> has the structure 

{'inf rule': 'this inf rule', 

input: [{'expr local ID': 942, 'expr ID': 59285924}], 

output: [{'expr local ID': 218, 'expr ID': 954849}]}