1 偏函数

在python中有时需要预加载某些函数的部分功能，此时偏函数的使用场景就出现了，那么这里我们了解一些偏函数基本知识。

图: 笛卡尔

1.1 偏函数定义

R 是集合 S 和 T 上的关系，则R被称为 S 到 T的偏函数， 如果总是有 (s, t1) ∈ R 和 (s, t2) ∈ R，则可以得到 t1 = t2。

如果此外还有，dom® = S，则称 R 为从 S 到 T 的全函数（或只是函数）。

1.2 偏函数dom定义

从 S 到 T 的偏函数 R 被定义在一个参数 s ∈ S， 如果 s ∈ dom®，否则未定义。
我们这样表示 f(x)↑，或 f (x) =↑ 表示“f 在 x 上未定义”，而 f (x)↓ 在 x 上表示“f 已定义”。

”在一些实现中，我们还需要定义可能在某些输入上失败的函数。

重要的是要将失败（这是一个合法的、可观察到的结果）与分歧区分开来；
一个可能失败的函数可以是部分的（即它也可能发散）或全部的（它必须总是返回结果或显式失败）——事实上，我们经常会有兴趣证明其结果的整体性。

当输入 x 时， 函数f 返回失败结果 时，我们写 f (x) = fail。
我们假设 fail 不属于 T，形式上，一个从 S 到 T 也可能失败的函数实际上是一个函数从 S 到 T ∪ {fail}。

2 使用场景

在实际使用中，比如编译器和解释器，评估关系的实现紧跟单步图 中的评估计算规则。

无类型计算评估函数中，正如我们所见，这些规则定义一个偏函数，当应用于一个还不是值的项时，产生该术语的下一步评估。

当应用于一个值时，评估函数的结果不会产生任何结果。

解释评估规则，我们需要决定如何处理这种情况。

一种直接的方法是编写单步评估函数eval1 以便在没有任何评估规则适用时引发异常
给它的期限。 （另一种可能性是让单步评估器返回一个术语选项，指示它是否成功，并且，如果是，给出结果项；

这也可以正常工作，但需要更多的信息记录。）当没有应用评估规则时，我们首先定义要引发的异常。

现在我们可以编写单步检查器本身。

	let rec eval1 t = match t with
	TmIf(_,TmTrue(_),t2,t3) →
	t2
	| TmIf(_,TmFalse(_),t2,t3) →
	t3
	| TmIf(fi,t1,t2,t3) →
	let t1’ = eval1 t1 in
	TmIf(fi, t1’, t2, t3)
	| TmSucc(fi,t1) →
	let t1’ = eval1 t1 in
	TmSucc(fi, t1’)
	| TmPred(_,TmZero(_)) →
	TmZero(dummyinfo)
	| TmPred(_,TmSucc(_,nv1)) when (isnumericval nv1) →
	nv1
	| TmPred(fi,t1) →
	let t1’ = eval1 t1 in
	TmPred(fi, t1’)
	| TmIsZero(_,TmZero(_)) →
	TmTrue(dummyinfo)
	| TmIsZero(_,TmSucc(_,nv1)) when (isnumericval nv1) →
	TmFalse(dummyinfo)
	| TmIsZero(fi,t1) →
	let t1’ = eval1 t1 in
	TmIsZero(fi, t1’)
	| _ →
	raise NoRuleApplies

请注意，我们从几个地方构建术语从头开始，而不是重新组织现有术语。由于这些新术语确实在用户的原始源文件中不存在，他们的信息注释没有用。

常量 dummyinfo 在此类术语中用作信息注释。
变量名 fi（用于“文件信息”）始终用于匹配模式中的信息注释。

在 eval1 的定义中要注意的另一点是显式 when模式中的子句以捕获元变量名称（如 v 和 nv）的影响。

在下图中的评估关系表示中。

在里面用于评估的子句，例如，模式的语义将允许 nv1 匹配任何术语，这不是我们想要的；

添加 when (isnumericval nv1) 限制规则只有当 nv1匹配的术语实际上是一个数值时，它才能触发。

（如果我们愿意，我们可以用相同的风格重写原始推理规则作为 ML 模式，将由元变量产生的隐式约束将名称转换为规则上的显式附加条件）

t1 is a numeric value   
-------------------------------- (E-PredSucc)
pred (succ t1) - → t1

这是以紧凑性和可读性为代价。
最后，eval 函数接受一个项并通过重复调用 eval1 来找到它的范式。

每当 eval1 返回一个新术语 t0 时，我们对 eval 进行递归调用以继续从 t0 进行评估。

当 eval1 最终达到在没有规则适用的地方，它会引发异常 NoRuleApplies，导致eval跳出循环并返回序列中的最后一项。

let rec eval t =
try let t’ = eval1 t
in eval t’
with NoRuleApplies → t

显然，这个简单的评估器经过调整以便与评估的数学定义，不是为了尽可能快速找到范式。
一个更有效的算法可以通过启动取而代之的是“大步”评估规则。

3 在解释器语言规则的应用

解释器或编译器有很多部分——即使是非常一个简单的——除了我们在这里明确讨论过的那些。 实际上，语言规则要评估的开始是文件I/O流中的字符序列。

他们必须是从文件系统读取，由词法分析器处理成标记流，并由解析器进一步处理成抽象语法树，之前它们实际上可以通过我们看到的函数来评估。 此外，评估后，需要将结果打印出来。

file I/O      --> chars  
/lexing      --> tokens
/parsing     --> terms 
/evaluation   -->values 
/printing

鼓励有兴趣的读者看看在线的代码对于整个解释器，是否基于以下基本流程.

为了简单起见，我们以这种方式编写 eval，但是将 try 处理程序放在递归中loop 在 ML 中实际上并不是很好的样式。

在前面的实现章节中，我们有实际实现的经验，其应用形式如下：