[Boards: 3 / a / aco / adv / an / asp / b / biz / c / cgl / ck / cm / co / d / diy / e / fa / fit / g / gd / gif / h / hc / his / hm / hr / i / ic / int / jp / k / lgbt / lit / m / mlp / mu / n / news / o / out / p / po / pol / qa / r / r9k / s / s4s / sci / soc / sp / t / tg / toy / trash / trv / tv / u / v / vg / vp / vr / w / wg / wsg / wsr / x / y ] [Home]
4chanarchives logo
Prove that bubble sort is correct. Can you do it /g/? If not,
Images are sometimes not shown due to bandwidth/network limitations. Refreshing the page usually helps.

You are currently reading a thread in /g/ - Technology

Thread replies: 175
Thread images: 12
File: CMjGO.jpg (94 KB, 941x582) Image search: [Google]
CMjGO.jpg
94 KB, 941x582
Prove that bubble sort is correct.

Can you do it /g/? If not, put that CS degree in the trash.
>>
>>50774884
Joke is on you, I don't have a CS degree.
>>
>>50774884
i could give you a hand-wavey one. i don't want to write out all the tex right now
>>
How?
>>
>>50774884
Do your own homework
>>
>>50774884
why would you want to do this?
>>
>>50775125
Why would you want to know your algorithm is correct?
>>
>>50775306
because other people have already done it
>>
>>50775306
anon you can just run some test cases

proving your algorithm is actually quite useless
>>
>>50774884
http://web.cs.ucla.edu/~pouchet/lectures/doc/888.11.algo.6.pdf
>>
>>50775328
What if you're trying to solve new problems instead of being a code monkey?

>>50775329
That's going to take way longer.
>>
>>50775363
>That's going to take way longer.

unless you dual majored in math/CS it would take quite a bit of time to prove your algorithm.

test cases take 10 minutes maximum per algorithm. is this too much time?
>>
File: 1443899611842.png (111 KB, 500x482) Image search: [Google]
1443899611842.png
111 KB, 500x482
>never bothered learning sorting algorithms because I'm not a poo-to-the-loo shitskin codemonkey
>>
>>50774884
1. assume worst case
2. show each iteration of bubble sort can do no worse than the last
3. some other stuff, i forgot
4. QED
>>
>>50774884

Just because an algorithm is mathematically correct doesn't mean it's any good.

Also

This right here, being able to prove an algorithm, means that CS /is/ a math degree, contrary to what code-monkeys and /g/ denizens writing HTML every day claim with their "hurr, you don't need math to code".
>>
>>50775407
rather be skinks code monkey (btw I'm whtite and handsome) than a toad whom thinks he can code all on his own, lMfao
>>
File: Zig Zag Man_small.jpg (23 KB, 250x415) Image search: [Google]
Zig Zag Man_small.jpg
23 KB, 250x415
>>50775446
i can write hello world without knowing 1 + 1.

hurrr durrrr no math needed.
>>
>>50775485
What if you have to code fizzbuzz?
>>
File: 1423103901262.gif (219 KB, 899x455) Image search: [Google]
1423103901262.gif
219 KB, 899x455
>>50774884
>>
>>50775407
Algorithm implementation is the codemonkest of codemonkey tasks. People in senior roles never do it.
>>
>>50774884
http://www.cs.cornell.edu/courses/cs482/2007su/exchange.pdf
do that thing
>>
>>50775407
>never bothered LEARNING
All information is useful.
>>
Hey guys, OP is such a retard that he posted this same thread in /p/.

>>>/p/2684025
>>
>>50774884
N = 1 -> trivial.
N = n -> either n > n-1 and is already ordered, or n < n-1 and it is swapped with n. QED.
>>
>>50775626
Nice meme :^)
>>
>>50775672
534261 -> 534216

Not sorted
>>
>>50775742
That's not how bubblesort works, tard. I can't believe you're literally so dumb you can't read a 2-line proof on bubblesort right.
>>
>>50775800
Your proof implies that would sort it
>>
>>50774884
I haven't programmed anything since graduating
>>
>>50775700

