Re: [isabelle] "Unfolding" the sum-of-products encoding of datatypes



> When I read "some" I wondered what that means. Experimentally I found:
> 
> datatype t1 = A bool
> ==> size (A True) = 0
> 
> datatype 'a t2 = A 'a
> ==> size (A True) = 1
> 
> I understand why, but I am not convinced this difference in behaviour is beneficial for users of size.

Beneficial as opposed to what? Returning 1 in both cases would be even less compatible (esp. for list), and returning 0 in both cases is -- well -- precisely the old behavior, which doesn't have the nice "foolproof" property mentioned by Andreas, and for which I can easily construct an example like yours above that exhibits an odd difference in behavior (which is even less regular and intelligible). And of course, the old way of doing things required two "primrec" definitions instead of one "primrec" and one simple "definition".

If I could go back in time, I'm still not sure if we would go for 100% compatibility with the old package or for the current scheme, but I would have brought it up for discussion on "isabelle-users". I suspect the outcome of the discussion would have been "don't fix it if it ain't broken".

>> In other words, the old package defined "size" and "size_list" (or rather, back then, "list_size") independently of each other, with some anomalies. IIRC, a constructor like "C 'a" used to count as 0 for "size" (instead of 1 now) and as "1 + f a" (where a is C's argument of type 'a) for "size_list". I thought this was crazy, but experience has shown that the old definition often gave better automation in termination proofs, as the IsaFoR developers discovered when porting their theories to the new package.
> 
> I could have told you that because that is one of the reasons for the old design. Experience, not only doctrine.

I believe you are mistaking lethargy for strategy.

If the old design had been documented in any way, it might have helped me understand it and replicate it. But not only it wasn't documented, the odd behavior looked so much like an oversight (in terms of both behavior and code) that it didn't cross my mind to ask around. Had I realized for one second that there might be a deeper reason for the behavior, I would have not hesitated to bring this up.

If there is a strong consensus in favor of restoring the old behavior, it wouldn't be terribly hard for me to change things to how they used to be. But from what I understand, the porting pains where not very big and are now behind us, and the new behavior is actually useful sometimes (cf. Andreas's solution and Manuel's "foolproof" comment).

Jasmin





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