Sorting with proofs - Githubissues

siddhartha-gadgil / LTS2019

Web page, code for "Logic, Types Spaces 2019" at IISc

http://math.iisc.ac.in/~gadgil/LTS2019/

MIT License

9 stars 13 forks source link

Sorting with proofs #2

Open siddhartha-gadgil opened 5 years ago

siddhartha-gadgil commented 5 years ago

Implement sorting algorithms such as quick sort or merge sort but with proofs, i.e.

Define a Sorted(v) type parametrized by a vector v(the input) that corresponds to
- an output vector
- a proof that the output is sorted
- a proof that the input and output differ by a permutation.
Define sorting algorithms as dependent functions mapping v to Sorted(v)

SS-C4 commented 5 years ago

So do we fork your repository, modify it and send pull requests to include our edits, possibly in a new folder?

siddhartha-gadgil commented 5 years ago

Yes, ideally not in a new folder but just in Code

On Wed, Jan 23, 2019 at 11:00 AM SS-C4 notifications@github.com wrote:

So do we fork your repository, modify it and send pull requests to include our edits, possibly in a new folder?

— You are receiving this because you authored the thread. Reply to this email directly, view it on GitHub https://github.com/siddhartha-gadgil/LTS2019/issues/2#issuecomment-456675565, or mute the thread https://github.com/notifications/unsubscribe-auth/ADatpPVUcN0oKtKggKqZGP4MB7in7eqGks5vF_NpgaJpZM4aOCO2 .

anotherArka commented 5 years ago

Do we sort vectors of natural number or a general ordered type?

siddhartha-gadgil commented 5 years ago

A general ordered type would be best, but should be easy to upgrade from natural numbers.

AR-MA210 commented 5 years ago

Are other sorting algorithms allowed (other than Quick Sort and Merge Sort)?

Also, as the project is collaborative, is it okay to submit code in pieces?

-- Abishek

siddhartha-gadgil commented 5 years ago

Yes, all algorithms are welcome. But a good sorting one like quick sort gets more credit than say insertion sort - though it may be good to start with something simple.

It is good to submit in pieces, but it should be clear how the piece fits in the planned whole.

anotherArka commented 5 years ago

The problem with a general ordered type is we don't always have a proof of the ordering similar to LTE for Nat.

shafilmaheenn commented 5 years ago

Sir, the code that i gave for the merge function was actually wrong. I am really sorry. Can you please remove it

siddhartha-gadgil commented 5 years ago

Just delete it and send a fresh pull request, making sure you pull from my branch before editing.

Regards Siddhartha

On Wed 23 Jan, 2019, 9:00 PM shafilmaheenn, notifications@github.com wrote:

Sir, the code that i gave for the merge function was actually wrong. I am really sorry. Can you please remove it

— You are receiving this because you authored the thread. Reply to this email directly, view it on GitHub https://github.com/siddhartha-gadgil/LTS2019/issues/2#issuecomment-456845657, or mute the thread https://github.com/notifications/unsubscribe-auth/ADatpP_GMaEYZWoMfBi46mTOHnhignZJks5vGIAegaJpZM4aOCO2 .

shafilmaheenn commented 5 years ago

I have corrected the code and sent a new pull request

shafilmaheenn commented 5 years ago

I think that the merge function that I gave doesnt work in linear time as it is supposed to (because of the sillycast function that I had to introduce).Can someone else please confirm this