8 ms·

Functional Algorithms, Verified

dwohnitmok 5y ago
This is really cool! Seeing more examples of formal verification in the wild is always exciting for me. I'm slightly let down by how they are formally proving time complexity bounds. I was excited because proving performance bounds is a pretty tough nut to crack, but looking through the sort algorithms (and their overview in Section 1.5) it looks like they don't prove the runtime of the function directly. Rather they create a whole new cost function, assert without proof that the cost function accurately represents the original function, and then prove that the cost function has certain bounds. I would be interested to hear if anyone has experience with formal verification frameworks that can be used to prove time and space complexity bounds of arbitrary code.
- 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 ago
    Yeah 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 ago
      Concrete 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 ago
        I'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 ago
        I’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.
- tomsmeding 5y ago
  Try playing with Why3. http://why3.lri.fr/ http://why3.lri.fr/ It's slightly idiosyncratic, and it has its own programming language that is ML-like. But it allows you to write arbitrary code in that language, and then prove statements about that code using SMT solvers as helpers. I haven't used it in practice yet, just played with an example, but it felt quite powerful if you get to know its capabilities.
  - dwohnitmok 5y ago
    I haven't used Why3, but I have used other SMT solver-based frameworks such as Dafny and TLAPS for TLA+ and they all seem focused on proving function behavior, rather than function runtime or memory usage. I suspect there's a way to encode runtime and memory usage theorems, but I don't have a clear conception of the best way of doing so without polluting function definitions.
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 ago
  This is not Haskell. Everything is implemented in Isabelle/HOL.
- amw-zero 5y ago
  From 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.
mjfl 5y ago
"Functional Algorithms" is a strange topic for me since algorithms seem very imperative, compared to the declarative nature of FP.
- kadoban 5y ago
  If you're into the idea, I'd recommend Purely Functional Data Structures by Okasaki and Pearls of Functional Algorithm Design by Bird, both really interesting books IMO.
  - nextos 5y ago
    Bird's book and its prequel, Thinking Functionally with Haskell, are outstanding. His approach of calculating algorithms by performing algebraic transformations is very interesting. It attracted some interest during the 80s and 90s, but it has faded away as it's too tough to be followed by a human. I wonder if it could benefit from some automation by using e.g. modern synthesis techniques.
- amw-zero 5y ago
  Computation is the creation of and executing of algorithms. Even if an algorithm is expressed functionally, it progresses through a sequence of states when executed. Check out Computation and State Machines by Leslie Lamport: https://lamport.azurewebsites.net/pubs/state-machine.pdf https://lamport.azurewebsites.net/pubs/state-machine.pdf. Specifically, in Section 3, he shows how interactive and recursive definitions of the same program are actually executing the same underlying algorithm, even though their source code looks drastically different. Syntax is superficial, and declarativeness is really just an illusion, or maybe a convenience. But, a program is executing a sequence of states no matter what paradigm it’s expressed in. Functional programs are still executed. In this respect, you’re talking about a very superficial aspect of algorithms.
  - benlivengood 5y ago
    Additionally lambda calculus, general recursive functions, combinatorial logic, Turing machines, and a number of other systems are equivalently powerful[0] and so any computable function can be expressed in any of the systems. So it's fine to refer either to purely functional algorithms or purely state-machine algorithms since they are equivalent statements. [0] https://en.m.wikipedia.org/wiki/Church%E2%80%93Turing_thesis https://en.m.wikipedia.org/wiki/Church%E2%80%93Turing_thesis
tubby12345 5y ago
Maybe someone here knows: is there a standard transformation from sequential logic to combinational logic? I'm thinking something like that immediately gives me the 3sat representation of an algorithm that has an iteration step.
- pkhuong 5y ago
  Loop unrolling.
  - tubby12345 5y ago
    That only works if there are no branches
- benlivengood 5y ago
  3sat is not Turing-complete since every 3sat problem is finite but Turing machines have infinite tapes. Combinatory logic[0] is Turing-complete but combinational logic[1] is not for the same reason. [0] https://en.m.wikipedia.org/wiki/Combinatory_logic https://en.m.wikipedia.org/wiki/Combinatory_logic [1] https://en.m.wikipedia.org/wiki/Combinational_logic https://en.m.wikipedia.org/wiki/Combinational_logic
  - tubby12345 5y ago
    Ya you're right I've confused complexity with universality. But actually it's not there actually exist TMs with infinitely long tapes so actually my question still makes some kind of sense - how do I express a finite program (that I constrain to not loop infinitely) as a boolean or combinational circuit.
    - cybernautique 5y ago
      My understanding is that you don't get a choice. You either allow loops, and accept that they might go infinite, or you axe them altogether. I believe this is a direct corollary of the halting problem, but please correct me if I'm wrong.
