函数定义和值
:material-circle-edit-outline: 约 351 个字 :material-clock-time-two-outline: 预计阅读时间 1 分钟
一阶函数
ED 语言
函数代换
高阶函数
EF 语言
\(arr(,)\) 用于指示一个函数的类型，第一个为输入，第二个为输出
上面的 lam 就是函数，大括号是参数类型，小括号是输入与表达式
[!EXAMPLE] reduction
answer: x
高阶递归的系统 T
全函数与部分函数
a 输入给 f 能有非空输出，就记作 \(f(a) \downarrow\)
全函数 Total function
对于集合 \(A\)，一个函数 \(f\) 能作用在 \(A\) 中任意元素上得到 B 中的元素，那这个 \(f\) 就是 \(A\) 上的全函数，即，任意 a 属于 A，有 \(f(a) \downarrow\)
记作 \(f:A\rightarrow B\)
说白了就是函数定义域里面每个元素都有对应的输出，就是我们之前理解的函数
部分函数 Partial function
输出可能是空集的函数，这意味着部分函数可能不会终止，例如：
n 为偶数情况下，这个函数无法终止
比较重要，看智云和笔记 编程语言原理（本）2024-11-06 第 7-8 节
System T （T 语言）
重点关注 rec
第一个 \(e_0\) 的位置是指基本情形会输出 \(e_0\)
后面就是，上一轮递归结果 y 以及 succ(x) 带入 \(e_1\) 算出本轮迭代的结果
静态语义
动态语义
