Complete the equation solver

[nrnrnr]

Add enough rules to "ρ; T ⊢ g ⇓ r" so that every possible combination of ρ, T, and g either produces a known outcome or results in a compile-time error.

To express the compile-time error I recommend a new form of judgment that says "this combination of ρ, T, and g cannot be translated into a decision tree." You'll want to come up with a notation.

N.B. It's quite possible you'll get stuck here. In which case getting you unstuck should be top of agenda for our next meeting.

[rogerburtonpatel]

Next on my docket

[rogerburtonpatel]

Working on this now. Note if you're looking at the syntax-judgement docs for #17 : The rules are not done. Just the grammars are ready to present. I'm finishing up the rules today and maybe tomorrow, but maybe not.

[rogerburtonpatel]

I have a first draft, in the rules section here. There are a few rules missing, which I'll tackle tomorrow or at our meeting. Wanted to post now in case you were looking at this in the morning.

Questions:

1. Now that we have the no-decision-tree form, do we need the result metavariable $r$ to capture the possibility of a guarded expression $g$ resulting in no decision tree? Currently, it captures a value produced by evaluating an $\alpha$, denotated $\vartheta$, or reject. Since we have a new conclusion (no-tree-failure) for rules involving guarded expressions, my thought is yes, we would indeed appreciate this third form to reduce cases of a future proof (as we did with $r$).

2. Looking at rules like G-Vcon-Multi-Succ, should the new bindings go before $\mathcal{T}$ and $\mathcal{T}'$ like I have them, or in the middle? My guess is it doesn't matter, so what would you do?

3. Do we need a 'values' section for the grammars? i.e. what expressions evaluate to?

4. In our expression sequence form: $e; g$, if we attempt to evaluate an expression that "doesn't work" (say, 3 > 4), our previous rules said to return the empty sequence of values, indicating failure. However, now that we're in $\alpha$-land, we don't necessarily have an empty value sequence to work with. How do you recommend resolving this conflict? My thought is a fail form that can be represented in both Verse and ML (or any other language which provides an $\alpha$).

5. Rule EqNames-Bot-Fail seems crucial; I came up with it as a way to indicate when we can't make a decision tree from our guarded expression. However, it doesn't have a clear complement, e.g. something that works when $x$ or $y$ appear in $\mathcal{T}$ or $\mathcal{T}'$. I wrote such a rule, it's noted at the bottom of the page. But it looks horrible and its final premise is identical to the first one. Seeing this, I realized like the EqNames-Bot-Fail rule might be missing the mark with the whole "appears in $\mathcal{T}, \mathcal{T}'$" thing. If this isn't a good way to go about it, how do you recommend denoting that an equation is fully stuck and can't be solved further?

6. I kind of feel like a lot of my rule names are horrible. How can I improve them? A better question probably is: What are your heuristics for making good rule names? And if you can't teach them (""they only come with experience""), could you please help rename the ones you think are awful?

Finally, a random thought for the paper is to note the nondeterminism in anything involving $\mathcal{T} \cdot \mathit{eq} \cdot \mathcal{T}'$: we don't specify which equation to pick.

[rogerburtonpatel]

Done.