递归函数的系统 PCF
:material-circle-edit-outline: 约 632 个字 :material-clock-time-two-outline: 预计阅读时间 2 分钟
9 递归系统 PCF.pdf 编程语言原理（本）2024-11-13 第 7-8 节
PCF 是一种表示程序设计可计算函数的语言，是 ⼀ 个基于 \(\lambda\) 演算的类型化的函数式语 ⾔
PCF 语法
每个 PCF 表达式都具有一个唯一的类型，因此可以通过列出其类型来概括 PCF 的构造
只要看到这个表达式长什么样子，就能确定其是什么类型
基本类型为 nat、bool 和 arr
只有满 ⾜ 特定类型求取约束的表达式才被认为是该语 ⾔ 的部分
[!EXAMPLE]
true+1：不符合
x+5：仅当x为nat时成 ⽴
布尔值和 ⾃ 然数
- 基本的条件表达式 ： if < 布尔值 > then < 值 > else < 值 >
- 相等测试 Eq? 作用在 自然数 上，返回 布尔值
- Eq? 5 6
- if < 布尔值 > then < ⾃然数 > else < ⾃然数 >
- 是一个自然数表达式
- if < 布尔值 > then 3 else true
- 是错的
- if < 布尔值 > then λx: nat.M else λx: nat.N
- 是 arr 表达式
BNF 表示的基本表达式
等式公理
废话
每种类型的条件表达式的两个公理模式:
- if true then M else N = M
- if false then M else N = N
存在 ⽆ 限多个相等性测试的公理，确定如下:
- Eq? n n = true, 对每个数 n
- Eq? m n = false, m 与 n 为互异的数
操作语义
归约规则：通过从左到右读取 ⼀ 个等式公理 ⽽ 获取的基本归约“规则”
redex：与 ⼀ 个归约公理左边相匹配的项（还可以再被规约），与 normal form 相对
例如：
if Eq? (6+5) 17 then (1+1) else 27
为了得到结果，(6+5)必须得做，(1+1)却不一定需要
⼆ 元组（序偶）
PCF 支持积类型，不能支持和类型
看 PPT 吧。。。
数值函数的构造
在 PCF 中，数值函数不仅仅是简单的 ⾃ 然数之间的映射，PCF 语 ⾔ 通过递归和组合等机制可以定义复杂的数值函数
- 递归函数：PCF 中允许定义递归 ⾃ 然数函数，例如阶乘函数，这些递归函数能够根 据基本的 ⾃ 然数表达式（如加法、乘法、递归调 ⽤ 等）构造复杂的数值函数。
- ⾼ 阶函数：PCF 中还 ⽀ 持 ⾼ 阶函数，这意味着可以将 ⾃ 然数的 函数作为参数 传递给其他函数，从 ⽽ 构造更复杂的数值操作
隐式定义
数值函数 f(n) = n+5 隐式地被 x+5 表达式定义
if x then false else true 隐式定义了否定
if x then y else false
if x then true else y
参数分离（柯里化）
例题
