3 ms·
Seems the implementation is Haskell, would've been much cleaner in Ocaml. Appearently it's a grad coruse in functional algorithms but can't even see the time-co
by cupofcoffee 5y ago
Seems the implementation is Haskell, would've been much cleaner in Ocaml. Appearently it's a grad coruse in functional algorithms but can't even see the time-complexity analysis of heapify.
- nextos 5y agoThis is not Haskell. Everything is implemented in Isabelle/HOL.
- amw-zero 5y agoFrom section 1.1: > The programs in this book are written in Isabelle’s functional programming language From what I can tell, Binomial Heaps also have a runtime analysis. Not sure what you’re referring to with “heapify.” I would encourage others to ignore this snide comment. I have read other books from the authors, particularly Concrete Semantics, and it’s honestly incredible what can be achieved with Isabelle. Obviously it’s not going to be interesting if formal verification isn’t your thing, but if it is, the content is priceless.