Re: giving exact cases
Jonathan Aldrich
from the Google groups web; I think the email gateway may be overly
sensitive to the exact email address details) but wrote:
> One of the tricky things for people is exactly how to phrase cases.
> I'd rather that sasylf have better error messages about
> (say) "type errors" in cases rather than the ubiquitous error
> about cases being overly specific. I would like students to
> express the cases themselves. Would you agree, Daniel, that there
> is purpose in making the student/user express the case themselves?
Yes, I'd like to get Daniel and others' feedback on exactly this point!
But John, perhaps you could also clarify: by "type error" you mean
essentially that the case does not even typecheck, e.g. it's not even a
valid instance of the rule it claims to be an instance of?
I'd have to look back at the source code to see what checks are being
done, but it seems we could check for that before doing the "overly
specific" check (not sure why we aren't already, actually). I think I
can guess at what this is but as always, if you have a particularly nice
example of where SASyLF could give a better error message, it may help
make sure we get the fix right.
Thanks,
Jonathan
Original message from Jonathan Aldrich:
> ] One of my students is using SASyLF for real research, and found that the
> ] hardest aspect of using SASyLF is coming up with exactly the right cases
> ] in case analysis. I'm sure many SASyLF users feel the same.
> ]
> ] It turns out that in order to check that all cases are present, the tool
> ] has to generate them. So if you are missing one, the tool can
> ] (conceptually) tell you *exactly* what the missing cases are. Should it?
> ]
> ] For a "real" user like my student, the answer is clearly yes. But would
> ] this take away too much of a "learning opportunity" in an educational
> ] context?
> ]
> ] I actually have a kludgey version of this implemented already, but have
> ] not distributed it (beyond the one student) because of this concern.
> ] Let me know what you think.
Daniel Spiewak
> One of the tricky things for people is exactly how to phrase cases.
> I'd rather that sasylf have better error messages about
> (say) "type errors" in cases rather than the ubiquitous error
> about cases being overly specific. I would like students to
> express the cases themselves. Would you agree, Daniel, that there
> is purpose in making the student/user express the case themselves?
Absolutely! I don't think SASyLF should be writing cases for us. I think that all it should do is tell us the rules for which corresponding cases are still lacking. For example, given the following:
syntax
e ::= fn x => e[x]
| e e
| x
// ...
lemma normalizing:
forall e
exists e ->* e' /\ e' value .
_: e ->* e' /\ e' value by induction on e:
case (e1 e2) is
e ->* e' /\ e' value by unproved
end case
end induction
end lemma
SASyLF should complain about "missing cases for syntactic rules 'fn x => e[x]' and 'x'", or something to that effect. Actually, my memory is betraying me now; does SASyLF already do this? It's been a while since I've used it, and I assume things have changed slightly in the meantime.
Either way, I don't think that SASyLF should provide exact information like "missing 'case (fn x => e1[x])'". In other words, it should carefully avoid writing any of the actual proof for the student. It's like the difference between giving a student feedback on an assignment and actually doing parts of the assignment for them.
The one place where this sort of generating might serve to ease some needless frustration is in deeply nested cases. It can become very difficult to tell the difference between t''''''' and t''''''''. But I don't see how SASyLF can actually help in this area without giving too much information at other times. Maybe a separate analysis looking for common, hard-to-trace errors like shadowing?
Daniel
John Boyland
One of the lemmas requires interaction with rule QR-AppAbs (see
TAPL).
We collected a lot of false attempts for the case.
(I have a file with 13 attempts which I will send Jonathan by email.)
It would not have been good had SASyLF given the "answer" right away.
But it's possible that the errors given by SASyLF could be improved.
When I said type erros, I was mistaken. I was talking about a kind
error
on the semantic level, i.e. saying F[X] where F expects a type of kind
K
and X had kind K1. This is not a type error for SASyLF -- the two
kinds could just
be unified. (Maybe SASyLF should not allow unification in this case?)
Best regards,
John