3 ms·
A typical way to prove an algorithm uses less than N steps is include N as a "fuel" parameter to the algorithm and decrement it by 1 at each recursive call, so
by throwaway81523 5y ago
A typical way to prove an algorithm uses less than N steps is include N as a "fuel" parameter to the algorithm and decrement it by 1 at each recursive call, so if N reaches 0 then the algorithm has run "out of gas" so it fails. Then you need some proof terms to verify that N never reaches 0.
Space complexity is different and functional programming historically hasn't paid such close attention to it, since running out of memory can be seen as an external event like a hardware crash. In other words, idk ;).
You might also like Concrete Semantics, a related book: http://concrete-semantics.org/ http://concrete-semantics.org/
- dwohnitmok 5y agoYeah I've heard of the fuel param (although I've only ever used fuel params as a hack to brute force "prove" termination). I'm interested in whether there are frameworks that don't require you to change the function signature. I've skimmed (very very quickly) through Concrete Semantics in the past, but never actually sat down to read it. Does it have anything on proving time or space complexity?
- throwaway81523 5y agoConcrete Semantics is yet another book that looks very good that I want to read someday but haven't. So I don't know if it says anything about either time or space complexity. I believe I learned about using a fuel parameter in an old Edward Yang blog post (http://ezyang.com/ http://ezyang.com/) but I don't have a direct link. Jeff Okasaki's well known book "Purely Functional Data Structures" (highly recommended) does some complexity analyses of operations on functional data structures. They're not formalized but maybe they could be.
- nextos 5y agoI've read and worked through Concrete Semantics and I cannot recall any complexity proofs. It's mostly about program semantics, static analysis, abstract interpretation and type/effect systems.
- amw-zero 5y agoI’m finishing up Concrete Semantics right now. No mention of time complexity that I saw, but even without that it’s become one of my top programming books of all time.