lolwut
>>
>>50776046
Fine, I'll spoonfeed you since you're clearly too retarded to even breathe. Wouldn't want you to kill yourself from the effort it would take you to think this through.
Bubble sort works like this:
for (i from 0 below size(list))
for (j from 0 below size(list))
if (list[i] < list[j])
let tmp = list[i];
list[i] = list[j];
list[j] = tmp;
end;
end;
end;

Hence, case 2b degrades to itself (with n = n-1) where the rest of the list is already sorted by construction, hence the proof is sound.
>>
>proving something proved billions of times in the history of mankind
>kek
that's something for first year faggots
adults just do the hand wave and say "o yea, it's like dat"
>>
Please tell me this thread is a fucking joke. If you use bubblesort for ANY set of data you deserve to be fired.

PLEASE PLEASE PLEASE use quicksort and mergesort for any remotely large dataset and insertion sort for everything else.
>>
>>50777159
What about heapsort
>>
>>50776046
>what is proof by induction
>>
>>50774884
>If not, put that CS degree in the trash.
Joke's on you, I'm dropping out this Wednesday.
>>
>>50777422
If you're already working with a heap.....then go for it, but in general heapsort would lose out to mergesort due to the need to construct the heap which will cost you an expensive O (n) operations
>>
>>50776994
Your pseudocode is wrong, and your proof is still wrong

The proof would be correct for insertion sort though but bubble sort never guarantees a sorted sublist before the pivot
>>
>>50777159
No one says you should use it.

You should be able to prove a simple algorithm is correct though. Also you should combine a simpler algorithm such as insertion sort into quicksort to sort small subarrays
>>
>>50774884
>CS degree

shit dude I'm a junior in my CS minor right now let's chill out
>>
>>50777696
It's wrong even if you know what it's called
>>
File: tumblr_n4plt7G7JY1tao282o1_1280.jpg (349 KB, 1200x930) Image search: [Google]
tumblr_n4plt7G7JY1tao282o1_1280.jpg
349 KB, 1200x930
programming music thread

https://www.youtube.com/watch?v=nNQdorTq3bs
>>
>>50778017
ops, well how about we derail this shit thread?
>>
>>50777935
Both are correct. Come back when you graduate middleschool.
>>
>>50777935
What the fuck are you talking about? There's no pivot in bubble sort.
>>
>>50774884
The first iteration "bubbles" the maximum element to the rightside of the array, obviously. (call this *)

Induction over the length of the array:
n = 1: its sorted
n -> n+1: use *, remaining list (besides the maximum, which is already at its position) is only n elements long. Use induction hypotheses + the insight that the last index won't be swapped)

qed
>>
>>50775362
Is this actually a formal proof? It just reads like a reiteration of the algorithm in natural language/english.
>>
>>50778095
assuming all list elements are pairwise different. If not, change all "...the maximum..." to "...a maximal element..."
>>
>>50778071
Pivot=The current element being compared.

Let's say you have n sorted like this:
1 2 3 4 5

Let's add another so you get n+1:
1 2 3 4 5 0

Now we do the swap as you said:
1 2 3 4 0 5

Obviously not sorted. If you swap it multiple times until you get to the right place you're just doing insertion sort.
>>
>>50778060
>middle school
This isn't Beijing, you fag.
>>
>>50774884
>put that CS degree in the trash
you mean where it belongs?
>>
>>50778140
You are dumber than a 5 years-old.
>>
>>50778123
I think this proof is okay. It doesn't get much more formal in most undergraduate algorithm lectures. The invariant technique is quite illustrative and powerful.
>>
>>50778178
Says the guy who can't tell the difference between bubble and insertion sort.
>>
>>50778196
9/10 if troll, -5/10 if retarded.
>>
>>50775329
>just run some test cases
>proving your algorithm is actually quite useless
k

http://www.envisage-project.eu/proving-android-java-and-python-sorting-algorithm-is-broken-and-how-to-fix-it/
>>
>>50778196
A pivot is usually fixed during a iteration of the sorting algorithm/partitioning procedure. In Bubblesort you could say that the partitioning is the "bubbling" of a currently maximal element in the current sublist to the right side. But the "pivot" as you call it, might change during this procedure. Hence the name "pivot" is not really applicable in this scenario.
>>
>>50778095
this
>>
>>50775442
Sounds like you're talking about the complexity and not about correctness. Back 2 skul, kiddo
>>
You never dd formal correctness proofs of algorithms in 99.9% of jobs you're going to get with a CS degree.