the_only_law 5y ago
How does one learn and get involved with formal verification outside academia? What sort of mathematical background is required. I always get lost with pure functional languages and the related subjects, even in the introductory material. Though I’ve been able to understand the usefulness of both some functional concepts (through playing with various impure languages like F# or Erlang) and of formal verification (from looking at SPARK with Ada) but all the notation and vocabulary and such of languages like Isabelle’s HOL and Idris confuse me. I even find myself lost among Scala developers.
- amautertt 5y ago
  I am further along in the journey, I have been learning formal verification/type theory and logic on my own. I think these two are excellent books, SF : Logical Foundations for the basics, SF: Verified Functional Algorithms. Unfortunately there is no royal road in type theory. This subject is incredibly demanding yet satisfying. Software foundations are excellent books to read even if you aren't interested in verification/program proof.
- cybernautique 5y ago
  My advice: swing wide. If you don't know where to start, then judge a book by its cover and read it until you hit a knowledge gap, then slither down that gap and keep digging for resources until you either get bored or achieve something. I recommend starting with geometric algebra or topology. The aspiring selfstarter has a bevy of great options. Sidney A. Morris' "Topology Without Tears" is fine androgogy, as is the widely-acclaimed undergrad textbook "Intro to Topology: Pure and Applied" by Colin Adams. The biggest thing, in my opinion, is to realize that there are precious few things you need permission to think, mathematically. The fundamental mathematical advantage is abstraction. If you can manage your abstractions and approach the math as nothing more than especially pedantic philosophy- it helps.
  - jhanschoo 5y ago
    I'm sorry, how is geometric algebra and basic topology even relevant to formal verification? Your suggestions sound more related to your own interests. The commenter is better served browsing through some introductory formal verification material like Concrete Semantics by one of the same authors as the linked document.
amautertt 5y ago
If you are already familiar with Coq or even Ocaml/Haskell style programming. I really believe, the volume 3 of SF series is a more polished and more approachable book. https://softwarefoundations.cis.upenn.edu/vfa-current/index.html https://softwarefoundations.cis.upenn.edu/vfa-current/index.... I am halfway through the first book (doing ALL exercises), I hope by next year end I would really like to finish vol 3. This Isabelle books seems to cover more ground though.
Zababa 5y ago
Small fact about Isabelle: that's where the pipeline operator |> comes from. Here's a post about it with a few sources: http://mamememo.blogspot.com/2019/06/a-brief-history-of-pipeline-operator.html http://mamememo.blogspot.com/2019/06/a-brief-history-of-pipe... "also" isn't an excellent name for it, but I like the idea of giving names to operators instead of using things like >>=, <$>, <*>. I have a hard time reading code with it, as I always pause to think "okay, how should I read that?". I wonder if that's something you get used to, or a difference in how people think.

This is really cool! Seeing more examples of formal verification in the wild is always exciting for me. I'm slightly let down by how they are formally proving time complexity bounds. I was excited because proving performance bounds is a pretty tough nut to crack, but looking through the sort algorithms (and their overview in Section 1.5) it looks like they don't prove the runtime of the function directly. Rather they create a whole new cost function, assert without proof that the cost function accurately represents the original function, and then prove that the cost function has certain bounds. I would be interested to hear if anyone has experience with formal verification frameworks that can be used to prove time and space complexity bounds of arbitrary code.

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 ago
  Yeah 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 ago
    Concrete 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 ago
      I'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 ago
      I’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.
tomsmeding 5y ago
Try playing with Why3. http://why3.lri.fr/ http://why3.lri.fr/ It's slightly idiosyncratic, and it has its own programming language that is ML-like. But it allows you to write arbitrary code in that language, and then prove statements about that code using SMT solvers as helpers. I haven't used it in practice yet, just played with an example, but it felt quite powerful if you get to know its capabilities.
- dwohnitmok 5y ago
  I haven't used Why3, but I have used other SMT solver-based frameworks such as Dafny and TLAPS for TLA+ and they all seem focused on proving function behavior, rather than function runtime or memory usage. I suspect there's a way to encode runtime and memory usage theorems, but I don't have a clear conception of the best way of doing so without polluting function definitions.

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 ago
This is not Haskell. Everything is implemented in Isabelle/HOL.
amw-zero 5y ago
From 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.

mjfl 5y ago

"Functional Algorithms" is a strange topic for me since algorithms seem very imperative, compared to the declarative nature of FP.

kadoban 5y ago
If you're into the idea, I'd recommend Purely Functional Data Structures by Okasaki and Pearls of Functional Algorithm Design by Bird, both really interesting books IMO.
- nextos 5y ago
  Bird's book and its prequel, Thinking Functionally with Haskell, are outstanding. His approach of calculating algorithms by performing algebraic transformations is very interesting. It attracted some interest during the 80s and 90s, but it has faded away as it's too tough to be followed by a human. I wonder if it could benefit from some automation by using e.g. modern synthesis techniques.
amw-zero 5y ago
Computation is the creation of and executing of algorithms. Even if an algorithm is expressed functionally, it progresses through a sequence of states when executed. Check out Computation and State Machines by Leslie Lamport: https://lamport.azurewebsites.net/pubs/state-machine.pdf https://lamport.azurewebsites.net/pubs/state-machine.pdf. Specifically, in Section 3, he shows how interactive and recursive definitions of the same program are actually executing the same underlying algorithm, even though their source code looks drastically different. Syntax is superficial, and declarativeness is really just an illusion, or maybe a convenience. But, a program is executing a sequence of states no matter what paradigm it’s expressed in. Functional programs are still executed. In this respect, you’re talking about a very superficial aspect of algorithms.
- benlivengood 5y ago
  Additionally lambda calculus, general recursive functions, combinatorial logic, Turing machines, and a number of other systems are equivalently powerful[0] and so any computable function can be expressed in any of the systems. So it's fine to refer either to purely functional algorithms or purely state-machine algorithms since they are equivalent statements. [0] https://en.m.wikipedia.org/wiki/Church%E2%80%93Turing_thesis https://en.m.wikipedia.org/wiki/Church%E2%80%93Turing_thesis

tubby12345 5y ago

Maybe someone here knows: is there a standard transformation from sequential logic to combinational logic? I'm thinking something like that immediately gives me the 3sat representation of an algorithm that has an iteration step.

pkhuong 5y ago
Loop unrolling.
- tubby12345 5y ago
  That only works if there are no branches
benlivengood 5y ago
3sat is not Turing-complete since every 3sat problem is finite but Turing machines have infinite tapes. Combinatory logic[0] is Turing-complete but combinational logic[1] is not for the same reason. [0] https://en.m.wikipedia.org/wiki/Combinatory_logic https://en.m.wikipedia.org/wiki/Combinatory_logic [1] https://en.m.wikipedia.org/wiki/Combinational_logic https://en.m.wikipedia.org/wiki/Combinational_logic
- tubby12345 5y ago
  Ya you're right I've confused complexity with universality. But actually it's not there actually exist TMs with infinitely long tapes so actually my question still makes some kind of sense - how do I express a finite program (that I constrain to not loop infinitely) as a boolean or combinational circuit.
  - cybernautique 5y ago
    My understanding is that you don't get a choice. You either allow loops, and accept that they might go infinite, or you axe them altogether. I believe this is a direct corollary of the halting problem, but please correct me if I'm wrong.

the_only_law 5y ago

How does one learn and get involved with formal verification outside academia? What sort of mathematical background is required. I always get lost with pure functional languages and the related subjects, even in the introductory material. Though I’ve been able to understand the usefulness of both some functional concepts (through playing with various impure languages like F# or Erlang) and of formal verification (from looking at SPARK with Ada) but all the notation and vocabulary and such of languages like Isabelle’s HOL and Idris confuse me. I even find myself lost among Scala developers.

amautertt 5y ago
I am further along in the journey, I have been learning formal verification/type theory and logic on my own. I think these two are excellent books, SF : Logical Foundations for the basics, SF: Verified Functional Algorithms. Unfortunately there is no royal road in type theory. This subject is incredibly demanding yet satisfying. Software foundations are excellent books to read even if you aren't interested in verification/program proof.
cybernautique 5y ago
My advice: swing wide. If you don't know where to start, then judge a book by its cover and read it until you hit a knowledge gap, then slither down that gap and keep digging for resources until you either get bored or achieve something. I recommend starting with geometric algebra or topology. The aspiring selfstarter has a bevy of great options. Sidney A. Morris' "Topology Without Tears" is fine androgogy, as is the widely-acclaimed undergrad textbook "Intro to Topology: Pure and Applied" by Colin Adams. The biggest thing, in my opinion, is to realize that there are precious few things you need permission to think, mathematically. The fundamental mathematical advantage is abstraction. If you can manage your abstractions and approach the math as nothing more than especially pedantic philosophy- it helps.
- jhanschoo 5y ago
  I'm sorry, how is geometric algebra and basic topology even relevant to formal verification? Your suggestions sound more related to your own interests. The commenter is better served browsing through some introductory formal verification material like Concrete Semantics by one of the same authors as the linked document.

amautertt 5y ago

If you are already familiar with Coq or even Ocaml/Haskell style programming. I really believe, the volume 3 of SF series is a more polished and more approachable book. https://softwarefoundations.cis.upenn.edu/vfa-current/index.html https://softwarefoundations.cis.upenn.edu/vfa-current/index.... I am halfway through the first book (doing ALL exercises), I hope by next year end I would really like to finish vol 3. This Isabelle books seems to cover more ground though.

Zababa 5y ago

Small fact about Isabelle: that's where the pipeline operator |> comes from. Here's a post about it with a few sources: http://mamememo.blogspot.com/2019/06/a-brief-history-of-pipeline-operator.html http://mamememo.blogspot.com/2019/06/a-brief-history-of-pipe... "also" isn't an excellent name for it, but I like the idea of giving names to operators instead of using things like >>=, <$>, <*>. I have a hard time reading code with it, as I always pause to think "okay, how should I read that?". I wonder if that's something you get used to, or a difference in how people think.