本文為翻譯文章,原文: Guerrilla logic: A salute to Mervyn Pragnell, by peter on vukutu, Sep 13 2009. 感謝作者授權翻譯。
如果寫一部英國電腦科學的詳細歷史,一個不能忘記的名字是 Mervyn O. Pragnell. 據我所知,Mervyn Pragnell 從沒擔任過學術工作,也沒有發表過論文。但他把英國電腦科學的幾個關鍵角色介紹給彼此,同樣重要地,讓他們認識了 Alonzo Church 的 λ calculus (Hodges 2001). 在 1950 和 60 年代,邏輯學在哲學或是純數學中都尚未受到很大重視,更別說電腦科學。他並不是一個在大學裡領薪水的學者,卻以自己辦私人讀書會的方式研究邏輯,幾乎像是在打游擊似地。
Pragnell 招募邏輯讀書會成員的方式是到倫敦的書店中閒逛,若看到有人買邏輯的書就和對方搭訕 (Bornat 2009). 其中不少人後來成為知名的電腦先驅,包括 Rod Burstall, Peter Landin (1930-2009), 和 Christopher Strachey (1916-1975) 等等。讀書會都在晚上舉辦,通常在倫敦大學 Birkbeck 學院,而學院方面並不知道有這回事,也自然沒有正式批准 (Burstall 2000) (譯注:據說 Pragnell 認識一個在那工作的技師,每次偷偷幫他們開門). 有時候他們會移師到附近的酒吧 The Duke of Marlborough 去繼續討論。Pragnell 似乎曾在 1960 年代時受聘擔任 Strachey 的研究助理,在 Strachey 家裡工作 (Burstall 2000)。在 1980 年代時他是倫敦大學帝國學院計算系的邏輯程式討論會的固定成員。在當時(和現在)那都是電腦科學形式邏輯的重要研究中心。
很遺憾地,很少人知道 Pragnell 在早期理論電腦科學扮演的關鍵角色。例如,Donald MaKenzie 那本關於自動定理證明的歷史與社會面的好書雖然提到了 Pragnell (MacKenzie 2001, p. 273), 卻在索引中把他遺漏了。除此之外,我找到的資料都是從其他人的訃聞或回憶錄中拼湊而來。如果有其他資訊,請不吝提供給我。
2009.9.23 更新: 衛報刊出了一篇 Peter Landin 的訃聞,其中也提到了 Mervyn Pragnell. (譯注:我也是因此得知 Pragnell 的故事,並找到這篇文章的。)
參考資料
- Richard Bornat (2009): Peter Landin: a computer scientist who inspired a generation, 5th June 1930 – 3rd June 2009. Formal Aspects of Computing, in press.
- Rod Burstall (2000): Christopher Strachey – understanding programming languages. Higher-Order and Symbolic Computation, 13: 51-55.
- Wilfrid Hodges (2001): A history of British logic. 未出版之投影片. 可從作者網站下載。
- Donald MacKenzie (2001): Mechanizing Proof: Computing, Risk, and Trust. Cambridge, MA, USA: MIT Press.
Thanks, Shin-Cheng.