I found an article that nicely demonstrates why thread-safe functions are sometimes not enough and why you als need atomic transactions. To this end, you also have to re-think your class’s interface.
This post is supposed to collect cool geometric proofs that I’ve found on other websites. The current version contains a proof of Nicomachus’s theorem and of the Binomial theorem. Continue reading
Assuming two particles of masses and in the gravitational field of the earth.The earth has a mass of kg according to Wikipedia. What is the tidal force on the two particles as a function of their distance to the center of the earth? Continue reading
tl;dr: In this post I point to two ideas: How to write proofs by Leslie Lamport and how to write reasearch papers by Simon Peyton Jones.
Last week, we had the Heidelberg Laureate Forum here in … well, Heidelberg. I did not participate but I like to read about the event and in particular its invited laureates, as for example on their blog.
One talk that I liked particularly was the one by Leslie Lamport. (Btw.: Some people like to call him “The Turing award winner and father of LaTeX”, but given his publications list that’s both too unspecific and too narrow.) Anyway, I liked his talk about “How to write a 21st century proof”. There is also a paper about the same idea.
I liked the idea of clearly structured proofs. He demonstrates this idea with a proof of a corollary of the mean value theorem in calculus. He does this by taking a conventionally written prose proof from a text book and adding structure and names to it. Pretty much as one would do when trying to teach a computer (proof assistant) the proof. Eventually (in the paper) he even goes all the way to define the proof in his own specification language (TLA+) which can be used as a proof checking language. So he goes from conventional (mostly prose) proof to structured and better readable proof on to not-readable-for-humans-but-for-computers proof. And the middle step is the one I liked very much.
The particular proof that Leslie Lamport has picked for his talk and paper has a linear structure. Therefore, it is easy to enumerate the steps of the proof as a list. However, some proofs don’t have this linear structure but still lend themselves to a depiction by other directed acyclic graphs (See for example this rewrite of Szemeredis theorem by Terence Tao, page 8). But the general idea of dividing a proof into smaller (how small) steps and specifying all the assumptions and conclusions of each step, linking them to a directed acyclic graph is a very natural way to do this.
The difficult questions are of course how small should the steps be and how much detailed should be added to each step. But Lamport also answers this question: Make it hierarchical and use modern tools (in this case hypertext). This way one can expand or collapse each part of the proof and hide details from the eyes of sophisticated readers. If one cannot use hypertext, the only solution is to make an assumption and imagine a particular reader. This reader can be a little curious kid (as in the paper’s proof from the freshman calculus book) or a fields medalist reading your latest research article.
For me personally, it sounds like an interesting idea to extend the idea of less prose and more structure to scientific articles. But of course, this has already been done by Lamport’s fellow Microsoft employee (and Haskell inventor (again the question: is this fair to him or the other Haskell inventors)) Simon Peyton Jones in his article and talk How to write a great research paper.
One thing that I don’t like about papers can be captured by the following quote from Jones’ talk:
Example:“Computer programs often have bugs. It is very important to eliminate these bugs [1,2]. Many researchers have tried [3,4,5,6]. It really is very important.”
Yawn![Better] Example:“Consider this program, which has an interesting bug. <brief description>. We will show an automatic technique for identifying and removing such bugs”
I also agree with Jones in that I don’t like it when authors put the related work section in the beginning and therefore build a hill or wall over which the reader has to climb to get to the actual results. I think a good approach to this problem would be the same way that Lamport proposed in his talk: Add structure and hide the details in the lower levels of the hierarchy.
If I find the time I will try to exemplify this at few papers from my field.
Every beginning is difficult. I always feel the implications of this sentence when I want to understand something completely new. This something can be a mathematical concept or a piece of code (software or hardware) written by someone else or my former self.
At the beginning you have to de-construct the work of the other person. What they have built with their creativity, you have to persistently un-build with your intelligence to understand their creative process if you later want to be creative with what they’ve done.
That’s a fundamental problem with human creativity (in certain disciplines?) that you have to go through the process that others have already gone through in order to augment their achievements. Unfortunately, you cannot just continue working with the knowledge of the other person that has been there before. There is no magical transfer of state of mind. All you can do is absorb what they’ve done and get into another, similar state of mind that allows you to reproduce and the surpass their results.
And sometimes that just feels hard. But it feels even harder if you allow yourself or other people to put time pressure on your project. This process is never fast and predictable and you never know how long it will take you to understand the creation of other people.
After I’ve started working with reward-modulated STDP in spiking neural networks, I got curious about the background of research on which it was based. This led me to the book by Richard Sutton and Andrew Barto called “Reinforcement Learning”. The book is from 1998 and it’s freely readable on the internet! In the book’s Introduction they cover the example of an agent learning to beat a given (imperfect) agent in the game of Tic Tac Toe. Two remarks have to be made: 1. The agent has to be imperfect because a perfect agent in Tic Tac Toe (if it’s the one doing the first move) can never be beaten. 2. The agent does not learn to play Tic Tac Toe, this skill is assumed, but it learns a value map for its policy.
Quote by Albert Einstein from “Ideas and Opinions” found on Brain Pickings:
In this sense I have never looked upon ease and happiness as ends in themselves — this ethical basis I call the ideal of a pigsty. The ideals which have lighted my way, and time after time have given me new courage to face life cheerfully, have been Kindness, Beauty, and Truth.