[isabelle-dev] New (Co)datatypes: Status & Plan (FYI)

[Jasmin Blanchette]

Am 01.08.2013 um 18:15 schrieb Makarius <makarius at sketis.net>:

>> Another important missing piece is "primcorec".
> 
> What is the proper technical term for that?  Isn't it just "corec"?

If the proper name for "primrec" is "primrec", then the proper name for this is "primcorec".

I wouldn't mind killing the "prim" -- after all, the recursor constants are just called "_rec" -- but that's an orthogonal question. Another alternative: "prim_rec" and "prim_corec".

The corecursive counterpart to "fun", corecursion up-to, is something Andrei urges us to work on, but where Dmitry and I are applying the brakes because of the pile of work that remains to be done on the new (co)datatype package before we can consider adding such nice features. In fact, inspired by Leino et al.'s (co)recursion mixture in Dafny [*], Andrei has some ideas to support some recursion in conjuction with corecursion up-to.

Also related to the new (co)datatypes: Larry pointed out in private that my email to the mailing list didn't mention performance (compared with the old package). Performance is generally decent, but we're fighting with n-way mutual recursive defitions where n >= 8. This is certainly solvable by changing the LFP construction, and perhaps Brian's simplifications, which we haven't incorporated yet, would solve this; but until this is addressed, we cannot realistically hope to dislodge the old package. This goes to show once again how challenging (but also rewarding) package writing can be.

Jasmin

[*] which is so powerful it is possible to prove that the stream [7, 7, ...] equals the stream [8, 8, ...] (from which it is trivial to derive False). See http://rise4fun.com/Dafny/HcSLn, click the play button, and check that it says "Dafny program verifier finished with 4 verified, 0 errors". A fixed version of Dafny should be released soon.