Prove that bubble sort is correct.
Can you do it /g/? If not, put that CS degree in the trash.
>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?
>never bothered learning sorting algorithms because I'm not a poo-to-the-loo shitskin codemonkey
Just because an algorithm is mathematically correct doesn't mean it's any good.
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".
i can write hello world without knowing 1 + 1.
hurrr durrrr no math needed.
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;
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.
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.
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
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
programming music thread
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)
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.
>just run some test cases
>proving your algorithm is actually quite useless
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.
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.
>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.
by inductionn on n, assuming we aren't morons unable to swap, anyway you can prove the swap until ordered by induction aswell
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
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.
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.
>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.
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"
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.
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.
>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.
>in which you need to uses Z Transforms, Lagrange and Fourier.
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.
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.
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.
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
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
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.
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.
>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? :^)
>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.
>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.
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"
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.
Induction on the inner loop.
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
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.)
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
but I'm pretty sure at least not induction is the right term
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
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.
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