The remaining 0.1% they would call in a someone with a math phd to do the proofs.
>>
>>50778277
If you say so, rajeesh.
>>
For the retards who can't into induction here's a correct inductive proof: http://math.stackexchange.com/questions/1046848/prove-correctness-of-algorithm-using-induction
>>
>>50778123
>Is this actually a formal proof?
Yes. Look up Hoare logic.

>It just reads like a reiteration of the algorithm in natural language/english.
It's not. It asserts the truth of some predicate that holds between all iterations of the loop. The predicate in this case is "the array is partially sorted". The proof shows that the modifications done by the loop don't break this assumption. It obviously has to walk through the steps of the algorithm to do so, but it contains more information than the algorithm itself, namely the invariant and associated proof steps.
>>
>>50778511
i.e. literally the same proof as the previous two proofs itt.
>>
>>50778511
see
>>50778095
>>
File: 1328112474161.png (37 KB, 679x852) Image search: [Google]
1328112474161.png
37 KB, 679x852
by inductionn on n, assuming we aren't morons unable to swap, anyway you can prove the swap until ordered by induction aswell

n=2
swapping them if the first is > second makes them orderered, root of induction done

assuming n' <n true
i can order the n-1 length subvector since bubblesort is correct for n'<n, after that i have a n length vector where the last member is not ordered, and proced by swapping until it's ordered

rip
>>
>>50778603
Not this one
>>50775672
It never talks about the largest elements going anywhere. It seems to talk about n elements instead of iterations.
>>
File: preorder my game.jpg (25 KB, 500x303) Image search: [Google]
preorder my game.jpg
25 KB, 500x303
>>50774884
>unironically using O(n^2) sorts
>>
>>50774884
What the fuck is that picture talking about?

I know what a Bubble Sort is, and I know how it works.

The fuck does that picture mean, though?

Mind you, I don't have a CS degree. I took some programming classes and plan to take some more. But I can't make heads or fucking tails of that picture.
>>
>>50778809
>What the fuck is that picture talking about?
Square root of 2 is irrational.
>>
>>50775558
merge sort best
>>
>>50778746
I see you have brain problems. Cool.
>>
>>50778809
It's math.
>>
>>50778825
Ok, so what is the picture trying to do?
>>
>>50778835
The proof is ambiguous at best
>>
>>50775558
https://www.youtube.com/watch?v=kPRA0W1kECg
>>
>>50778848
Sorry, misread it. It's talking about how the sets of rationals approximating sqrt(2) is unbounded. Probably from a discussion about why the supremum property is needed to construct the reals. In this case the supremum property shows that sqrt(2) exists.
>>
>tfw cs degree
forgot 75% of this shit.
too bad my job is mostly perl and bash scripts
>>
>>50775404
in most algorithms it woud take you infinite time to test all cases, so that's quite a lot of time
>>
>>50778936
>unbounded.
Agh. "Has no least upper bound", I mean.
>>
>>50778936
Oh.... k.... yeah idk what that means.

I'm not that into Maths.
>>
>>50778648
That one is correct
>>
>>50778957
>my job is mostly perl and bash scripts
I'm so sorry.

Anyway, what really matters is whether you once understood them. Usually it's not something you can come up with by yourself if you don't remember anything. The point is you'll understand the same shit easier next time.
>>
>>50775672
What if n = n - 1?
>>
>>50779090
Impossible, n can't be equal to n-1
>>
>>50779090
Then it doesn't matter which you choose, of course.
>>
>>50779106
A[N] == A[N-1]
>>
>mfw CS fags think they know math
nope.avi

Get a proper degree in electrical engineering and then come back.
>>
>>50779129
oh, you meant that with n = n-1. Just define bubblesort in a way that two equal elements aren't swapped.
>>
>>50779152
we just know how to do linear algebra and proofs
>>
>>50779216
Linear algebra is best math
>>
>>50779090
Then 0=1
>>
>>50777159

>ANY set of data

Using a complex algorithm for small sets of data is retarded, jesus christ I never realized what kind of code monkeys CS students are.
>>
>>50779303
There's no reason to use bubblesort when insertion sort exists.
>>
>>50777159

