指称语义学

第1章 引论

第2章 指称语义学

第3章 二进制数码

第4章 第一级函数

第5章 $\lambda$演算

第5.1节 $\lambda$演算

第5.2节 递归定义

第6章 格与域

前一章最后的讨论已经指出如果我们想要成功地找到一个$\lambda$演算的语义理论, 那么我们就必须找出一种限制我们能够考虑的函数类的方法. 否则的话, 就太多了而不能找到任何具有同构函数空间的非平凡的空间.

逻辑学家的通常解决方案是压根不与函数打交道, 换而与函数的表示打交道. 简而言之, 他们用哥德尔配数. 他们通常处理整数上的函数, 在这种情况下哥德尔配数操作将可用有限长度的算法表达的函数 (构成了一个可数集) 映射至整数. 当他们想要考虑以函数$B$作为参数的函数$A$时, 他们可以形式化地给$A$提供$B$的哥德尔配数.

第6.1节 近似序

不使用算法的哥德尔配数, 那么我们将采用另一种方式, 这种方式更加关注于函数或者说映射本身. 让我们通过观察我们的问题的另一方面来获得一点直觉, 即多重不动点的麻烦. 考虑递归函数:$$\begin{array}{cc}f=\lambda x.& \mathtt{\text{if }}x=0\mathtt{\text{ then }}1\hfill \\ & \mathtt{\text{else if }}x=1\mathtt{\text{ then }}f(3)\hfill \\ & \mathtt{\text{else }}f(x-2)\mathtt{\text{.}}\hfill \end{array}$$我们知道我们在寻找$$\begin{array}{cc}\lambda f.\lambda x.& \mathtt{\text{if }}x=0\mathtt{\text{ then }}1\hfill \\ & \mathtt{\text{else if }}x=1\mathtt{\text{ then }}f(3)\hfill \\ & \mathtt{\text{else }}f(x-2)\mathtt{\text{.}}\hfill \end{array}$$的不动点. 我们对于递归函数的实际经验或许会将我们引向解$$f^{\prime }(x)=\{\begin{array}{cc}1& (x\mathtt{\text{ even}})\hfill \\ \mathtt{\text{undefined}}& (x\mathtt{\text{ odd}})\hfill \end{array}$$但是$$f_1(x)=1$$或者更一般的$$f_a(x)=\{\begin{array}{cc}1& (x\mathtt{\text{ even}})\hfill \\ a& (x\mathtt{\text{ odd}})\hfill \end{array}$$也是解, 其中$a$是任意的常数. 那么为什么$f^{\prime }$是实践中的计算机实现会提供的函数呢?

答案在于其他的解都包含了我们不希望实现去决定的任意的信息 ($a$的值). 另一方面, $f^{\prime }$仅包含递归定义实际传达的信息. 它是我们所需要的最小的解, 即包含最少信息量的解. 让我们现在来形式化这个根据信息量对于值进行排序的想法.

为了看明白这个序是如何运作的, 让我们先来看看一个比函数更简单的值的集合. 考虑一种对于实数进行近似的可能方式, 即闭区间, 记作$[\underset{\_}{x},\bar{x}]$其中$\underset{\_}{x}$和$\bar{x}$是实数, 并且$\underset{\_}{x}\le \bar{x}$. 想法在于绝对精确的值介于这两值之间.

令$x=[\underset{\_}{x},\bar{x}]$而$y=[\underset{\_}{y},\bar{y}]$. 如果$\underset{\_}{y}\le \underset{\_}{x}$且$\bar{x}\le \bar{y}$, 那么$x$与$y$一致, 但是更加精确. 我们或许可以将其记作$y⊑x$, 意思在于$x$比$y$更精确 (或者说至少不更不精确), $x$比$y$包含更多 (或者相等) 的信息, 但是$x$中没有任何会与$y$相冲突的信息.我们看到在以上图片中, 有$x⊑z$和$y⊑z$, 但是$x$和$y$是不可比较的. 实际上, $z$是将$y$和$z$的所有信息合并了: 我们称$z$是$x$和$y$的最小上界, 记作$z=y\bigsqcup z$.

存在一些特殊的情形. 一种是区间$[-\infty ,\infty ]$, 整个实轴. (?或许应该称为扩展实轴) 这压根就没有给出任何信息, 它比任何其他可能给出的信息都要弱, 我们称其为$\perp$. 另一种特别的情况是包含不一致的信息, 例如$[0,1]\bigsqcup [2,3]$, 我们称其为$\top$. 因此, $\perp$代表信息的缺失, 而$\top$代表信息太多, 以至于产生了矛盾的地步. 其他某些值集可能更容易根据信息进行排序. 例如, 两个真值之间是无法比较的, 于是如果我们添加$\perp$和$\top$以代表欠定和过定的真值, 那么我们就得到了下图所呈现的内容.

第6.2节 偏序集

下图呈现了一些例子.

1. 整数集, 序为$\le$.
2. 非负整数集, 序为$\le$.
3. $12$的因子集, 以整除性排序.
4. 三元素集的幂集, 序为$\subseteq$.

第6.3节 完全格

第6.4节 格上的函数

第6.5节 一个不动点算子

第7章 自反域

第8章 $\lambda$演算的形式语义