zoukankan      html  css  js  c++  java
  • Inductive Definitions

    背景呢还是背景呢

    这学期学了一门Type System and Programming Language,感觉是一门很有意思的课。虽然讲的是编程语言,但是很多思想其实工作的时候可能也会用的到。记得老师有一节课说:『你们现在不学习(PL),以后就不会学了。这是你们多数人唯一的机会了』。这门课有个本科生版本的Principles of Programming Languages,多了些写代码的作业,少了点证明,可惜Fall不开。教材是老师自己写的Practical Foundations for Programming Languages,这里只写下我自己的理解,有错了欢迎讨论。

    Judgement 和 Inference Rule

    一个Judgement就是一组断言,比如说( au~type),就是说( au)是一个类型。再比如(n~nat) 就是说(n)是一个自然数。从这里看其实就是一个断言。

    当我们有多个Judgement的时候,我们可以推导出其余的Judgement。比如说:(a=3)并且(b=5),那么在某些条件下面(就是多一些别的规则)我们可以推出来(a+b=8)。用正式的语言写出来就是

    [frac{a=3~~b=5}{a+b=8} ]

    在PL里面,可以用这种规则来定义一个类型的规则。比如

    [frac{a~mathtt{nat}~~b~mathtt{nat}}{a+b~mathtt{nat}} ]

    就是说,如果(a)是一个自然数,而且(b)也是一个自然数,那么(a+b)就是一个自然数。这个就是Inference Rule。
    我们如下定义所有的自然数

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

    这里我们首先有(0mathrel{ riangleq} z)。然后如果(n)是一个自然数,那么(succ(n))也是一个自然数。这样其实就是说(1mathrel{ riangleq} mathtt{succ}(0))(n+1mathrel{ riangleq} mathtt{succ}(n))
    书上的另外一个例子是定义一棵树

    [frac{}{mathtt{empty}~mathtt{tree}}~~frac{a_1~mathtt{tree}~~a_2~mathtt{tree}}{mathtt{node}(a_1,a_2)~mathtt{tree}} ]

    就是说,如果我们有两个树,那么着两个子树可以组成另一个树。

    其实这种定义的方法,在BNF里面也可以看到,比如
    Exp := num | Exp + Exp 就是说一个表达式可以是一个数字也可以是两个表达式的和。

    Rule Induction

    如果我们要证明某个类型有某种属性,那么我们该怎么证明呢?这里就是用归纳法。
    首先让我们会想下数学归纳法。数学归纳法是定义在自然数上的

    • 首先证明最简单的情况是对的
    • 然后假设当(n=i)的时候也是对的
    • 最后证明当(n=i+1)的时候也是对的

    通常(n=i+1)是定义在(n=i)上面的。
    不过如果说我们有(a_{i+1} = f(a_i , a_{i-1}))那么我们再第二步还需要假设(a_{i-1})也是对的。现在让我们假设(fmathrel{ riangleq} mathtt{node}),然后我们要证明类型(tree)满足某个属性(P),那么和数学归纳法类似,我们需要

    • 证明(P(empty)),即(P)在空树上成立(类似(n=0)时,成立)
    • 假设当(a_1~tree)(a_2~tree)时,(P(a_1))(P(a_2))
    • 证明(P(node(a_1, a_2)))

    这就是Rule Induction。其实感觉上就是数学归纳在树形结构上的推广。
    最后我们证明如下一个定理来加深一下理解下:
    如果(succ(s)~nat),那么(s~nat)

    这条定理叫做inversion lemma。乍一看显然,其实还是需要证明的:

    • (e=zero)时,因为(e)不能被写成(succ(s))的形式,所以定理成立。(初始情况)
    • 假设(s)满足这条定理,当(e=succ(s))时,我们需要证明,如果(e~nat)那么(s~nat)。因为(s)满足这条定理,并且(e=succ(s)~nat),那么我们有(s~nat)。那么(e)满足这条定理。

    证明完毕。

  • 相关阅读:
    SQL函数介绍,SDE函数
    [API]Google的语音识别API,支持各种语言
    (C#)Windows Shell 外壳编程系列8 同后缀名不同图标?
    (C#)Windows Shell 外壳编程系列8 同后缀名不同图标?
    获取某路径下,最后被修改的文件
    centos7下关闭防火墙
    linux下常用命令
    unittest断言
    **目录找出最后一次修改的文件(html结果),发送报告到指定qq邮箱
    unittest,requests,assertEqual实战演练
  • 原文地址:https://www.cnblogs.com/esing/p/5056650.html
Copyright © 2011-2022 走看看