[Coq-Club] Proving bounds on data structures in Coq?

[Siddharth Bhat]

Hello,

I was interested in implementing data structures from Okasaki's "purely
functional data structures", but I'm not sure how to actually *prove* theorems
about the amortized analysis -- in terms of the banker's method /
physicist's method, while still being able to extract such a data structure
out to Haskell code.

So, TL;DR:
How do I define data structures in Coq such that it is:
1. Extractable to code
2. Allows reasoning to prove bounds using Okasaki's methods?

Thanks,
~Siddharth

[Xuanrui Qi]

Hello Siddharth,

In general, to prove things about complexity, you would define a cost
semantics, i.e. a recursive running function that defines time costs.
Then you'd prove your desired complexity properties against that.

Here's a recent paper about formalizing and proving amortized
complexity in a theorem prover (but Isabelle, not Coq): "Amortized
Complexity Verified", by Tobias Nipkow, in ITP '15 (
http://isabelle.in.tum.de/~nipkow/pubs/itp15.pdf).

Also, for something in Coq, there's Arthur Charguéraud and François
Pottier's 2017 JAR paper, "Verifying the Correctness and Amortized
Complexity of a Union-Find Implementation in Separation Logic with Time
Credits". Those might be helpful.

I'm not an expert in cost semantics, so this is just to get you
started. I suppose the list knows much more about the specifics of
functional cost analysis.

-Ray
--
Xuanrui "Ray" Qi

Department of Computer Science
Tufts University
Halligan Hall, 161 College Ave
Medford, MA 02144, USA

Post by Siddharth Bhat
Hello,
I was interested in implementing data structures from Okasaki's
"purely functional data structures", but I'm not sure how to actually
prove theorems about the amortized analysis -- in terms of the
banker's method / physicist's method, while still being able to
extract such a data structure out to Haskell code.
1. Extractable to code
2. Allows reasoning to prove bounds using Okasaki's methods?
Thanks,
~Siddharth
--
Sending this from my phone, please excuse any typos!

[Robby Findler]

You might also be interested in our paper:

A Coq Library For Internal Verification of Running-Times
McCarthy, Fetscher, New, Feltey, Findler
Science of Computer Programming (SCP) 2018
https://www.eecs.northwestern.edu/~robby/pubs/papers/scp2018-mfnff.pdf

There are some other good papers that are worth checking out described
in the related work section, too.

(It actually was first at FLOPS in 2016; Elsevier took a surprisingly
long time to publish the revised version.)

Robby

Post by Xuanrui Qi
Hello Siddharth,
In general, to prove things about complexity, you would define a cost
semantics, i.e. a recursive running function that defines time costs.
Then you'd prove your desired complexity properties against that.
Here's a recent paper about formalizing and proving amortized
complexity in a theorem prover (but Isabelle, not Coq): "Amortized
Complexity Verified", by Tobias Nipkow, in ITP '15 (
http://isabelle.in.tum.de/~nipkow/pubs/itp15.pdf).
Also, for something in Coq, there's Arthur Charguéraud and François
Pottier's 2017 JAR paper, "Verifying the Correctness and Amortized
Complexity of a Union-Find Implementation in Separation Logic with Time
Credits". Those might be helpful.
I'm not an expert in cost semantics, so this is just to get you
started. I suppose the list knows much more about the specifics of
functional cost analysis.
-Ray
--
Xuanrui "Ray" Qi
Department of Computer Science
Tufts University
Halligan Hall, 161 College Ave
Medford, MA 02144, USA

Post by Siddharth Bhat
Hello,
I was interested in implementing data structures from Okasaki's
"purely functional data structures", but I'm not sure how to actually
prove theorems about the amortized analysis -- in terms of the
banker's method / physicist's method, while still being able to
extract such a data structure out to Haskell code.
1. Extractable to code
2. Allows reasoning to prove bounds using Okasaki's methods?
Thanks,
~Siddharth
--
Sending this from my phone, please excuse any typos!

[Siddharth Bhat]

Thanks, both of those look like excellent references :)

Cheers,
~Siddharth

