在内容选取上,本讲义只涉及 λ-演算,Coq 和 OCaml。毫无疑问,λ-演 算是理解函数式编程语言的基础和出发点,因此在第一章我们介绍不带类型 的 λ-演算和简单类型的 λ-演算,主要讨论语法和 β-规约语义。虽然 λ-演算适 合理解函数式编程的一些核心思想,比如数据即函数,但是它的语法构造比较原始,即使表示一个数字都要写很长的 λ 项,可读性低,更不用提编写程序。 Coq 是离 λ-演算比较接近但又能用于编写一些可读性较好的计算函数的编程 语言,因此在第二章我们介绍 Coq,重点是从函数式编程的角度展开讨论,内 容涉及自然数函数、列表、多态数据结构、高阶函数以及柯里-霍华德关联。作 者认为 Coq 是来用于讲授归纳定义和归纳证明思想的出色工具。虽然 Coq 的 长处在于定理证明,但是深入讲解需要很大篇幅,因此最好留给专门的书籍, 不适合在入门课程的讲义中展开。为满足适合逻辑证明的需要,Coq 只接受可 终止的函数。这么强的要求决定它不可能用于日常编程。因此,在第三章我们 介绍一门通用的编程语言 OCaml,除了基本的程序设计概念,我们还会讨论 函子和 Monad 这样比较高级的特征。讲义中选取了一些练习题,希望通过做练习加强 对基本概念的理解。第四章提供了部分习题的参考答案,以方便感兴趣的读者 自行学习。本讲义可作为高等院校计算机科学或软件工程专业的本科教学参 考书。
1.一本专门介绍函数式程序设计基本思想和方法的入门级读物。 2.循序渐进,从基础原理到高级的语言特征逐步介绍,具有通俗、系统、宽广的特点。 3.学习门槛低,适合不具备相关知识基础的初学者阅读和理解。 4.习题丰富,并对部分有难度的习题给出参考答案,照顾不具备课堂学习条件的读者自行学习。 5.适合作为普通高等院校计算机科学和软件工程专业的本科生教学参考书。
- 版权: 清华大学出版社
- 出版: 2023-07-01
- 更新: 2024-09-27
- 书号:9787302626909
- 中图:TP311.1
- 学科:工学控制科学与工程工学计算机科学与技术