[isabelle] mergesort (was: BUG in conv.ML: rewr_conv and then_conv fail due to beta-normalization issue)



On 10/23/2012 08:17 PM, Makarius wrote:
(Next time I will tell a story how an efficient and fully verified
merge-sort function included in the core sources caused several days of
worries.)

Please tell the story. I'm particularly interested since in the near future I was going to suggest to run some tests whether it would make sense (performance-wise) to replace the existing sorting algorithm in the Isabelle sources by the one from (sorry for the self-advertisement):

  http://link.springer.com/article/10.1007/s10817-012-9260-7

As I'm writing this email I saw that the current sorting algorithm in src/Pure/library.ML actually already is a very similar mergesort (last time I checked, it wasn't ;)). Just curious: Is there a specific reason for not using the function composition "trick" to avoid 'rev' in 'ascending'?

cheers

chris









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