[isabelle-dev] Redundant equations in function declarations

[Lawrence Paulson]

I may as well be a bit more explicit. About seven Cambridge MPhil students were given an assignment that included converting the following ML code into HOL and proving theorems about it.

fun nnf (Atom a) = Atom a
  | nnf (Neg (Atom a)) = Neg (Atom a)
  | nnf (Neg (Neg p)) = nnf p
  | nnf (Neg (Conj(p,q))) = nnf (Disj(Neg p, Neg q))
  | nnf (Neg (Disj(p,q))) = nnf (Conj(Neg p, Neg q))
  | nnf (Conj(p,q)) = Conj(nnf p, nnf q)
  | nnf (Disj(p,q)) = Disj(nnf p, nnf q);

fun distrib (p, Conj(q,r)) = Conj(distrib(p,q), distrib(p,r))
  | distrib (Conj(q,r), p) = Conj(distrib(q,p), distrib(r,p))
  | distrib (p, q) = Disj(p,q)  

fun cnf (Conj(p,q)) = Conj (cnf p, cnf q)
  | cnf (Disj(p,q)) = distrib (cnf p, cnf q)
  | cnf p = p  

Nearly half of the students moved the “catchall" lines from the last position to the first, for reasons I cannot fathom. At least one discovered that annoying termination issues in the function nnf could be fixed by inserting the line

  | nnf (Neg p) = Neg (nnf a)

near the top. None of the students were stupid, but they were rushed due to the impact of other deadlines, and were desperate to get their definitions past the system. Moreover, I didn't notice all of these errors myself until I actually executed their examples. I don't need to elaborate the effect these errors had on the rest of the assignments. Which were worth 50% of their course grade.

I don't think underlining would make much difference, because people are already used to ignoring underlined material in Microsoft Word.

Larry

On 3 Jun 2012, at 20:29, Alexander Krauss wrote:

>> Thank you for investigating. I have been waiting for Alex to present his view.
> 
> Sorry for being late. I've been offline for some days and am a bit behind now :-)
> 
>> Naturally, the current treatment resembles ML's.
> 
> Yes. I don't think there were any further considerations.
> 
> [...]
>> There is no reason to allow a specification to contain material that may contradict another part of the specification.
> 
> Well, the meaning of an equation in the "fun" command is: If the equation overlaps with a previous one, consider just the non-overlapping part. And your proposed change would be an exception to this rule.
> 
> It does not happen very often, but I have occasionally written thing like this myself in intermediate experimentation stages. Eventually, I clean things up of course, but having a hard error would force me to comment out more stuff temporarily...
> 
> But I understand your concerns.
> 
> Technically, this situation represents a recoverable error (the definition and the rest of the theory can be processed), but always indicates a problem in the sources that should be fixed. It seems that we do not currently have a corresponding severity level. Therefore choosing between "ignored spam warning" and "break your leg error" is a bit difficult.
> 
> Questions:
> 
> - Do we need a level for such messages/annotations? In IDE terms, a little yellow triangle with an exclamation mark comes to my mind. I wouldn't want to see this for most iother warnings, but here it might make sense.
> 
> - @Larry: Do you think your students would have noticed it if the redundant equations had been underlined in yellow?
> 
> - @Makarius: Is it already possible for a package to emit a message/report that carries position information, say to underline one of the clauses in a specification processed by read_specification? This could also improve the error reporting in other cases.
> 
> Alex
> 
>