Shin

avatar

最大信用問題 — 一個區段問題的例子

給定一個含數字的陣列 A [0.. N), 0 ≤ N. 其中任一個連續區段 [p..q) 的「信用」是其中正數的個數減去負數的個數:

credit p q =〈# i : p ≤ i < q : A i > 0〉-
                 〈# i : p ≤ i < q : A i < 0〉

請推導出一個程式,計算該陣列中「信用最高的區段」的信用,也就是

〈↑ p q : 0 ≤ p ≤ q ≤ N : credit p q〉

除二、相減,大小不變?來自《結構化編程》中的一個小例子

請問如何論證:如果 0 ≤ r < dd 成立,經過這兩行程式後,0 ≤ r < dd 仍成立?

dd := dd / 2;
if dd ≤ r then r := r - dd

這個例子來自 Dahl, Dijkstra & Hoare 1972 年的 Structured Programming. 書名引起我的注意:「結構化程式設計」在 70, 80 年代曾被學界、業界視為軟體危機的解方、所有人寫程式該遵守的圭臬。但每個陣營對它是什麼都各有一套解釋。數十年過去,structured programming 卻以一種不知能否算功成而退的方式被遺忘:現在的學生們自然地把程式寫成塊狀的結構,許多人甚至已經不知有 goto 這個指令。但他們沒聽過 structured programming, 對於 Dijkstra 等人當年提倡的程式推論仍一樣地陌生。

我想知道這套概念的創始者們怎麼談它,因此好奇地想讀這本書。

「讓程式能依據其結構被理解、被證明」便是我心目中的「結構化編程」。而在那個時代,他們的挑戰便是設計語言、符號,使得這種編程與推論成為可能。

2012 「邏輯、語言與計算」暑期研習營 (FLOLAC ’12)

因為今年做的種種改變,FLOLAC 2012 的籌備比起往年慢了一些。這兩天發現已經有人在詢問了。是的,今年 FLOLAC 照常舉辦,而且將成為大學部的正式暑修課程!也因此,FLOLAC 開課時間改為暑期後半(8月27日至9月7日)而非傳統的七月。今年的國外講者是任職於 Max Planck Institute for Software Systems 的 Arthur Charguéraud, 將為我們介紹程式語言學界影響力日增的定理證明/程式驗證工具 Coq.

Benoît Mandelbrot 與碎形

雲、山、海岸線、閃電等都是自然界可看到的碎型,複雜而不規則。然而這是自然之所以美的原因。如果雲是圓形的,那多無聊。而如果數學不能捕捉自然之美,那是多麼可惜的事情。碎型理論揭去了這層神秘的面紗,告訴我們,這些自然事物的「規則」其實隱藏在另一個維度中。