Post by Robby Findler
A Coq Library For Internal Verification of Running-Times
McCarthy, Fetscher, New, Feltey, Findler
Science of Computer Programming (SCP) 2018
https://www.eecs.northwestern.edu/~robby/pubs/papers/scp2018-mfnff.pdf
There are some other good papers that are worth checking out described
in the related work section, too.
(It actually was first at FLOPS in 2016; Elsevier took a surprisingly
long time to publish the revised version.)
Robby

Post by Xuanrui Qi
Hello Siddharth,
In general, to prove things about complexity, you would define a cost
semantics, i.e. a recursive running function that defines time costs.
Then you'd prove your desired complexity properties against that.
Here's a recent paper about formalizing and proving amortized
complexity in a theorem prover (but Isabelle, not Coq): "Amortized
Complexity Verified", by Tobias Nipkow, in ITP '15 (
http://isabelle.in.tum.de/~nipkow/pubs/itp15.pdf).
Also, for something in Coq, there's Arthur Charguéraud and François
Pottier's 2017 JAR paper, "Verifying the Correctness and Amortized
Complexity of a Union-Find Implementation in Separation Logic with Time
Credits". Those might be helpful.
I'm not an expert in cost semantics, so this is just to get you
started. I suppose the list knows much more about the specifics of
functional cost analysis.
-Ray
--
Xuanrui "Ray" Qi
Department of Computer Science
Tufts University
Halligan Hall, 161 College Ave
Medford, MA 02144, USA

Post by Siddharth Bhat
Hello,
I was interested in implementing data structures from Okasaki's
"purely functional data structures", but I'm not sure how to actually
prove theorems about the amortized analysis -- in terms of the
banker's method / physicist's method, while still being able to
extract such a data structure out to Haskell code.
1. Extractable to code
2. Allows reasoning to prove bounds using Okasaki's methods?
Thanks,
~Siddharth
--
Sending this from my phone, please excuse any typos!

[mukesh tiwari]

Hi Siddhart,
You can see quicksort's average case complexity [1], and annotating
complexity in type system TiML [2] [3].

Best,
Mukesh

[1] https://github.com/Eelis/qs-avg
[2] https://dl.acm.org/citation.cfm?id=3133903
[3] https://github.com/mit-plv/timl

Post by Siddharth Bhat
Thanks, both of those look like excellent references :)
Cheers,
~Siddharth

Post by Robby Findler
A Coq Library For Internal Verification of Running-Times
McCarthy, Fetscher, New, Feltey, Findler
Science of Computer Programming (SCP) 2018
https://www.eecs.northwestern.edu/~robby/pubs/papers/scp2018-mfnff.pdf
There are some other good papers that are worth checking out described
in the related work section, too.
(It actually was first at FLOPS in 2016; Elsevier took a surprisingly
long time to publish the revised version.)
Robby

Post by Xuanrui Qi
Hello Siddharth,
In general, to prove things about complexity, you would define a cost
semantics, i.e. a recursive running function that defines time costs.
Then you'd prove your desired complexity properties against that.
Here's a recent paper about formalizing and proving amortized
complexity in a theorem prover (but Isabelle, not Coq): "Amortized
Complexity Verified", by Tobias Nipkow, in ITP '15 (
http://isabelle.in.tum.de/~nipkow/pubs/itp15.pdf).
Also, for something in Coq, there's Arthur Charguéraud and François
Pottier's 2017 JAR paper, "Verifying the Correctness and Amortized
Complexity of a Union-Find Implementation in Separation Logic with Time
Credits". Those might be helpful.
I'm not an expert in cost semantics, so this is just to get you
started. I suppose the list knows much more about the specifics of
functional cost analysis.
-Ray
--
Xuanrui "Ray" Qi
Department of Computer Science
Tufts University
Halligan Hall, 161 College Ave
Medford, MA 02144, USA

Post by Siddharth Bhat
Hello,
I was interested in implementing data structures from Okasaki's
"purely functional data structures", but I'm not sure how to actually
prove theorems about the amortized analysis -- in terms of the
banker's method / physicist's method, while still being able to
extract such a data structure out to Haskell code.
1. Extractable to code
2. Allows reasoning to prove bounds using Okasaki's methods?
Thanks,
~Siddharth
--
Sending this from my phone, please excuse any typos!

--
Sending this from my phone, please excuse any typos!