CMU 15-150笔记

主要是对于CMU 15-150课程的幻灯片等材料的翻译.

第1章求值和定型, 绑定和作用域

第1.1节引入

今天我们给出了课程的大纲及其目标, 包括引用透明, 外延等价, 以及并行. 我们从观察其类型开始探索SML语言.

关键概念

计算是函数式的
编程作为阐释性的过程
类型, 值, 表达式
定型规则和求值规则
integer, real, boolean, product
并行, work, span
外延等价

第1.2节幻灯片

第1.2.1小节课程哲学

计算是函数式的
编程是阐释性的语言过程

第1.2.2小节计算是函数式的

值相对于类型被分类
表达式{译注: 也有类型}
函数将值映射为值

第1.2.3小节命令式 vs. 函数式

命令	表达式
被执行	被求值
具有副作用	无副作用
`x := 5`	`3 + 5`
(新状态)	(新值)

第1.2.4小节编程作为阐释

问题陈述
- 不变量
- 规格
- 正确性证明
分析, 分解和适应, 证明

第1.2.5小节并行

\begin{matrix} ⟨ 1, 0, 0, 1, 1 ⟩ & \to & 3 \\ ⟨ 1, 0, 1, 0, 1 ⟩ & \to & 3 \\ ⟨ 1, 1, 0, 1, 1 ⟩ & \to & 4 \\ ⟨ 0, 0, 0, 1, 1 ⟩ & \to & 2 \\ ↓ \\ 12 \end{matrix}

sum: int sequence -> int
type row = int sequence
type room = row sequence
fun count (class: room): int = sum (map sum class)

第1.2.6小节分析

做这个计算需要多长时间?
如何改进count的运行时间?
分而治之

第1.2.7小节代价分析

work

顺序计算
总顺序时间; 操作数目

span

并行计算
在可用处理器数目不受限制时的所需时间; 最长关键 (critical) 路径的长度

第1.2.8小节介绍ML

类型 $t$
表达式 $e$
值 $v$ (作为表达式的子集)

第1.2.9小节例子

     (3 + 4) * 2
=1=> 7 * 2
=1=> 14

     (3 + 4) * (2 + 1)
=3=> 21

如果使用并行, 第二个需要多少步骤?

    "the " ^ "walrus"
==> "the walrus"

"the walrus" ^ 1
ill-typed

SML从不会求值病态类型表达式!

第1.2.10小节类型, 表达式, 值

类型是对于表达式的值的预测, 如果表达式最终确有一个值的话 {译注: 求值过程可能因为无限进行而发散}
一个表达式是良类型的, 如果其至少具有一个类型, 否则就是病态类型的.
良类型表达式具有一个类型, 可能具有一个值, 可能具有一个副作用 (但是现在的effect-free部分当然是没有的)

每个良形式的ML表达式 $e$

具有类型 $t$ , 记作 $e : t$
可能具有一个值, 记作 $e ↪ v$ , 或者 $e ⟹ v$
可能具有一个副作用 (但是现在的effect-free部分当然是没有的)

例子:

(3 + 4) * 2 : int

(3 + 4) * 2 ==> 14

{译注: 结合前文, 看起来 $⟹$ 是归约关系而非求值至的关系.}

第1.2.11小节 ML中的类型

基本类型
- int, real, bool, char, string
构造类型
- 积类型
- 函数类型
- 用户定义的类型

第1.2.12小节整数(类型), 表达式

类型: int
值: ..., ~1, 0, 1, ...
表达式: $e_{1}$ + $e_{2}$ , $e_{1}$ - $e_{2}$ , $e_{1}$ * $e_{2}$ , $e_{1}$ div $e_{2}$ , $e_{1}$ mod $e_{2}$ , ...
例子: ~4 * 3

第1.2.13小节整数, 定型

定型规则
- $n$ : int
- $e_{1}$ + $e_{2}$ : int, 如果 $e_{1}$ : int且 $e_{2}$ : int
- 其他运算也是类似的

(3 + 4) * 2 : int
because (3 + 4): int and 2: int
(3 + 4): int because 3: int and 4: int

第1.2.14小节整数, 求值

第2章函数

第2.1节引入

第2.2节幻灯片

第2.2.1小节上次内容

类型, 表达式, 值
外延等价
声明

第2.2.2小节今天的目标

编写匿名函数 (lambda表达式)
声明有名字的函数
陈述什么是一个函数闭包
对于牵涉函数应用的表达式进行求值
使用模式
- clausal的函数声明
- case表达式

