Re: [isabelle] Proof of concept: BNF-based records



> It is presently unclear to me, where the scalability features are used
> in practice. If L4.verified no longer requires that, we can probably
> remove 80% of the record package and then update it easily. If scalable
> records are still required, it will need more work to update.
> 
> Can some Data61 people say more about their current applications of the
> record package?

We still do require it, and in fact make more use of the scalability than ever, because seL4 keeps growing and we keep adding support for further architectures.

We also depend on extensibility of records in a few places.


>> Looking for your input on whether this is useful, and whether it belongs
>> into HOL-Library, the AFP, or the bin.
> 
> Spontaneously, I would have said HOL-ex or the bin. By putting it in
> HOL-Library, you make certain claims of quality and sustained
> maintenance. I.e. the first posting I can imagine on isabelle-users:
> 
> "I've found out about HOL-Library.Datatype_Records by accident -- there
> is no NEWS entry and no documentation whatsoever. That tool appears to
> be in conflict with the existing record package. Can anybody please fix
> this ASAP, such that I can use theories with regular records together
> with these new BNF records? Anyway, what is the roadmap? Can I expect
> new BNF records will eventually supersede old-fashioned typedef records?”

:-)

I must admit that we have been maintaining a similar (very bare-bones) additional datatype record package on the side for about a decade. We use it in addition to the standard record package to model C structs, because they can contain recursive pointer types, which we couldn’t do with normal records. I.e. it might make sense to have both, as long as it is clear what each is for, what the differences are, and why they can’t/shouldn’t be the same.


>> The longer reason: there are more problems with records, e.g. there is
>> no support for nested recursion (they do not constitute BNFs), and even
>> "copy_bnf" can't fix the absence of a suitable "size" function (which
>> makes termination proofs impossible).
> 
> Can you explain this further? Is there an inherent problem of the
> general idea of the regular record package wrt. BNFs? Can the BNF
> experts comment on that?

I’d be interested in that too. It’d be nice to properly localise and BNF-ify records eventually.

Cheers,
Gerwin


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.