函数式程序设计 / 2024秋

课程简介

函数式程序设计是一种具有悠久历史的程序设计方法。在几十年以来的大多数时间中，函数式程序设计栖身于象牙塔内，慢慢成长，积蓄力量，并没有在软件开发实践中得到广泛使用。世异时移，这种情况正在发生变化。随着软件系统复杂性的不断提高以及软件与现实世界关系的日益紧密，如何严格确保软件系统的正确性和可靠性，逐渐成为一个重要的现实问题。函数式程序设计建立在严格的数学概念的基础上，具有良好的数学性质，为上述问题提供了一种现实可行的解决方案。目前，大多数的主流程序设计语言都在逐渐引入函数式程序设计的各种成分。本课程将系统介绍函数式程序设计的基本思想、核心概念、以及相关的程序设计方法和程序推理方法，为学生从事算法设计、程序语言设计、软件开发等领域的研究和实践工作建立坚实的理论基础。

课程信息

理论课程：第二教学楼 413；每周周三5~6节、每周周五3~4节
上机实习：理科一号楼 1235；每周周五5~6节

课程大纲

课程基本目的

培养学生使用函数式思维进行程序设计和推理的基本能力，了解函数式程序设计语言的基本运行原理，熟练使用Haskell语言及相关工具进行程序设计与调试，并能使用 Agda 语言对函数式程序进行推理和变换。

内容提要

1. 函数式程序设计导引
   1. 课程介绍
   2. 函数式思维介绍
2. Haskell程序设计语言
   1. Haskell语言入门
   2. Type and type class
   3. List comprehension
   4. Recursive function
   5. Higher-order function
   6. Declaring types and classes
   7. Interactive programming
   8. Monads
   9. Lazy evaluation
3. 函数式程序推理与演算
   1. Agda定理证明器入门
   2. 程序演算概要
   3. Theory of Lists
   4. Theory of Generic Data Types
   5. 程序演算的应用
4. 计算机技术专题讲座（全年级所有《计算概论A》选课同学集中上课）

教学方式

本课程的教学方式涉及两个方面：课堂讲授、上机实习。其中，在课堂讲授环节，主要由授课教师对课程内容进行讲解，并根据课程进度布置课后作业（课后作业包括每周一次的习题作业，以及一次定理证明的大作业）。在上机实习环节，主要由学生对课堂授课内容进行实际操作，并完成课后作业。

往年课程

• 2021秋
• 2022秋
• 2023秋
• 2024秋

任课教师

胡振江
教授

张伟
副教授

课程助教

黄柘铳
willhuang@stu.pku.edu.cn

曹奕远
cyy9447@pku.edu.cn