Curry–Howard correspondence

If one now abstracts on the peculiarities of this or that formalism, the immediate generalization is the following claim: a proof is a program, the formula it proves is a type for the program. Most informally, this can be seen as an analogy which states that the return type of a function (i.e., the type of values returned by a function) is analogous to a logical theorem, subject to hypotheses corresponding to the types of the argument values passed to the function; and that the program to compute that function is analogous to a proof of that theorem. This sets a form of logic programming on a rigorous foundation: proofs can be represented as programs, and especially as lambda terms, or proofs can be run.

The correspondence has been the starting point of a large spectrum of new research after its discovery, leading in particular to a new class of formal systems designed to act both as a proof system and as a typed functional programming language.

— Wikipedia on Curry–Howard correspondence

2010.03.07 Sunday ACHK

Past papers 5

“Past papers” means “past HKCEE/HKAL examination papers”. The topic is for Hong Kong students who are facing HKCEE or HKAL. But the general principles can also be used for tackling other public examinations.

基本上,你把每天的溫習化成模擬考試(即是按年份做 pastpaper)就可以。然後根據每日的分數和每日的錯處,來決定下一日溫什麼。

有一個原理就是,千萬不要企圖完成所有事情。大部分的情況下,你的時間只會足夠完成 “所有事情” 中的一小部分。你可以達到的,就是選最重要的事去做。

比喻說,有一個人入了急症室。他的 心、眼、手 都有危險。那樣,醫生應先救哪一個器官呢? 

— Me@2010.03.06

2010.03.07 Sunday (c) All rights reserved by ACHK

天空堤壩

Talent at its best and character at its worst

.

Lord Acton said we should judge talent at its best and character at its worst. For example, if you write one great book and ten bad ones, you still count as a great writer — or at least, a better writer than someone who wrote eleven that were merely good. Whereas if you’re a quiet, law-abiding citizen most of the time but occasionally cut someone up and bury them in your backyard, you’re a bad guy.

— Paul Graham

.

才能方面,如果一個人的最高點是可以接受的話,你就可以錄用他,即使他有其他任何才能缺點;

品德方面,如果一個人的最低點是不可接受的話,你就千萬不要錄用他,即使他有其他任何品德優點。

— KinOn’s presentation, modified by Me@2010.03.06

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

才能方面,一個太陽可以照亮整個天空;

品德方面,一條裂縫可以摧毀整個堤壩。

— Translation by Me@2010.03.06

.

.

.

2010.03.07 Sunday copyright ACHK