Interesting new sort algorithm...

[brucehoult]

When comparing it with bubble or insertion sort, you need to consider the order of the loop indices, which will give you a hint.
The article explains why it is not obvious at first sight, so for those wondering, just read it.

While in the end, this "algorithm" is completely useless per se, for people studying (or brushing up on) how to prove algorithm correctness, this can be a nice simple exercise, so that's where I would put the value of this article.

Being able to prove/disprove algorithm correctness is a very valuable skill.

I don't distinguish between "proving correct" and "getting how it works".

[KaneTW]

I don't distinguish between "proving correct" and "getting how it works".

You do a formal proof on every algorithm that you learn?

[golden_labels]

First and foremost: I just confirmed that the publication is authentic, written by that author. And that it indeed is often misinterpreted the way it did happen in this thread.

magic:
Some other people above have realized their mistake, did read the article carefully and understood its key idea. Perhaps it would be wise to rethink the position if such a strong warning signal is present?

brucehoult:
Understanding an algorithm means you grasp the idea behind its operation. That doesn’t automatically mean it actually achieves the goal. For that a proof is needed. Otherwise everything would be always valid, because anyone proposing an algorithm understands it: obviously that is not true.

[brucehoult]

I don't distinguish between "proving correct" and "getting how it works".

You do a formal proof on every algorithm that you learn?

I don't write it down, but "getting how it works" means figuring out what the invariants and induction schemes for any loops or recursions are, which means I *could* write down a proof, yes.

[brucehoult]

brucehoult:
Understanding an algorithm means you grasp the idea behind its operation. That doesn’t automatically mean it actually achieves the goal. For that a proof is needed. Otherwise everything would be always valid, because anyone proposing an algorithm understands it: obviously that is not true.

If you propose an algorithm but it doesn't work then you don't understand it at all!

Do they not teach preconditions, postconditions, invariants, and weakest preconditions these days?

You don't need to type up a formal proof in LaTeX, you only have to figure out the invariants and how they are maintained. If you haven't done that then you DON'T "grasp the idea behind its operation", you only have a wet finger in the air.

[golden_labels]

Perhaps the difference in interpreting word “understand”?

I’m not a native English speaker and, at least according to their flags, the same is true for KaneTW. That may affect to what concepts the word maps. However, multiple things contradict that explanation and support our perception of “understand”:

• English doesn’t treat it as a binary property, but as one with multiple levels: “deeper understanding”, “shallow understanding” &c. See Google Ngram Viewer for examples. Your interpretation makes it binary.
• The English Wikipedia article on understanding contains a fragment, written by a native English speaker Greenrd: “A teenager may understand that multiplication is repeated addition, but not understand the broader implications of this.” That wouldn’t be possible in your interpretation. The tone of the entire article is also giving the same impression.
• I can’t easily recall, from my own experience, a piece in English that would use “understand” in your interpretation. At the same time any use I find⁽¹⁾ is either one I can’t classify or matching our version. That includes those in the top search results for “.edu”, like “the analysis of an algorithm can help us understand it better” (taken from a course materials at Princeton) or “if a grader cannot understand your solution, they cannot give you any credit for it.” (from MIT 6.006 syllabus).
• I have trouble accepting your interpretation from philosophical point of view. It has completeness of knowledge as a prerequisite for understanding.

From my perspective “understand” used in this context is limited to having a valid model. It does not extend to drawing conclusions from that model, but that’s what making a formal proof is.

I believe we may need a clarification, what each of us meant.

⁽¹⁾ And is relevant here. “Understand his feelings” is clearly a different meaning.

[magic]

Do they not teach preconditions, postconditions, invariants, and weakest preconditions these days?

Yes, at those places that used to teach it 50 years ago.
For each reputable university, you now have ten "higher schools of web development, data science and cooking on a gas stove".
And for each of the above, you have ten YouTube channels and Medium tutorials of the "small current controls large current" variety.

This puts things into perspective

[magic]

magic:
Some other people above have realized their mistake, did read the article carefully and understood its key idea. Perhaps it would be wise to rethink the position if such a strong warning signal is present?

I genuinely don't understand what you are even trying to imply here.
If you think I have made a mistake, what it is supposed to be?

I continue to maintain that the algorithm is trivial, and a trivial variant of a well-known one at that. I outlined how it works, Bruce posted a useful invariant if you wanted to write a formal proof. If you think we are wrong, go ahead and post a rebuttal instead of stating the obvious that "the author is getting that sort of response" all the time, as if it meant anything.

Now, there may be people who don't see it, but for those people that sort of algorithms and proofs belong in introductory programming books. I would be mildly uncomfortable writing such an article and utterly embarrassed to put my IRL name under it.

