正版现货新书 函数式程序设计 9787302626909 邓玉欣

提到计算机编程语言，很多人只听说过流行的语言，如 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月上海

在内容选取上，本讲义只涉及 λ-演算，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的程序委员会委员。

第 1章 ζ-演算 .1 

1.1 ζ-演算的起源1 

1.2不带类型的 ζ-演算2 

1.2.1语法 3 

1.2.2船-等价 .4 

1.2.3替换 6 

1.2.4 (-归约 .7 

1.2.5表达能力9 

1.2.6不动点 .12 

1.2.7其他数据类型 .13 

1.2.8邱奇-罗索定理 14 

1.2.9归约策略15 

1.3简单类型的 ζ-演算16 

1.3.1简单类型的项 .16 

1.3.2归约 19 

1.3.3正规化 .20 

1.4 F系统 .21 

1.4.1语法 21 

1.4.2语义 22

第 2章 Coq 24 

2.1基本的函数式编程.24 

2.2归约规则 31 

2.3列表.33 

2.4规则归纳 39 

2.5多态列表 40 

2.6依赖类型 42 

2.7高阶函数 43 

2.8柯里-霍华德关联.45 

2.9归纳证明 47 

2.10常用证明策略50 

2.11证明自动化 .53 

2.12余归纳类型 .55 

2.13代码抽取 62 

函数式程序设计
第 3章 OCaml .65 

3.1安装和使用 OCaml .65 

3.2数据类型与函数 66 

3.3控制结构 78 

3.4高阶函数 82 

3.5记忆.84 

3.6异常.85 

3.7排序.86 

3.8队列.87 

3.9模块.90 

3.10函子 .92 

3.11单子 .94

第 4章部分习题参考答案 98 

4.1第 1章练习题.98 

4.2第 2章练习题.99 

4.3第 3章练习题. 106

参考文献  112

索引. 113 

在内容选取上，本讲义只涉及 λ-演算，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的程序委员会委员。