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

[Florian Haftmann]

Hi Jasmin,

>> 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".

To add a further dimension to the design space, there was once the idea
of a generalized primrec in the manner:

1. recursive specification following some pattern considered »primitive«
2. foundational definition of this specification using a suitable
recursion combinator
3. maybe some proof by the user that certain conditions a satisfied
4. deriving the original specification again

A new command »primitive_recursion« would then expose (3) to the user,
whereas the existing »primrec« would assume a trivial proof instead
(similar in appearance like the pair »function« and »fun«)

An example could be something like

primitive_recursion card :: "'a set => nat"
where
  "card {} = 0"
  "card (insert x A) = Suc (card A)"
proof -
  show "!!x y. insert x o insert y = insert y o insert x"
  show "!!x. insert x o insert x = insert x"
qed

thm card.simps -- {*
  "card {} = 0"
  "finite A ==> card (insert x A) = Suc (card A)"
*}

using Finite_Set.fold internally.

Apart from that aside, are separated keywords for primrec and primcorec
really needed, or can they be distinguished just syntactically?

> 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.

Agree.  Such a fundamental replacements needs some time to iron out
properly, before new floors can built on top.

> 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.

I guess (co)primrec(_new) has no problem with performance.  Concerning
datatypes, this is indeed an issue which deserves attention.  We have
still some recdef applications not migrated yet to function due to
performance issues.

Cheers,
	Florian

-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 261 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20130804/1dd118a0/attachment.sig>