>quicksort and mergesort
>look mom i just learned babby's second and third algorithm

Protip: there are much better alternatives
>>
>>50779152
>mfw EE doesn't even do 1/10th of the math that CS does
>>
>>50779234
Absolutely correct
>>
>>50778095
This isn't using induction to prove anything, it just describes the sort procedure recursively in a very backwards manner

The n+1 case pretty much says "put biggest element last and then sort the list in front of the last element"
>>
>>50779361
implying
>>
>>50779383
What are people this dumb doing on /g/ again, /g/?
>>
>>50779361
This. Engineers do a few courses calculus without proofs and some basic linear algebra, perhaps some probability. Perhaps some simple complex analysis and Fourier series.
>>
>>50779409
At least use proper English when calling somebody dumb

Anyway, what's wrong with the statement?
>>
>>50779348

it adds no relevant benefit compared to bubblesort in small sets of data, doesnt matter which you use
>>
>>50779430
It does though. It is relevant when it is run over hundreds of small lists such as when it is used as a part of quicksort.
>>
>>50778833

Heap sort is faster though.
>>
>>50778976
In order to prove things about a mathematical object, you first have to define exactly what it is, in a way that anyone can follow and get (mostly) the same idea as you about that object. One of the driving forces during the 19th century (when math started to be properly formalized) was to define even the most simple notions in these exact terms. For example numbers.

This is a rough sketch of how the various sets of numbers are defined:
Natural numbers (0, 1, 2, ...). Their existence can be taken as an axiom. Alternatively, you can start with more basic notions and construct them from there.
Integers (..., -2, -1, 0, 1, 2, ...). Constructed using "codings" with natural numbers.
Rational numbers (fractions, positive and negative). Constructed using "codings" with integerrs
Real numbers (Ï€, sqrt(2), etc. The numbers you use for calculus). Constructed with "approximations" using infinitely many rational numbers.

The picture talks about how to perform the last step in the special case sqrt(2). You can read a (poorly written) discussion of it here: https://en.wikipedia.org/wiki/Dedekind_cut#Construction_of_the_real_numbers

It's 11pm and I can't into words, but I hope this makes at least a bit of sense to you. Pick up a first year math book if you are interested. It's all explained there.
>>
>>50775672
This proof is basically worthless unless one is familiar with what you are talking about. It isn't clear at all what you mean or what n refers to (iterations? elements?).
>>
>>50775485
>Programming is Computer Science
>>
>>50779383
Of course it is by induction, "...sort the list in front..." is the invocation of the induction hypothesis. Correctness for bubblesort is trivial, thats why the induction proof is trivial.
>>
>>50779418
>simple complex analysis
Yeah, no. The most difficult math courses I took were not from calculus or related courses. It was from Digital Analysis Systems and Discret Time Analysis in which you need to uses Z Transforms, Lagrange and Fourier.

So, we take "simple" complex analysis courses?. No

Next time, lurk more.
>>
>>50779566
But did you solve any triple integrals?
>>
>>50778886
https://www.youtube.com/watch?v=lyZQPjUT5B4
>>
How the fuck radix sort works.
>>
File: 1428778562885.png (444 KB, 617x548) Image search: [Google]
1428778562885.png
444 KB, 617x548
>>50779566
>in which you need to uses Z Transforms, Lagrange and Fourier.
Anon...
>>
>>50779557
Is it though? To prove the n -> n+1 case you would have to do something to prove that in general if you have a list of n that can be sorted, a list of n+1 can be sorted. So the hypothesis would be that "a list of n can be sorted". It's not really handling those questions.
>>
>>50779582
Yes, we take all the calculus courses.

