semantic-math / math-rules

Manipulate math-ast ASTs based on algebraic rules
MIT License
4 stars 1 forks source link

Learning the fundamentals of PRESS using MathPiper #14

Closed tkosan closed 7 years ago

tkosan commented 7 years ago

@kevinbarabash and @aliang8 the first two modules in the materials I am putting together on MathPiper and PRESS are ready:

Module 1: Installing MathPiperIDE

Module 2: MathPiperIDE Worksheets

One needs to know a bit about using the procedural parts of MathPiper before moving on to learning its rewrite rule parts. I have been teaching the procedural parts of MathPiper to incoming freshman since 2008, and some of these procedural parts are what are presented in these modules. One goal I have for MathPiper is to eventually have it compete with other programming languages as a beginner's first language.

Feel free to ask questions if you have them.

tkosan commented 7 years ago

The second two modules are now available:

Module 3: Parsing And The Language Of Expression Trees

Module 4: Tree Pattern Matching And Transformation Rules

These worksheets can be copied and pasted into MathPiperIDE if you would like to play with them. However, you will need update to version .953 of MathPiperIDE, and save the files with a .mpws extension.

kevinbarabash commented 7 years ago

@tkosan thanks for putting all these materials together. I'll have a look at them over the weekend.

kevinbarabash commented 7 years ago

What freshman course do you use MathPiper in?

I'm curious how paths are used in rewrite rules.

Is PRESS the same PRESS described in https://www.era.lib.ed.ac.uk/bitstream/handle/1842/4475/BundyA_Solving%20symbolic%20equations%20with%20PRESS.pdf?sequence=1&isAllowed=y?

tkosan commented 7 years ago

What freshman course do you use MathPiper in?

One of my goals for MathPiper is for it to be the first CAS programming language that has been specifically designed to meet the needs of K-12 education. Since 2008 I have been using MathPiper in an introduction to programming class that incoming freshman take. I have also had some local high school teachers teach this course in their schools. Since I am currently the primary user of MathPiper, I have had the luxury of being able to heavily modifying it each year in a non-backwards compatible way so that it better meets the above goal.

Each assignment and exam I give out is in the form of a worksheet that contains a number of programming problems. Each problem has a %mathpiper_grade fold below it that analyzes the student's program and then provides immediate feedback on it. This is an assignment from earlier in the course:

Assignment example 1

and this is an assignment from later in the course:

Assignment example 2: Plotting points

If you would like to play with these worksheets, just paste them into MathPiper and save them with a .mpws extension. Note1: If you right click in a worksheet then select Remove Unpreserved Folds, all output folds will be removed from the worksheet. Note 2: The GeoGebra plugin on the right side of the application needs to be opened at least once during a session to enable plotting of points.



I'm curious how paths are used in rewrite rules.

Using paths for equation solving are a concept that comes from the PRESS research, and they are used at the meta-level for making meta-level inferences about the tree. The implementation of PRESS that is currently in MathPiper uses procedural code for meta-level inferences instead of rewrite rules. The code that does the meta-level inference will be shown in the next module.

In the meantime, I am currently working on including paths in the explanations that the solver generates, and if you evaluate the following code in the MathPiper console, an explanation will be displayed that contains the beginnings of paths explanations:

In> Symbols(x)

In> Show(StepsView(SolveSteps(MathParse("−20 = −4 x − 6 x"), x), ShowTree:True, ShowPositions:False, ShowRuleName:True, ShowRule:True, Scale:1.7, Code:False, FullParentheses:True))



Is PRESS the same PRESS described in

Yes, that is it. Dr. Bundy still teaches at the University of Edinburgh. A few years ago I updated the PRESS source code to work on a modern implementation of Prolog, and Dr. Bundy placed this updated version on GitHub. I had to teach myself Lisp to work with MathPiper, and I had to teach myself Prolog to work with PRESS. I found Prolog to be much much harder to learn than Lisp was.

An interesting thing about PRESS is that for a while it was the largest Prolog program in the world. Another interesting thing about PRESS is a later version called Learning PRESS is able to automatically learn the rules that are used to solve a given equation if it is given a worked-out solution to this equation.

kevinbarabash commented 7 years ago

It sounds like it's finding more using in programming classes than math classes. Is that correct?

I had a look at the assignment examples. The programming challenges on khanacademy.org use similar techniques for checking student work. The checkers are rather laborious to write unfortunately.

I started looking at the PRESS source code by I don't know Prolog. I should need to read through the PRESS article I posted when I have more time.

I don't see math-rules itself implementing any sort of solving system. I see that being built on top of math-rules in mathsteps or other solving libraries that people may want to write using math-rules.

tkosan commented 7 years ago

It sounds like it's finding more using in programming classes than math classes. Is that correct?

Currently its finding more use in programming classes because I am a faculty member in a Computer Engineering Technology degree, and I don't have permission to teach math in the classes I teach. However, the language should also be effective in math classes.

I had a look at the assignment examples. The programming challenges on khanacademy.org use similar techniques for checking student work. The checkers are rather laborious to write unfortunately.

Since MathPiper's checking code is written in MathPiper and included in the assignment worksheets where it's easily accessible, I am hoping people will be able start writing their own testing code soon after they become comfortable with the fundamentals of the language. So instead of a small number of skilled programmers writing laborious checking code, this work could be spread out over a larger number of less skilled programmers.

The AI research from the 70s and 80s also shows how to synthesize programs that meet specified constraints, and I am hoping to use this research to either enable MathPiper to automatically generate checking code for a given program, or to automatically generate a program from a given set of checks.

tkosan commented 7 years ago

@kevinbarabash the final module that explains the fundamentals of how PRESS works should be posted by Monday evening.

tkosan commented 7 years ago

@kevinbarabash the last module (which explains the fundamentals of PRESS's approach to solving equations) is now available:

Module 5: The Hidden Rules That Are Used To Solve Elementary Algebra Equations

The MathPiper SolveSteps procedure is a general-purpose step-by-step equation solver that is based on PRESS. It obtains its object-level rules from a rule database, and the following is the current elementary algebra rulebase that contains rules that were inspired by the ones in PRESS:

SolveSteps Rules

This is the source code to SolveSteps itself:

SolveSteps Source code

I just made a new release of MathPiperIDE (v.954), and it includes documentation on most of the procedures that are used in SolveSteps.

I am convinced that someday the PRESS research will completely revolutionize the way K-16 mathematics is taught.