Open poser3 opened 10 years ago
poser3
commented
10 years ago As we consider substitution of one variable for another, we will need variables to be able to be marked as "free" or "bound" -- with substitution handled differently in each case. See the book "Introduction to Metamathematics" by S.C. Kleene, Section 18, Example 5 for a good discussion of why this will be needed... (Lee, the book referenced is the one you got last year for the Oxford Math award).
poser3
commented
10 years ago More random thoughts... with regard to the "free" or "bound" business -- this needs to be handled by the Operators class, as the operators are the things doing the "binding". Also, we need a way to "define" a (previously unused) variable to be equal to some expression of our choosing (possibly connected to the drawables, but not necessarily so), and a way to define a new statement in terms of other ones. In the simplest example, the statement a != b can be defined as !(a==b). For something slightly more complicated, a > b can be defined by "There exists some c > 0, such that a = b + c". We'll need the ability to move back and forth between the defined and the definition (i.e., if we have one in our statement list or in some expression, we can add a statement where it has been replaced with the other).
poser3
commented
10 years ago A follow-up thought...
Some of these "definitions" should be as "permanent/internalized" as theorems (maybe in their own file? ..maybe treat them as a special type of theorem?) -- but we need to allow the user to make his own (possibly temporary) definitions too, and allow him or her to be able to add those new definitions to our internal list of definitions and/or theorems (for one reason -- this will help us from hard-coding too many things later).
lee-vian
commented
10 years ago Definitions-as-theorems works okay. If definitions are just a special subset of the theorems, then we could just make new .thm files for definitions as we reach them (theorems are already one-per-file, look in /res/theorems/ for examples). We could also put definitions in their own list, where they would be like theorems, but, with the knowledge that definitions are equivalences and not just implications, we could save some time by being able to apply each definition in either direction. The existing theorem framework and file format would work for this.
As for user-defined definitions, we need to keep in mind that anything that lets users define new symbols (operators) will require some Java to govern those operators' behavior. The default implementations in Operator.java (for example, Operator.toLatex()) are as general as I could make them at the time, but we could create a dialog to choose between some of the more common notations used for operators. Anything more complicated would have to be recompiled (you would have to leave Prove-It, do some Java programming, and rebuild Prove-It). If we have to, I suppose we could embed an interpreted language like Python or Ruby (look into Jython or JRuby to see how this works) and use that to process some of the operator methods.
When theorems or definitions introduce new bound variables (such as the c in your a>b example), we don't want them to conflict with the names of existing variables. We could use the label maker, or similar logic, to generate new variable names that aren't already free elsewhere.
lee-vian
commented
10 years ago Regarding the names of variables, the Expression parser is already fairly lenient. A variable name must: (1) not contain any spaces, (2) not contain any parentheses, and (3) cause BigDecimal's String constructor to throw a NumberFormatException (which means that a variable name cannot look like a number). Since most LaTeX strings that might reasonably be used as variable names already meet these criteria and all expressions (including variable names) are shown to the user as LaTeX, using LaTeX in variable names is already supported, as an accidental but fortuitous consequence of the way I wrote the parser so long ago. The biggest obstacle is figuring out how to deal with backslashes, which both Java and LaTeX use to start escape sequences. I'll do some testing with Java's text boxes to see if I can't work this out.
It would be nice to a variable constructor mechanism, similar to the sketch canvas so we weren't limited to a-z vars. Perhaps internally, use vars x1, x2, x3, ... and give each var a tex-based "label" so we could have mu, sigma, etc... in our statements. This may necessitate a panel or dialog for selecting/adding vars. This might provided a much needed link for the measurements of various structures in the Sketch canvas too... This may also help with the application of theorems/axioms like the reflexive property. I need to think more about this, but those are some of my thoughts...