Also, all the physics around electromagnetism (Maxwell equations) can be solved with triple and double integrals. But we resort to the differential forms most of the time.
>>
>>50779723
Sure it is. We perform one iteration of bubblesort, i.e. we put a maximal element of our list of n+1 elements to the right side of the array (this is *). A (unsorted) list of n elements remains (everything to the left of the maximal element, which we just put in its right place). Since we know that bubblesort is correct on inputs of length n, we invoke the induction hypothesis for the remaining list.
>>
File: slide_2.jpg (96 KB, 960x720) Image search: [Google]
slide_2.jpg
96 KB, 960x720
>>50779758
Forgot image
>>
>>50779495
It's nobody's fault that you're retarded.
>>
>>50779723
I think you have to additionally prove that if the list of n+1 has as its last element some element that's not bigger than its predecessors in the list of n, the sorting procedure will put the last element in its correct place without disturbing the ordering of the rest of the list
>>
>>50779786
Ok but it's your fault your proofs are shit-tier.
>>
>>50779800
the ordering of the rest of the list is not important as it will be handled AFTER a current maximal element (of the n+1 elements) is put in its right place.
>>
>>50779766
It's just saying in English the procedure:
bubblesort list =
let max = maximum list
let maxRemoved = delete max list
bubblesort maxRemoved ++ max


I don't think it's enough proof or else all valid Haskell programs would be proven by default
>>
>>50779868
That's not at all how bubblesort works, tard.
>>
>>50779882
this tbh
>>
>>50779868
The procedure you just described isn't bubblesort. Your procedure is a trivially correct sorting procedure, also called selectionsort. The argument I made, is that the correctness argument of bubblesort can be reduced to the correctness argument of selectionsort.
>>
>>50779882
Excuse me, friend. Doesn't bubblesort essentially move the biggest element of the list last, then the second biggest to the second last index, etc? Because that's what the code does exactly.
>>
>>50779976
You must have single-digit IQ.
>>
>>50775363
>What if you're trying to solve new problems instead of being a code monkey?
Oh, you mean reading a white paper and implementing something the writer doesn't have the ability to? :^)
>>
>>50779976
>implying insertion sort = bubble sort = selection sort
>>
>>50779925
>the correctness argument of bubblesort can be reduced to the correctness argument of selectionsort.
Well that seems to be true if you think about it abstractly enough. That's a the case for a lot of sorting algorithms, they can be thought of as specific examples of more general ones. But still, I'm kinda feeling we're still missing a proof that would please a mathematician.
>>
>>50775363
>What if you're trying to solve new problems instead of being a code monkey?
proving bubbleshit is correct is not a new problem, it's a waste of time
>>
>>50780014
>>50779996

>>50778095 is describing the algorithm that way. Put largest element last and do the same for the preceding list. Are you saying it doesn't or what?
>>
File: fizzbuzz.webm (265 KB, 486x500) Image search: [Google]
fizzbuzz.webm
265 KB, 486x500
>>50775536
>>
>>50780016
I have a math minor and am pleased with the proof.
>>
>>50779774
>not without muh formula sheet!

please
>>
>>50780016
>I'm kinda feeling we're still missing a proof that would please a mathematician.
I'm a master's in math, and no.

Unless you want to talk about the operational semantics of whatever language you're using to describe your algorithm or something, in which case I don't give a fuck.
>>
>>50780065
>minor
I have a math minor and I'm not
>>
>>50780091
Guess I'll have to give in

What I've been missing is something that really does directly prove "assuming a list of n can be sorted, a list of n+1 can be sorted" instead of "let's put max last and sort the rest"
>>
>>50780171
what? That's literally in this very thread
>>
>>50780171
Also the "bubble sort puts largest element last" is kind of a big abstraction too, if you wanna be thorough math-wise. Sure we can see that, but how does on prove it?
>>
>>50774884
>/g/uys please do my homework for me.
>>
>>50780171
Yes, but this is an imageboard and not a scientific journal. There is nothing wrong with being colloquial when everybody knows we're doing an induction proof anyway. People have spelled out the base case and the induction step. That enough if we can tell the hypothesis by context.
>>
>>50780208
dude, shut up, this is semester 1 proof by induction shit
>>
>>50780248
>imageboard
>doesn't post qt animu waifu
>>
File: 1432423424060.gif (402 KB, 360x640) Image search: [Google]
1432423424060.gif
402 KB, 360x640
>>50780208
Induction on the inner loop.

>>50780299
S-sorry...
>>
Hey guys, does anybody have any code that can, like, take random code and basically say whether or not it's good? Like if it would ever produce errors or whatever? not for homework I'm trying to do it for work a promise
>>
>>50779383
if it's not induction it's at least similar to to this proof technique:
https://en.wikipedia.org/wiki/Proof_by_infinite_descent
>>
>>50780372
It's using structural induction over arrays to prove that the algorithm can sort an arbitrary list of any length. (This is equivalent to using induction over the length of an array, which is what you'd do if you were being ultra-formal.)
>>
>>50780372
I think you have it right