Also, different people have different standards of what it means to understand something, particularly when it comes to maths and related fields. You don't need to write a tl;dr wall of text and speculate about imaginary language barriers, just read and accept what the guy told you.

[SiliconWizard]

Do they not teach preconditions, postconditions, invariants, and weakest preconditions these days?

Yes, at those places that used to teach it 50 years ago.
For each reputable university, you now have ten "higher schools of web development, data science and cooking on a gas stove".
And for each of the above, you have ten YouTube channels and Medium tutorials of the "small current controls large current" variety.

This puts things into perspective

It does. In some universities, you can add "how not to write offensive code" courses too. Then there are only so many hours in a week, so it gets difficult to find time for teaching those old CS concepts.
 

[magic]

I didn't have that option. But we had to take 1h/week or thereabouts of a chosen non-technical course (many options from all over the university) and I recall gender theory being one of the options, kinda regret not trying to get in there, it could have been amusing and unlikely to be hard to pass

[brucehoult]

I didn't have that option. But we had to take 1h/week or thereabouts of a chosen non-technical course (many options from all over the university) and I recall gender theory being one of the options, kinda regret not trying to get in there, it could have been amusing and unlikely to be hard to pass

I did a paper in the Humanities department, a 1st year Philosophy course "Basic Logic". A lot of it duplicated things also covered in computer science, such as AND/OR/XOR, De Mogan's theorem. They used F and T instead of 0 and 1 and wrote their truth tables backwards, from T T T to F F F. They did add some names for others of the 16 truth tables e.g. "implication" for "!A | B" and forms of argument such as Modus Ponens and Modus Tollens, so it wasn't a total waste of time. Also, there were a lot of hotties.

[Mechatrommer]

i can only look from far without having a clue what they are up to, comp sc had more female than we do, i think even now. i mean how many of them interested in mechanic of materials and messing their hand with fiber glass for prototype modelling? so then i had to self develop gender theory and preconditioning during the night by intuition. i dont think i got them correctly until now

[westfw]

Do they not teach preconditions, postconditions, invariants, and weakest preconditions these days?

I think "analysis of algorithms" is generally an MS-level class.  Undergrads are lucky to get "check it out - some sort algorithms perform better than others.  Tomorrow we do trees, and next week is regular expressions!"

[brucehoult]

Do they not teach preconditions, postconditions, invariants, and weakest preconditions these days?

I think "analysis of algorithms" is generally an MS-level class.  Undergrads are lucky to get "check it out - some sort algorithms perform better than others.  Tomorrow we do trees, and next week is regular expressions!"

Seriously?

How are you supposed to design even the simplest loop [1] without knowing what your base case, invariant, and inductive step are?

I mean ... proof by induction was high school, so when I got to programming at university they could assume that as background. And I went to the 5th best out of 7 universities in NZ at the time. [2]

I just did a quick search and found these lecture notes at a university near here (Australia, not NZ, but close enough), so this stuff was taught in 2nd year as recently as 2016:

https://comp.anu.edu.au/courses/comp2600/Lectures/19wp1.pdf


[1] ok, except maybe "for x in set/range ..."

[2] quite deliberately, as 1) it was in a smallish pleasant city, and more importantly 2) they were too small to get one of the Burroughs 6700 mainframe computers the four bigger universities had, and had an infinitely nicer PDP-11/70 instead, with a VAX on the way by the time I got there.

I only learned decades later that they got the PDP-11/70 via a swindle which displeased the Ministry of Education considerably. The Ministry was not prepared to provide capital funding for a computer, saying that Waikato university should use a terminal/punched card reader/printer connected to the University of Auckland mainframe 100 miles away. The computing department arranged to take delivery of a brand new 11/70 for $548,000 (academic pricing, with no import duties or sales tax) at 11:00 one morning in 1976 with "absolutely no ability to pay for it". At 11:01 they sold it to a friendly commercial bank, and at 11:02 signed a deal for lease-to-buy.

[Nominal Animal]

I did a paper in the Humanities department, a 1st year Philosophy course "Basic Logic".

Reminds me of a Uni "party" decades ago, when a Philosophy student presented their truthiness truthfulness theory.  (That in itself was odd, us physics students were used to parties being where you drink and meet people and have fun.)

The theory itself was: Let \$T_k\$ represent the truthfulness of sub-statement \$k\$, \$0 \le T_k \le 1\$ \$\forall k\$.  Then, we can calculate the overall truthfulness \$T\$ of the combined statement via
$$T = \prod_k T_k$$
and they spent forty minutes describing it.

The cute chicks were really in awe of the babble, though.

[westfw]

I just did a quick search and found these lecture notes at a university near here (Australia, not NZ, but close enough), so this stuff was taught in 2nd year as recently as 2016:

https://comp.anu.edu.au/courses/comp2600/Lectures/19wp1.pdf

Well, comp2600 is not in the current "requirements" for "Bachelor of Advanced Computing (Research and Development) (Honours)", much less any of the lesser degrees...

https://programsandcourses.anu.edu.au/program/AACRD#program-requirements

[SiliconWizard]

Do they not teach preconditions, postconditions, invariants, and weakest preconditions these days?

I think "analysis of algorithms" is generally an MS-level class.  Undergrads are lucky to get "check it out - some sort algorithms perform better than others.  Tomorrow we do trees, and next week is regular expressions!"

Seriously?

How are you supposed to design even the simplest loop [1] without knowing what your base case, invariant, and inductive step are?

True.
Welcome to the 21st century.

[Mechatrommer]

make me wonder why i can still make some useful programs even though i cant prove them formally?... when reading turing's paper on his general purpose machine, i thought whats the big deal? we all know binary numbers!.. its amazing the knowledge that was once only in the great thinkers mind now is like a childborn built-in knowledge 

[Nominal Animal]

make me wonder why i can still make some useful programs even though i cant prove them formally?

Because you apply rules that either someone else has worked out and taught you, or you yourself have found via practical experimentation.  You do not know the domain where those rules are reliable, you just write the program according to the rules you know.

The problem is, you do not know when your program no longer produces useful results.  You only know "it works for me".  It is usually a surprise to you that the program fails in certain cases.  To those that understand the implementation formally, usually immediately grasp where the problem lies when the input and the error or problem is described to them.

(This assumes that by "prove them formally", we mean that you have a complete understanding of the implementation, not that you know how to convey such understanding in standard form.  Being able to convey the understanding, somehow, is important though, because us humans often believe we completely understand something until we actually try to convey that understanding, even if to a rubber duck.)


I self-taught myself to program before I had had any higher math or formal logic classes.  I am by nature analytical, so I had a huge relief and excitement when I found the formal math used to describe these things; it was like finding a language that can express the things I had been trying to grasp, and then apply the tools hundreds of mathematicians and logicians had developed, to solve more and more complex problems.

(I myself am "bad" at writing formal proofs.  For some reason, I seem to see and think a bit differently about certain things, so those that do formal proofs often can usually simplify them into much simpler and easier to understand expressions.  But that is not the same thing as my proofs being invalid or wrong or incomplete, just, uh, "artless".)

While those formal proof things can seem a waste of time, they do actually come packaged with extremely powerful tools in algorithm analysis and development, which will allow you to cut some problems into trivial bits, and do so with simple code that you probably wouldn't understand without those tools.
Recursion and loop analysis, algorithm time and space complexity, and logic and graph theory based approaches to certain problems come to mind.

Here is a practical example:

Consider a large chessboard-like grid.  You have different colored pebbles on the grid.  Whenever two pebbles of the same color are in adjacent cells, they belong in the same group.  The question is, how do you count the number of groups on the grid?

The solution is a simple abstract data type called disjoint-set, preferably with path compression.  When you start with an all-singleton set with each pebble described in the set, then apply Union to each pair of adjacent pebbles, you end up with a set where each group is distinct.  Flatten the disjoint-set data structure, and you have a group identifier for each pebble.  To count the number of groups using this approach, you need two numbers (between 0 and the total number of pebbles, inclusive) per pebble, of space.  Time complexity is less than you'd expect, but is a pretty complex topic.

You can use this data structure without understanding why it works, but unless you know its limitations and requirements, you won't know if or when it fails.
It will be almost impossible to say (without it being a pure guess) whether it can be used to solve some problem more efficiently/faster than some other method.  With algorithm analysis, you can at least easily compare asymptotic behaviour.

[brucehoult]

I just did a quick search and found these lecture notes at a university near here (Australia, not NZ, but close enough), so this stuff was taught in 2nd year as recently as 2016:

https://comp.anu.edu.au/courses/comp2600/Lectures/19wp1.pdf

Well, comp2600 is not in the current "requirements" for "Bachelor of Advanced Computing (Research and Development) (Honours)", much less any of the lesser degrees...

https://programsandcourses.anu.edu.au/program/AACRD#program-requirements

A sufficient reason for it not to be a required course is they're not teaching comp2600 at all currently.

However if seems much the same material is being taught in a FIRST year class, comp1600, which is on that required course list:

https://comp.anu.edu.au/courses/comp1600/lectures/

There are even a bunch of videos on youtube:

https://www.youtube.com/playlist?list=PLA72M-qSGPm2WxSxXthNiYx2u4KBZlXCC

The first video is less than 3 minutes long:



2nd comment on youtube: "this is where the good stuff starts."

[Mechatrommer]