第2.2.3小节声明

val     pi :       real = 3.14
keyword identifier type   value

这引入了一个绑定, 将pi绑定至3.14, 也可以写成[3.14/pi]. {译注: 其实就是替换的写法.}

词法静态作用域 (lexically statically scoped)

第2.2.4小节绑定

val x : int = 8 - 5 [3/x] 
val y : int = x + 1 [4/y]

第2.2.5小节绑定

第3章递归和归纳

第4章列表上的递归和结构归纳, 尾递归

第5章数据类型, 树上的递归和结构归纳

我们将数据类型声明作为抽象形式引入, 其旨在将程序员从跟踪低级hacking约定的细节之中解放出来.

我们考虑了预先定义了的数据类型int option, 其有一个常量构造子None和一个非常量构造子Some, 其接受一个i : int以构造出Some i : int option. 我们也作成了一些我们自己的数据类型, 包括用于模拟颜色的类型, 多返回值类型, 以及一个二叉树类型.

我们展示了如何使用结构归纳证明关于树的定理.

关键概念

数据类型声明
常量构造子
接受参数的构造子
递归定义类型
树类型

CMU 15-150笔记

第1章求值和定型, 绑定和作用域

第1.1节引入

第1.2节幻灯片

第1.2.1小节课程哲学

第1.2.2小节计算是函数式的

第1.2.3小节命令式 vs. 函数式

第1.2.4小节编程作为阐释

第1.2.5小节并行

第1.2.6小节分析

第1.2.7小节代价分析

第1.2.8小节介绍ML

第1.2.9小节例子

第1.2.10小节类型, 表达式, 值

第1.2.11小节 ML中的类型

第1.2.12小节整数(类型), 表达式

第1.2.13小节整数, 定型

第1.2.14小节整数, 求值

第2章函数

第2.1节引入

第2.2节幻灯片

第2.2.1小节上次内容

第2.2.2小节今天的目标

第2.2.3小节声明

第2.2.4小节绑定

第2.2.5小节绑定

第3章递归和归纳

第4章列表上的递归和结构归纳, 尾递归

第5章数据类型, 树上的递归和结构归纳

第6章渐进分析

第7章渐进分析

第8章排序列表

第9章多态和类型推导

第10章高阶函数

CMU 15-150笔记

第1章 求值和定型, 绑定和作用域

第1.1节 引入

第1.2节 幻灯片

第1.2.1小节 课程哲学

第1.2.2小节 计算是函数式的

第1.2.3小节 命令式 vs. 函数式

第1.2.4小节 编程作为阐释

第1.2.5小节 并行

第1.2.6小节 分析

第1.2.7小节 代价分析

第1.2.8小节 介绍ML

第1.2.9小节 例子

第1.2.10小节 类型, 表达式, 值

第1.2.11小节 ML中的类型

第1.2.12小节 整数(类型), 表达式

第1.2.13小节 整数, 定型

第1.2.14小节 整数, 求值

第2章 函数

第2.1节 引入

第2.2节 幻灯片

第2.2.1小节 上次内容

第2.2.2小节 今天的目标

第2.2.3小节 声明

第2.2.4小节 绑定

第2.2.5小节 绑定

第3章 递归和归纳

第4章 列表上的递归和结构归纳, 尾递归

第5章 数据类型, 树上的递归和结构归纳

第6章 渐进分析

第7章 渐进分析

第8章 排序列表

第9章 多态和类型推导

第10章 高阶函数

第1章求值和定型, 绑定和作用域

第1.1节引入

第1.2节幻灯片

第1.2.1小节课程哲学

第1.2.2小节计算是函数式的

第1.2.3小节命令式 vs. 函数式

第1.2.4小节编程作为阐释

第1.2.5小节并行

第1.2.6小节分析

第1.2.7小节代价分析

第1.2.8小节介绍ML

第1.2.9小节例子

第1.2.10小节类型, 表达式, 值

第1.2.12小节整数(类型), 表达式

第1.2.13小节整数, 定型

第1.2.14小节整数, 求值

第2章函数

第2.1节引入

第2.2节幻灯片

第2.2.1小节上次内容

第2.2.2小节今天的目标

第2.2.3小节声明

第2.2.4小节绑定

第2.2.5小节绑定

第3章递归和归纳

第4章列表上的递归和结构归纳, 尾递归

第5章数据类型, 树上的递归和结构归纳

第6章渐进分析

第7章渐进分析

第8章排序列表

第9章多态和类型推导

第10章高阶函数