函數式程序設計 鄧玉欣 9787302626909 【台灣高等教育出版社】

編輯推薦
1 一本專門介紹函數式程序設計基本思想和方法的入門級讀物。
2 循序漸進，從基礎原理到高級的語言特徵逐步介紹，具有通俗、系統、寬廣的特點。
3 學習門檻低，適合不具備相關知識基礎的初學者閱讀和理解。
4 習題豐富，並對部分有難度的習題給出參考答案，照顧不具備課堂學習條件的讀者自行學習。
5 適合作為普通高等院校計算機科學和軟體工程專業的本科生教學參考書。

內容簡介
在內容選取上，本講義只涉及 λ-演算，Coq 和 OCaml。毫無疑問，λ-演 算是理解函數式編程語言的基礎和出發點，因此在第一章我們介紹不帶類型 的 λ-演算和簡單類型的 λ-演算，主要討論語法和 β-規約語義。雖然 λ-演算適 合理解函數式編程的一些核心思想，比如數據即函數，但是它的語法構造比較原始，即使表示一個數字都要寫很長的 λ 項，可讀性低，更不用提編寫程序。 Coq 是離 λ-演算比較接近但又能用於編寫一些可讀性較好的計算函數的編程 語言，因此在第二章我們介紹 Coq，重點是從函數式編程的角度展開討論，內 容涉及自然數函數、列表、多態數據結構、高階函數以及柯里-霍華德關聯。作 者認為 Coq 是來用於講授歸納定義和歸納證明思想的出色工具。雖然 Coq 的 長處在於定理證明，但是深入講解需要很大篇幅，因此最好留給專門的書籍， 不適合在入門課程的講義中展開。為滿足適合邏輯證明的需要，Coq 只接受可 終止的函數。這麼強的要求決定它不可能用於日常編程。因此，在第三章我們 介紹一門通用的編程語言 OCaml，除了基本的程序設計概念，我們還會討論 函子和 Monad 這樣比較高級的特徵。講義中選取了一些練習題，希望通過做練習加強 對基本概念的理解。第四章提供了部分習題的參考答案，以方便感興趣的讀者 自行學習。本講義可作為高等院校計算機科學或軟體工程專業的本科教學參 考書。

作者簡介
鄧玉欣 華東師範大學軟體工程學院 教授 ，長期從事形式化方法領域的基礎研究，主要研究方向包括併發計算模型和程序理論。代表性工作包括一個已經被國外學者寫進教科書的「鄧引理」(DengLemma)（R Gorrieri， C Versari Introduction to Concurrency Theory – Transition Systemsand CCS Springer， 2015）和關於概率併發理論的一部英文專著（Y Deng Semantics of Probabilistic Processes: An Operational Approach Springer，2015）。發表學術論文75篇， 其中45篇為第一作者，單篇最高引用118次(GoogleScholar)。多篇論文發表在國際權威期刊和會議如Informationand Computation、TheoreticalComputer Science、CONCUR、ICALP、LICS、POPL等。曾為CONCUR2018作特邀報告，擔任TASE2016程序委員會共同主席，多次擔任理論計算機科學領域著名會議如ICALP2013、ICALP2016、ICALP2018、CONCUR2019、CAV2021的程序委員會委員。