thats explained why some papers/courses look gibberish to me, i've been having difficulty in understanding some engineering/paper/technical reading esp when it comes to SETS, recently i tried to dig whats the high level math is all about and i start to seeing things and notions that i've not seen before, being in engineering study i know we are using a subset of math (balance of left and right side or solving values, calculus etc), but this is not what i've imagined, it started to look like poetry a list of procedures/steps in proving things. i guess this kind of things have passed me, i cant start all over there are too much to study and time needed than what i think i currently have, so i have to move on... thanks for clarification about this subject... https://www.springerprofessional.de/en/springer-undergraduate-mathematics-series/1020322

[Nominal Animal]

i cant start all over there are too much to study and time needed than what i think i currently have, so i have to move on...

Don't worry; knowing what you don't yet know, but can reach for when you have the time, is a very big and Good thing.

Just like you said, those programs you write are useful; you just do not yet have the expertise to prove or 'formally quantify or qualify their behaviour'.  If you need that, you can always reach for others to help.  More importantly, you now know to say "I don't know, but I know how we can find out", instead of guessing.  This is important, and core part of rational behaviour.

As an example, I myself have lots of experience in numerical simulations, (pseudo)random number generators, and software development in general, and formal education in that.  I even have some formal education in electronics, although it is theoretical only.  What little practical experience I have, is wiring modules (sensors) to single board computers, implementing suggested application circuits from datasheet, and so on.  So, when it comes to real-world circuits, especially designing a new circuit to do a real-world task, I'm a complete beginner!

And that is okay.  Just go take a look at the threads I've started at the Beginners forum, and you can see how much I appreciate the help and learn from it.

There is absolutely nothing wrong in not knowing stuff yet, as long as one acknowledges it.

[westfw]

How are you supposed to design even the simplest loop without knowing what your base case, invariant, and inductive step are?
I mean ... proof by induction was high school, so when I got to programming at university they could assume that as background. And I went to the 5th best out of 7 universities in NZ at the time.

Well, I never had any classes that attached mathematical formalism or terminology to that sort of stuff.  But then, I was an EE major and carefully trying to fit "interesting" CS classes into a schedule that already had a limited number of "technical" electives I was allowed to take (that was back in ~1980 when no one was admitting that an EE might need to know how to program.) (that's back when Stanford didn't even have a CS degree, BTW.  They just considered it a subset of the Math major...)

Stanford has an interesting online class Introduction to Mathematical Thinking that posits "if you came up through a normal HS, or have taken science classes like physics, you probably think of math as a way of getting results."  Yeah, that's me.  I've tried taking some of the more mathematical online classes, and ... they're really tough.  It seems I need to go back a very long way just to learn (or re-learn) the vocabulary...

[DiTBho]

Do they not teach preconditions, postconditions, invariants, and weakest preconditions these days?

I think "analysis of algorithms" is generally an MS-level class.  Undergrads are lucky to get "check it out - some sort algorithms perform better than others.  Tomorrow we do trees, and next week is regular expressions!"

one week         

[brucehoult]

How are you supposed to design even the simplest loop without knowing what your base case, invariant, and inductive step are?
I mean ... proof by induction was high school, so when I got to programming at university they could assume that as background. And I went to the 5th best out of 7 universities in NZ at the time.

Well, I never had any classes that attached mathematical formalism or terminology to that sort of stuff.  But then, I was an EE major and carefully trying to fit "interesting" CS classes into a schedule that already had a limited number of "technical" electives I was allowed to take (that was back in ~1980 when no one was admitting that an EE might need to know how to program.) (that's back when Stanford didn't even have a CS degree, BTW.  They just considered it a subset of the Math major...)

I started university in 1981. I hard a hard time deciding whether to do Computer Science at the small (3000 students) Waikato University in Hamilton which had PDP-11s and a VAX on the way, or Electrical Engineering at the big Auckland university in the big city. I'd looked through both places. A friend started at Waikato a year before me and I went with him to one of his programming labs. The first year students were doing FORTRAN on a PDP-11/34, but I was told they were switching to Pascal next year. Auckland had an open day and I got my grandmother's brother (who passed away five years ago at 98) to take me. The electrical engineering department had some interesting HP lab computers and some microprocessor SBCs controlling various things. So it could have been interesting.

You don't have to get into scary mathematical notation (and it *is* scary if you try to read it too fast) to reason about your loops. Just think about what ASSERTs you can put before, after, and in the middle of your loop.  And how you can make one identical ASSERT that will work in all three places.

e.g.

Code: [Select]

ASSERT(is_sorted(a, 0, 0));
for (int i=0; i<n; ++i){
   ...
   ASSERT(is_sorted(a, 0, i));
}
ASSERT(is_sorted(a, 0, n-1));