I'm retarded, but I finally figured how to format it in an inductive way

hypothesis: a list of n is sortable
assumption: a list of n+1 is sortable if the hypothesis holds
proof: bubblesort puts the biggest element of a list of n+1 and puts it at the end. Now the last element is sorted in relation to the rest of the list. the rest of the list is sortable, and sorting it makes the whole list sorted, so the whole list is sortable
base: a list of 1 is sorted

It's pretty much the same thing but it describes it in a different "direction". It's not any better than
>https://en.wikipedia.org/wiki/Proof_by_infinite_descent
but I'm pretty sure at least not induction is the right term
>>
>>50780372
too complicated. Proof by induction is a much more straightforward way to do this
>>
>>50780516
and full of typos of course. I'm sorry, I'm sleep deprived.
>>
>>50780516
the only thing that's missing is a proof of the selection algorithim
>>
>>50780613
yeah. Has it been provided in the thread? I don't even know anymore.
>>
>>50780637
Yes, 3 times, you fucking retard.
>>
I'd just use induction like stated earlier in the thread. I have the proof all in my head but I wouldn't bother typing it out because it would take too long, and I'd rather prove the correctness of a more commonly used algorithm, like quicksort
>>
>>50780671
which post
>>
>>50780671
don't think so
>>
>>50780677
Do that then
>>
What are you all talking about, with induction and contradiction and shit? That's not how you prove algorithms (well, at least most of em).

You prove them by a) putting checkpoints after every operation and test, defining some invariable expressions, and showing how the invariable expressions hold true when one checkpoint flows into another, and b) showing that for every input the algorithm does in fact end with an output. Most of you probably don't even have a CS degree, and thus shouldn't be in this thread.
>>
>>50780743
>implying there's only one way to do it
>>
>>50780743
uh huh
>>
File: godl.jpg (38 KB, 400x514) Image search: [Google]
godl.jpg
38 KB, 400x514
>>50780743
>>
>>50780743
Sorry, most of us don't have 2^(32*1024*1024*1024*4) ms to spare.
>>
>>50780743
actually yeah, this seems to be true, we've only been proving that the abstract algorithm works but not that some correct bubblesort program produces the correct output with all inputs, so those are 2 different things. OP asked for general proof about the algorithm though
>>
/g/ talking about math and proofs is kind of sweet. BTW OP's pic is from Rudins principles of meme analysis
>>
>beginner CS maths
>tfw struggling
I should kill myself
>>
>>50779359
Yet you name none of them, just furthering how idiotic you argument is
>>
>>50781447
bogosort
>>
>>50781075
u gotta start somewhere bby
>>
I like how programming is all
"whoa revolutionary ideas man"
"lets make ai sex bots"

and then

BAM FUCKING MATH.
>>
>>50782131
math is sexy

the largest erogenous zone is the brain tbh
>>
>>50782150
Then my brain must be fucked cause I get off to logic puzzles.
>>
Is this why cs won't get oversaturated? Because everyone in it is this retarded?
>>
>>50782131
I know right, I just want to make video games.
Thread replies: 175
Thread images: 12

banner
banner
[Boards: 3 / a / aco / adv / an / asp / b / biz / c / cgl / ck / cm / co / d / diy / e / fa / fit / g / gd / gif / h / hc / his / hm / hr / i / ic / int / jp / k / lgbt / lit / m / mlp / mu / n / news / o / out / p / po / pol / qa / r / r9k / s / s4s / sci / soc / sp / t / tg / toy / trash / trv / tv / u / v / vg / vp / vr / w / wg / wsg / wsr / x / y] [Home]

All trademarks and copyrights on this page are owned by their respective parties. Images uploaded are the responsibility of the Poster. Comments are owned by the Poster.
If a post contains personal/copyrighted/illegal content you can contact me at [email protected] with that post and thread number and it will be removed as soon as possible.
DMCA Content Takedown via dmca.com
All images are hosted on imgur.com, send takedown notices to them.
This is a 4chan archive - all of the content originated from them. If you need IP information for a Poster - you need to contact them. This website shows only archived content.