前言/序言
自序
提到計算機編程語言，很多人只聽說過流行的語言，如 C、C++、Java、Python等。事實上，計算機科學家還創造了一類函數式編程語言，如 Lisp、Scheme、Clojure、Erlang、 OCaml、Haskell、F#等。目前函數式編程語言的用戶數較少，而且大部分用於學術研究而非商業，因此普及程度遠遠不能與流行語言相比。但是，的確有一些大型商業項目的開發基於函數式編程語言。例如， Jane Street是一家從事金融量化交易的跨國公司，擁有 400多名 OCaml程序員和超過 1500萬行 OCaml代碼，以支撐每天數十億美元的交易。另外，近年來形式化驗證方法逐漸受到關注，函數式語言廣泛用於開發編譯器、程序分析器、驗證器及定理證明器，以幫助提高軟硬體系統的可信程度。
在這樣的背景下，作者認為有必要在國內開展函數式程序設計相關的教學工作。深入講解函數式編程需要比較多的學時，而目前不少大學在主推通識教育，希望壓縮專業課程的學時數，因此，一種可能的辦法是開設一門本科選修課程，或者是在一門編程語言課程中預留學分給函數式編程教學模塊。本書的編寫目的是服務於這類函數式程序設計入門課，重點讓學生有機會了解函數式程序設計的基本思想和概念，讓學生了解、欣賞，進而喜歡函數式編程。至於函數式語言背後極其豐富的語義理論，更適合設置在軟體理論專業的研究生課程中，因此不在本書予以討論。
本書主要介紹 ζ-演算、Coq和 OCaml，通過這些內容的掌握，相信讀者可以觸類旁通，輕鬆學習其他函數式編程語言。關於這三部分內容，如果讀者希望了解更多，有專門的書籍進行深入講解，例如， ζ-演算的經典教材是 Barendregt的 [2]，Coq的著名教材是 Pierce等的 [13]，OCaml的優秀參考書是 Minsky等的 [10]和陳鋼老師的 [5]。本書精心挑選了一些練習題，希望讀者通過做練習加強對基本概念的理解。
希望本書的出版能夠為國內計算機程序設計和形式化驗證方向的專業人才培養貢獻微薄之力。
鄧玉欣
2023年 3月上海
前言
函數式程序設計是計算機科學中非常重要、歷史比較長久的一個研究方向，但本人在教學過程中發現國內還沒有一本系統介紹這個方向而且適合初學者的讀物。為此，通過總結國內外相關文獻和過去五年的教學實踐，本人嘗試編寫了這本教材 ——《函數式程序設計》。
在內容選取上，本書只涉及 ζ-演算、Coq和 OCaml。毫無疑問， ζ-演算是理解函數式編程語言的基礎和出發點，因此我們介紹相關的語法和歸約語義。雖然 ζ-演算適合理解函數式編程的一些核心思想，比如數據即函數，但是它的語法構造比較原始，即使表示一個數字，都要寫很長的 ζ-項，可讀性低，更不用提編寫程序。 Coq是離 ζ-演算比較接近但又能用於編寫一些可讀性較好的計算函數的編程語言，因此值得重點介紹。 Coq是用於講授歸納定義和歸納證明思想的出色工具，不過它的長處在於定理證明，若要深入講解，需要很大篇幅，因此最好留給專門的書籍，而在入門課程中只講解基本的證明方法。為滿足適合邏輯證明的需要， Coq只接受可終止的函數。這麼強的要求，決定它不可能用於日常編程。因此，最後我們介紹一門通用的編程語言 OCaml，除了基本的程序設計概念，我們還會討論一些比較高級的特徵。
本書共分 4章。
第 1章 ζ-演算。先概述 ζ-演算的起源，然後介紹不帶類型的 ζ-演算、簡單類型的 ζ-演算和 F系統。
第 2章 Coq。從函數式編程的角度介紹歸約規則、列表、多態列表、依賴類型、高階函數、柯里-霍華德關聯及余歸納類型等。
第 3章 OCaml。介紹基本的程序設計概念，例如數據類型與函數、控制結構、異常、模塊，以及函子和單子這樣比較高級的語言特徵。
第 4章部分習題參考答案。為前三章部分有難度的習題提供參考答案，方便感興趣的讀者自行學習。
本書由淺入深，從基礎原理到高級的語言特徵逐步介紹，具有通俗、系統、寬廣的特點，適合作為普通高等院校計算機科學和軟體工程專業的本科生教學參考書，同時也可作為軟體理論方向研究人員的入門讀物。
感謝傅育熙老師、陳鋼老師和曹欽翔老師對本書部分內容提出的寶貴意見。感謝清華大學出版社龍啟銘和常建麗兩位編輯在出版過程中給予的熱情幫助。本書由華東師範大學精品教材建設專項基金資助。
由於作者水平有限，書中的疏漏和不足之處在所難免，懇請廣大讀者及時指正！
鄧玉欣
2023年 5月上海