Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

Ask HN: What's your favorite elegant/beautiful algorithm?

news.ycombinator.com

Post reply on HN
Print view View original

491–500 of 507 posts

Re: Ask HN: What's your favorite elegant/beautiful algorithm?

#491

Post by jules »

wizeman wrote: post #490
jules wrote: post #489

Earlier quoted context omitted.

That would be nice, then the run time predicate can be fast while the logical version remains elegant. What happens if you remove requires { forall i j. (i (pred i -> pred j)}? I think it should still check, actually. That property ensures that the answer will be unique, but the algorithm will find a point pred i = False /\ pred (i+1) = True even if the predicate does not satisfy that property. If you add the uniquen…

> What happens if you remove requires { forall i j. (i (pred i -> pred j)}? I think it should still check, actually. If I simply remove that 'requires', then Why3 cannot prove the postcondition of `binary_search` automatically anymore (using the Z3, CVC4 and Eprover automatic provers that I have installed). Specifically, Why3 tries to split the postcondition into the 2 parts: `pred result = False`, which gets verifie…

> I think this is because nothing stops `high` from actually being lower than `low`.

Ahh, right. I guess that's exactly the type of oversight that a checker is for :)

We could return the pair (!cur_low, !cur_high) and have the postcondition that pred (fst result) = False and pred (snd result) = True and abs (first result - snd result) = 1. Then it would work also if low > high, but I'm not sure this is useful in practice...

> The run-time version of `pred` is a partial function (it only works for valid array indices), so it needs a precondition. However, when I pass `pred` as an argument to `binary_search`, I can't / don't know how to specify that the argument needs the precondition.

If I'm understanding this correctly, you want to do something like this:

  let binary_search (pred: (i:int) -> bool requires { low
But Why3 does not support this?

If you add a precondition like that to pred, wouldn't that also prevent requires/ensures/invariant from calling pred on arguments that don't satisfy the precondition? In the precondition we do want pred low = False /\ pred high = True, but the run time predicate only allows pred k for low < k < high?

Re: Ask HN: What's your favorite elegant/beautiful algorithm?

#492

Post by wizeman »

jules wrote: post #491
wizeman wrote: post #490

Earlier quoted context omitted.

> What happens if you remove requires { forall i j. (i (pred i -> pred j)}? I think it should still check, actually. If I simply remove that 'requires', then Why3 cannot prove the postcondition of `binary_search` automatically anymore (using the Z3, CVC4 and Eprover automatic provers that I have installed). Specifically, Why3 tries to split the postcondition into the 2 parts: `pred result = False`, which gets verifie…

> I think this is because nothing stops `high` from actually being lower than `low`. Ahh, right. I guess that's exactly the type of oversight that a checker is for :) We could return the pair (!cur_low, !cur_high) and have the postcondition that pred (fst result) = False and pred (snd result) = True and abs (first result - snd result) = 1. Then it would work also if low > high, but I'm not sure this is useful in prac…

> If I'm understanding this correctly, you want to do something like this:

Exactly!

> But Why3 does not support this?

As far as I can tell, it doesn't. I get a syntax error if I either try to name the argument to pred or if I try to add a 'requires {}'.

Maybe they will add this functionality to a future version, or maybe there is already a different but simple way to do this (but I don't know how).

> If you add a precondition like that to pred, wouldn't that also prevent requires/ensures/invariant from calling pred on arguments that don't satisfy the precondition?

No, logical/proof functions are always total, they cannot be partial.

One option is to always define what the function should return for the entire domain of its arguments.

The other main option AFAIK is to define the results only for a restricted domain that interests us and leave the function undefined outside this restricted domain (but in this latter case, we won't be able to extract conclusions about what the function returns outside this restricted domain).

However, as far as I know, the latter option needs to be implemented differently in Why3, specifically as an abstract predicate/function, and then you separately define axioms about things you know about the predicate/function. The disadvantage is that if you make a mistake in one of the axioms (say, you accidentally define that the function returns both True and False for the same input), then you are introducing an inconsistency which allows you to prove anything you want (i.e. you would be able to trivially prove that 2 = 3). This is undesirable, of course.

I think I saw somewhere that if you define a predicate `P` in Why3 that works both for runtime and for proofs, and then you add a precondition `A` to this predicate, then Why3 will automatically add an implication to the predicate for proofs, i.e. if use this predicate in a proof, the predicate will become `A -> P(x)` instead of just `P(x)`. But I'm not entirely certain about this, I could be wrong.

Unfortunately Why3 is not very well documented, the vast majority of what I've learned so far has been through reading the examples, looking through the git history, and trial-and-error.

> In the precondition we do want pred low = False /\ pred high = True, but the run time predicate only allows pred k for low Exactly, this is why I was trying to add a new predicate (for proofs only), which returns False for i = high, but calls the other predicate otherwise.

However, I still run into the same problem: I cannot specify that a function argument needs a precondition, and therefore Why3 cannot tell that the precondition doesn't get violated...

Re: Ask HN: What's your favorite elegant/beautiful algorithm?

#494

Post by j2kun »

mehrundmehr wrote: post #166
calciphus wrote: post #56

The Gale-Shapley Algorithm to solve the "Stable Marriage" problem. 2012 Nobel Prize in Economic Sciences for its wide-ranging use in medicine, education, and resource allocation. It's fairly easy to implement a basic version of it, feels intuitively obvious once explained, and has been applied to everything from organ transplants to student placement in elementary schools. Really, any place you have two groups where…

I remember when this "Nobel Prize" was announced I immediately started reading the paper and trying to figure out how it could work in code. It seems like it could have amazing economic potential if put to a good use, but until your comment I hand't known of any real-world uses outside of organ transplantation. Very excited to see it being appreciated by more computer scientists! I need to look into it again for sure…

The organ transplant algorithm is not really that similar to the stable marriage algorithm. It's a different mechanism based on the housing allocation problem. See https://www.nber.org/papers/w10002

I think they are lumped together because they are both "mechanism design" problems that were studied by Roth and part of his prize.

Re: Ask HN: What's your favorite elegant/beautiful algorithm?

#495

Post by joker3 »

QML wrote: post #430
joker3 wrote: post #325

Earlier quoted context omitted.

There's no matching process at the beginning of medical school, but there is for assigning med school graduates to residencies. This variant of the problem is NP-hard, so there's no exact solution, but matching still works pretty well. https://web.stanford.edu/~alroth/papers/rothperansonaer.PDF has all the details.

When you are referring to this "variant", are you referring to maximal matching, or bipartite matching when the number of people and schools don't equal?

The issue is that couples want to be placed together. That makes everything trickier than if people just placed independently.

Re: Ask HN: What's your favorite elegant/beautiful algorithm?

#496

Post by andrath »

prestonbriggs wrote: post #263
andrath wrote: post #168

Duff's device. Because you will first look at it in disgust, but then you realize how clever it really is. See: https://en.wikipedia.org/wiki/Duff%27s_device

Disgusting indeed: A way to write irreducible loops that doesn't use a goto. Good idea to measure the resulting code, given how poorly most optimizers deal with such loops. Even sadder because the same effect can be achieved cleanly (and "optimizably")by using as "switch" followed by a "while".

You should read Tom Duff's original email about this:

https://www.lysator.liu.se/c/duffs-device.html

A quote of the man himself about this: "I feel a combination of pride and revulsion at this discovery."

Re: Ask HN: What's your favorite elegant/beautiful algorithm?

#497

Post by andrath »

bunderbunder wrote: post #235
bsenftner wrote: post #206

Earlier quoted context omitted.

Quite a few EA Sports games have Duff's Device in locations of computational bottlenecks. I know because I put them there. Wonderful little mechanism.

That's really interesting to hear. I tried Duff's Device myself, once upon a time, and found it made no measurable difference, so I pulled it back out. This was a long time ago, so I had just assumed that a similar optimization was just built into most C compilers these days. Does it vary by toolchain? I believe I was using clang at the time. (I was still quite wet behind the ears at the time, so it's also more than…

Yes, modern compilers do loop unrolling nowadays, so Duff's device doesn't really have a use. But it's certainly a wonderful bit of history. I found Duff's device when I was researching coroutines in C.

Re: Ask HN: What's your favorite elegant/beautiful algorithm?

#498

Post by andrath »

Sean1708 wrote: post #251
bsenftner wrote: post #206

Earlier quoted context omitted.

Quite a few EA Sports games have Duff's Device in locations of computational bottlenecks. I know because I put them there. Wonderful little mechanism.

Is there ever a case nowadays where the compiler doesn't do this for you automatically?

No, this is just a wonderful bit of obsolete hacker history. Unless if you mess with retro-architecture for fun (like old PDP machines, be they emulated or real), then it's somewhat relevant.

Re: Ask HN: What's your favorite elegant/beautiful algorithm?

#499

Post by aerovistae »

jonathanstrange wrote: post #121
aerovistae wrote: post #109

Oh, man. So many answers. The blockchain of bitcoin is pretty gorgeous, if that counts. AES is beautiful as well. And I love Huffman encoding. hm, what else. Bloom filters are awesome. I suspect FFT is beautiful, too, but it surpassed my ability to understand.

Out of curiosity, what do you find beautiful about AES? I personally think that Speck is pretty cool because of its extreme simplicity, but I can't see anything special about AES.

I'm sorry, I meant to say RSA. My mistake. I find the mathematics of it quite elegant.

Re: Ask HN: What's your favorite elegant/beautiful algorithm?

#500

Post by vram22 »

vram22 wrote: post #470

Mildly amusing anecdote: I was on the panel for interviewing software engineer candidates at a large software company where I worked earlier. I asked one junior candidate (having a few years of experience) to tell me how she would solve the set cover problem [1]. I illustrated the problem with a concrete example: a project needing to fill roles with different tech skills; there is a pool of candidates, each of whom h…

Had forgotten to give the link for the set cover problem (the [1] above). Here it is:

https://en.wikipedia.org/wiki/Set_cover_problem

I didn't know the following about it before (from the Wikipedia page):

[ The set cover problem is a classical question in combinatorics, computer science and complexity theory. It is one of Karp's 21 NP-complete problems shown to be NP-complete in 1972.

It is a problem "whose study has led to the development of fundamental techniques for the entire field" of approximation algorithms.[1] ]

Post reply on HN