teorth / qed Goto Github PK
View Code? Open in Web Editor NEWRepository for the QED interactive text and possible extensions
License: MIT License
Repository for the QED interactive text and possible extensions
License: MIT License
To address an issue raised in the blog, I wanted to suggest an easy way to start adding tests that doesn't require installing or learning to use any tooling (e.g. of the kind that professional software developers normally use).
The purpose would be to address the following comment in the "QED version 2.0: an interactive text in first-order logic" blog post:
But writing this text (particularly the first-order logic sections) has brought me close to the limit of my programming ability, as the number of bugs introduced with each new feature implemented has begun to grow at an alarming rate.
The idea is to add a test.html
file which, when viewed locally, loads and runs a file called test.js
. The test.js
file can contain tests of functions in the other JS files (e.g. functions which are more bug-prone or otherwise difficult to get right). To start out, the tests can be simple, hand-coded assertions that raise or display an error on failure. Helper test functions could be added to facilitate making assertions, and test inputs and corresponding expected outputs could be stored in arrays to make the tests more compact.
If a test framework is later added, the hand-coded tests could be adapted to fit into whatever framework is used.
Reaching exercise 11.1 (through solving exercise 10.1(a)) and clicking A
from the formula window does not give NOT(A)
as one of the options.
Tested in Chrome 69 and reproduced in Edge 25.
It should be 2.10.6
Currently we have to manually create NOT FALSE
from FALSE
just to put it into an environment. Maybe an option to put NOT FALSE
into an environment with just FALSE
can be added separately as a convenience?
This issue is to finish simplifying Exercise
creation in main.js
.
The steps I suggest are--
Finish the exerciseData
mapping in main.js
, which has a structure identical to the lawsData
mapping:
Lines 100 to 103 in 699d583
Add divs of the following form to index.html
: <div class="section" id="section-1">Conjunction introduction</div>
. These section divs should be placed between the appropriate exercise divs inside the exercise-container div, so that the section headers and exercises are in the same order that they currently appear in main.js
:
Lines 123 to 126 in 699d583
Add a new data-law="<lawShortName>"
attribute for the two Exercise objects that use a prior law when being constructed (namely exercises 18.1 and 18.2(b)):
Lines 331 to 335 in 699d583
Change main.js
and the exerciseList.forEach()
loop to iterate instead over the children of the exercise-container div, similar to how the law-container div is now being iterated over:
Lines 70 to 74 in 699d583
newSection()
. And if the child has class "exercise," then call exerciseFromData()
or new Exercise()
, depending on whether the data-law
attribute is set.
I was thinking about how to simplify main.js
further, and the next thing that occurred to me (using the criterion of easiest, biggest win) is to move the base enumeration of laws to index.html
. For the below to work as I'm describing, can all of the Law
objects be instantiated before the first Exercise
objects are created?
If so, a section could be added to the data container element as follows:
<div id="dataContainer">
<div id="lawsContainer">
<div class="law" id="LawConjunction1">
<A HREF="https://en.wikipedia.org/wiki/Conjunction_introduction" target="_blank">CONJUNCTION INTRODUCTION</A>
</div>
...
</div> <!-- End lawsContainer -->
...
</div> <!-- End dataContainer -->
Then, prior to creating the Exercise
objects, main.js
could have a routine that iterates over the law elements in the HTML and instantiates a Law
object for each one.
After that, the JS could loop over an array of triples like the following to set the givens
and conclusion
on each law:
[
["LawConjunction1", [A, B], AND(A,B)],
...,
]
What's nice about this approach is that the HTML declaratively does the bulk of the work (which means less code, which is a good thing), and the JS is minimally responsible for only the part that has to be done in the JS (because of how the givens and conclusion are defined using JS functions).
If this works, something similar can be done for the sections and Exercise
objects within. (Currently, the reverse is happening for the Exercise
objects, with the JS procedurally enumerating the Exercise
objects, and the HTML decorating those objects with the additional info. But the idea would be to reverse those roles along the lines described above for the Law
objects.)
e.g Ex 9.5(a) and (b), Monotonicity of AND/OR: while (A AND C) IMPLIES (B AND C)
is good, often I also want a version that deduces (C AND A) IMPLIES (C AND B)
. Otherwise I'd have to find a way to either invoke a AND is commutative
or (A AND B) IFF (B AND A)
, which is inconvenient and actually hard to do as it's very hard to apply deductions to inner pieces under this system (e.g trying to deduce ((NOT (A IMPLIES B)) OR A) IMPLIES ((NOT ((NOT A) OR B)) OR A)
is just a huge pain.)
More examples:
A IMPLIES (A AND B)
; why not also A IMPLIES (B AND A)
?IMPLIES
: Why I can only make such deductions from an IFF, but not IMPLIES, considering the former is just the two-way version of the latter?(NOT A) AND A
is just as valid as A AND (NOT A)
, I think. No need to restrict the order. (The same goes to excluded middle, with AND
replaced by OR
)If there are only rules that occurred at or after the current exercise and you pressed 'c', "no available deductions" is not showed.
I can already see Existential Instantiation being put on the top of the deductions list when a THERE EXIST
item in an environment is selected.
There are many other things that should go on top though. Lots of deductions, especially in the formula window, applies to all kinds of terms and they clutter the deductions list very quickly if the term is big enough. Meanwhile I'm already struggling to find which item TRUE
/NOT FALSE
is at every single time.
Suggestion:
div
s in the deduction window, separated vertically. Though then the hotkey assignation would have to be revisedI'm pretty sure that if the main page is renamed from QED.html
to index.html
, then it will be accessible using the simpler and more easily publicized URL https://teorth.github.io/QED/
(because of how GitHub Pages is configured).
If this is done, it will require updating some links in the blog, etc. However, a simple HTML redirect page could also be added for people who already have a bookmarks set, etc.
If I open QED webpage using emacs eww browser, it automatically spits out the solutions of all the exercises. It's not that pretty looking though, but it's far more easier to edit it than to solve all the exercises.
On my blog at https://terrytao.wordpress.com/2018/08/18/qed-version-2-0-an-interactive-text-in-first-order-logic/#comment-504372 a commenter expressed interest in localising the software to other languages. I was wondering what would be a good way to do this. Right now the English text portions of the code are split between the javascript portion of the code and the HTML portion. I could see localising the javascript portion by replacing all text strings with variables and then loading a language-specific .js file that sets each variable to the translation of that string in the given language. Not sure how to proceed on the HTML side though.
EDIT: I guess one could place the text portions of the HTML in a separate language-specific file also. But then how would one change languages when viewing the web page?
Has anyone discussed turning this into an iOS app?
The code is free open source so I guess if we want to do that we can just get started?
Thanks very much
Currently the notification window is very useless because it just dumps all the solve status of the exercises. New notifications are also added at the back, so it's guaranteed to be not noticed. Most importantly, they don't actually notify anything. It's more like a "what happened recently" list.
Suggestions:
Sometimes there are just too many intermediate items around and they are cluttering the screen.
Maybe an option to remove (as in, "forget") existing items can be added, like dragging an item to the recycling bin. Of course, this might cause key items to be removed, but then it's a conscious option, and it's always possible to immediate undo/restart the proof anyway so it isn't that much of a big deal.
Syllogism matching rules are not implemented yet as mentioned in Ex22.8 description, but matching rules for every other law related to THERE EXISTS/FOR ALL (aka the entire Chapter 18 and 22) are not implemented either. This makes for some big inconvenience later on, e.g Ex22.6(b) cannot be used on Ex23.2.
Since Exercise.completionMsg
isn't so much related to a particular exercise (and is only used once), the Exercise
class could be simplified slightly by removing Exercise.completionMsg
. Instead, the message could be shown when the number of solved exercises equals one. This is also how completedAllExercises()
is already handled (and also makes sense from the perspective that this is a UX issue around how to interact with the user when solving exercises).
Another thing that could be done with this is to move the message text to a div in the HTML, following the pattern of moving more of the text from Javascript (code) to the HTML (textual content).
One easier thing that I think would improve the structure and maintainability of the code would be to store the HTML "notes" and "proof" for each exercise as HTML.
Currently, these HTML strings are stored as JS string literals (in docs/js/main.js
), which isn't great for storing "data" and makes it a bit harder to edit and view the HTML. For example:
Lines 29 to 30 in 2978fc5
One idea is to store this information in the form of hidden (i.e. not seen when browsing) "data" divs in the main html file. The structure for each exercise could be something like--
<div id="exercise-3">
<div class="notes">...</div>
<div class="proof">...</div>
</div>
Then a load_exercise_data(exercise, id)
JS function could be defined that populates an Exercise
object from the HTML document, and this called from within main.js
for each exercise. Over time, more of the exercise "data" could be transferred to a more structured form (e.g. the "unlocks" and "unlockedBy" information), until perhaps all of each exercise can be populated from data.
It's more helpful to navigate between exercises by going forward/backward instead of just warping into the first/last unsolved exercise. Warping into the first unsolved exercise becomes unhelpful to improving workflow if there is a dangling unsolved exercise behind, as pressing n
no longer warps to the next exercise to which I've just solved (which is what I would usually want), but always that dangling exercise.
Suggested hotkeys: Ctrl+Left/Right
Predicates takes at least one term and produces a formula. Operators takes at least one term and produces another term.
When the amount of them increases (like the new exercises in Chapter 24), it's not easy to tell which of the items in the predicates/operators window are predicates and which are operators. It'd be nice to separate them into two lists.
If you load the page, you'll notice that a bunch of content "flashes" before going away.
I'm guessing this is because the content starts out displayed, and then the JS hides it when first executing. It would be better if it starts out hidden to prevent the flashing.
Exercise 24.8 can be proven within 19 lines using cancellation law [after showing (x * (α * 1)) = (x * α), we can directly apply cancellation law].
DOUBLE DEDUCTION THEOREM Is unlocked by solving 6.2, and 7.1 shortest proof uses DDT, but exercise 7.1 is not dependent on 6.2 for unlock.
Therefore, the shortest solution is impossible for players who jump from 6.1 to 7.1, and the UI gives no indication of why.
Either DDT should be unlocked (silently) by 6.1, or 7.1 should be unlocked by 6.2 instead of 6.1(a)
<div class="exercise" id="EXERCISE-7.1" data-unlocked-by="6.1(a)" data-unlocks="Push PushAlt">
</div>
<ol class="proof">
<li><span>Deduce <em>A</em> [assuming <em>A</em>]. <i>[IMPLICATION INTRODUCTION]</i></span></li>
<li><span>From <em>A</em> [assuming <em>A</em>]: deduce <em>A</em> [assuming <em>A</em>, <em>B</em>]. <i>[PUSH (alternate form)]</i></span></li>
<li><span>From <em>A</em> [assuming <em>A</em>, <em>B</em>]: deduce <em>A</em> IMPLIES (<em>B</em> IMPLIES <em>A</em>). <i>[DOUBLE <a href="https://en.wikipedia.org/wiki/Deduction_theorem" target="_blank">DEDUCTION THEOREM</a>]</i></span></li>
<li><span>QED!</span></li>
Currently these things will not produce duplicates when being created:
New free/bound variable
However, these things will produce duplicates:
Ideally, each of the above should not have duplicates. Doing the same conclusion should be a no-op, and arguably doing a step that reaches a conclusion that already exists should also be a no-op?
It seems that the only to reset an exercise (due exercise content changes) is to either modify the local storage manually, or restart the whole game. It'd be good to have a button to just reset the selected exercise.
For example: click on "A", click "RESTART EXERCISE", ctrl-click "A", 'From formula "A", formula "A"' will be in the "Available deductions".
This HTML validator can be useful for finding HTML typos in index.html, etc:
https://validator.w3.org/
This issue can be used for resolving the various issues that the validator finds. The checkboxes below can be used for recording what the validator finds and what remaining things need to be resolved.
lang="en"
href
value: Illegal character in path segment(I just added a few initial checkbox items after using the validator's "direct input" feature.)
When you have solved many exercises and go back to the non-shortest ones and try to solve them with fewer steps, the "rules occur in the text at or after the current exercise" trouble a lot.
I suggest adding a setting of not showing these rules.
Or does there exist such a setting but I didn't notice it?
Hey Terence,
I'm still halfway through working out the exercises on the old url, is there a way to migrate over to the new page without losing progress?
A declarative, efficient, and flexible JavaScript library for building user interfaces.
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
An Open Source Machine Learning Framework for Everyone
The Web framework for perfectionists with deadlines.
A PHP framework for web artisans
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
Some thing interesting about web. New door for the world.
A server is a program made to process requests and deliver data to clients.
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
Some thing interesting about visualization, use data art
Some thing interesting about game, make everyone happy.
We are working to build community through open source technology. NB: members must have two-factor auth.
Open source projects and samples from Microsoft.
Google ❤️ Open Source for everyone.
Alibaba Open Source for everyone
Data-Driven Documents codes.
China tencent open source team.