zoukankan      html  css  js  c++  java
  • Hypothetical Judgments 和 Hypothetical Inductive Definitions

    Hypothetical Judgements

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

    Derivability

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

    Derivability有几个性质:

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

    Admissibility

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

    [egin{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)~evenvDash a~odd)。意思就是,如果(succ(a))是一个偶数,那么(a)就是一个奇数。

    Admissibility和Derivability对比

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

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

    还是不理解是不是?不要慌,让我们看下下面的例子:

    • (succ(potato)~nat vdash ~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,确是成立的。证明方法其实在上一章已经说过了,这里不再重复。

    不过我们可以证明(Gammavdash_R JRightarrow GammavDash_R J)。证明也很简单,如果我们可以通过(R)推导出(Gamma)也就是(vdash_RGamma),那么我们就可以通过(R)推导出(J)也就是(vdash_R J)(通过Transitivity: (vdash_R Gamma, Gammavdash_R J))。如果(vdash_RGamma)不成立,那么说明(GammavDash_R J)"天然"成立。

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

    • Reflexibility: (JvDash_R J)
    • Transitivity: 如果(GammavDash_R K)并且(Gamma,KvDash_R J)那么我们有(GammavDash_R J)
    • Weakening: 如果(GammavDash_R J)那么(Gamma,KvDash_R J)

    Hypothetical Inductive Definitions

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

    [frac{GammaGamma_1vdash J_1~GammaGamma_2vdash J_2~...~GammaGamma_nvdash J_n}{Gammavdash J} ]

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

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

  • 相关阅读:
    Apache Ant 1.9.1 版发布
    Apache Subversion 1.8.0rc2 发布
    GNU Gatekeeper 3.3 发布,网关守护管理
    Jekyll 1.0 发布,Ruby 的静态网站生成器
    R语言 3.0.1 源码已经提交到 Github
    SymmetricDS 3.4.0 发布,数据同步和复制
    beego 0.6.0 版本发布,Go 应用框架
    Doxygen 1.8.4 发布,文档生成工具
    SunshineCRM 20130518发布,附带更新说明
    Semplice Linux 4 发布,轻量级发行版
  • 原文地址:https://www.cnblogs.com/esing/p/5057095.html
Copyright © 2011-2022 走看看