转载

Hypothetical Judgments 和 Hypothetical Inductive Definitions

Hypothetical Judgements

之前一篇介绍了 Judgements和Inductive Definition ，这里通过给Judgements加上一些关系，同时扩展下Inductive Definition。

Derivability

Derivability指的是说，由某几个Judgements可以推导出某个Judgement。具体如下 /[J_1,...,J_n/vdash_R J/] 这个式子的意思就是说，由 /(J_1,...,J_n,R/) 我们可以推导出 /(J/) 成立。这里 /(R/) 是公理集合，而 /(J_i/) 是临时公理。这个意思是说，当我们承认 /(J_i/) 成立的时候，我们可以推导出 /(J/) 。举个例子 /(potato~nat/vdash succ(potato)~nat/) 。这里当我们知道土豆是一个自然数的时候，那么我们可以推导出来 /(succ(potato)/) 也是个自然数。但是反过来是不行的： /(succ(potato)~nat/vdash potato~nat/) 是不成立的。因为我们没办法推导出来这个结论。

Derivability有几个性质：

Weakening: 是说，如果 /(/Gamma/vdash J/) ，并且 /(/Gamma/subseteq/Gamma'/) ，那么我们有 /(/Gamma'/vdash J/) 。这个不难理解，当我们已经知道某个结论的时候，如果放宽要求，那么这个结论还是成立的
Reflexibility: /(J/vdash J/) ，是说自己可以推导出自己
Transitivity: 是说如果 /(/Gamma/vdash J/) 和 /(/Gamma, J/vdash J'/) 成立，那么 /(/Gamma/vdash J'/) 也是成立的。直觉上看就是 /(A/) 可以推导出 /(B/) ，同时 /(B/) 可以推导出 /(C/) ，那么我们可以直接从 /(A/) 推导到 /(C/) 。

Admissibility

Admissibility指的是说，如果某个假设成立，那么我们可以得到某个结论。具体如下 /[J_1,..,J_n/vDash_R J/] 。这里 /(J_1,...,J_n/) 是假设， /(R/) 是公理集合，而 /(J/) 是结论。换句话说，如果我们可以通过公理 /(R/) 推导出结论 /(J_1,...,J_n/) ，那么我们也可以推导出 /(J/) 。形式化表示出来是

/[ /begin{aligned} &/frac{}{J_1'}~/frac{}{J_2'}~...~/frac{}{J_n'}// &/frac{J_1,...,J_n}{J} /end{aligned} /]

这里

/(R=/{/frac{}{J_1'},...,/frac{}{J_n'}/}/)

。

下面举个例子: /(succ(a)~even/vDash a~odd/) 。意思就是，如果 /(succ(a)/) 是一个偶数，那么 /(a/) 就是一个奇数。

Admissibility和Derivability对比

这两个概念很容易混淆，所以这里再说一次

/(J_1,..,J_n/vdash_R J/) 是说，通过 /(/{J_1,..,J_n/}/cup R/) ，我们可以推出 /(J/)
/(J_1,..,J_n/vDash_R J/) 是说，如果 /(J_1,..,J_n/) 成立，那么我们可以由 /(R/) 推出 /(J/)

还是不理解是不是？不要慌，让我们看下下面的例子：

/(succ(potato)~nat /nvdash ~potato~nat/)
/(succ(potato)~nat /vDash ~potato~nat/)

这里再复习下什么是 /(nat/) ，具体可以看上一篇文章。

/[ /frac{}{z~/mathtt{nat}}~/frac{a~/mathtt{nat}}{/mathtt{succ}(a)~/mathtt{nat}} /]

/(nat/) 是递归定义的，也就是说，首先定义 /(z/) 是一个 /(nat/) 。然后如果 /(a/) 是 /(nat/) ，那么 /(succ(a)/) 也是 /(nat/) 。这两条我们可以看成是上面所说的公理集合 /(R/) 。然后对于例子1，也就是说我们在公理集合里面加入 /(/frac{}{/mathtt{succ}(potato)~/mathtt{nat}}/)

是没办法推导出

/(potato~nat/)

的。

但是对于例子2，确是成立的。证明方法其实在上一章已经说过了，这里不再重复。

不过我们可以证明 /(/Gamma/vdash_R J/Rightarrow /Gamma/vDash_R J/) 。证明也很简单，如果我们可以通过 /(R/) 推导出 /(/Gamma/) 也就是 /(/vdash_R/Gamma/) ，那么我们就可以通过 /(R/) 推导出 /(J/) 也就是 /(/vdash_R J/) （通过Transitivity: /(/vdash_R /Gamma, /Gamma/vdash_R J/) ）。如果 /(/vdash_R/Gamma/) 不成立，那么说明 /(/Gamma/vDash_R J/) "天然"成立。

同时，Admissibility也有类似于Derivability的性质:

Reflexibility: /(J/vDash_R J/)
Transitivity: 如果 /(/Gamma/vDash_R K/) 并且 /(/Gamma,K/vDash_R J/) 那么我们有 /(/Gamma/vDash_R J/)
Weakening: 如果 /(/Gamma/vDash_R J/) 那么 /(/Gamma,K/vDash_R J/)

Hypothetical Inductive Definitions

然后让我们把Hypothetical Judgement给整合到Inductive Definitions里面：

/[ /frac{/Gamma/Gamma_1/vdash J_1~/Gamma/Gamma_2/vdash J_2~...~/Gamma/Gamma_n/vdash J_n}{/Gamma/vdash J} /]

这里 /(/Gamma/) 是一个全局假设，也可以看做就是全局的公理，而 /(/Gamma_i/) 称为局部假设或者局部公理。这个表示当 /(J_i/) 在假设 /(/Gamma/) 和 /(/Gamma_i/) 的情况下成立，那么由 /(/Gamma/) 则可以推导出 /(J/) 。具体的在后面介绍具体的类型系统的时候可以体会到。

General Judgement因为目前用不到，所以这里不做介绍。

下一次介绍Statistics、Dynamics和Safety然后我们定义一个类型系统所需要的所有工具就都齐全了。有写错的或者不懂的欢迎留言。

原文 http://www.cnblogs.com/esing/p/5057095.html

正文到此结束