函数式程序设计

图书标准信息

• 作者 邓玉欣
• 出版社 清华大学出版社
• 出版时间 2023-07
• 版次 1
• ISBN 9787302626909
• 定价 39.00元
• 装帧 其他
• 开本 16开
• 纸张 胶版纸
• 页数 124页
• 字数 179千字

【内容简介】

在内容选取上，本讲义只涉及 λ-演算，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