函数式程序设计

[图书] - 邓玉欣 - 清华大学出版社 - 2023

在内容选取上，本讲义只涉及 λ-演算，Coq 和 OCaml。毫无疑问，λ-演 算是理解函数式编程语言的基础和出发点，因此在第一章我们介绍不带类型 的 λ-演算和简单类型的 λ-演算，主要讨论语法和 β-规约语义。虽然 λ-演算适 合理解函数式编程的一些核心思想，比如数据即函数，但是它的语法构造比较原始，即使表示一个数字都要写很长的 λ 项，可读性低，更不用提编写程序。 Coq 是离 λ-演算比较接近但又能用于编写一些可读性较好的计算函数的编程 语言，因此在第二章我们介绍 Coq，重点是从函数式编程的角度展开讨论，内 容涉及自然数函数、列表、多态数据结构、高阶函数以及柯里-霍华德关联。作 者认为 Coq 是来用于讲授归纳定义和归纳证明思想的出色工具。虽然 Coq 的 长处在于定理证明，但是深入讲解需要很大篇幅，因此最好留给专门的书籍， 不适合在入门课程的讲义中展开。为满足适合逻辑证明的需要，Coq 只接受可 终止的函数。这么强的要求决定它不可能用于日常编程。因此，在第三章我们 介绍一门通用的编程语言 OCaml，除了基本的程序设计概念，我们还会讨论 函子和 Monad 这样比较高级的特征。讲义中选取了一些练习题，希望通过做练习加强 对基本概念的理解。第四章提供了部分习题的参考答案，以方便感兴趣的读者 自行学习。本讲义可作为高等院校计算机科学或软件工程专业的本科教学参 考书。