美文网首页
简单类型Lambda演算(1)

简单类型Lambda演算(1)

作者: 卷毛宿敌大小姐 | 来源:发表于2019-08-04 19:07 被阅读0次

    对于lambda演算相信只要学过离散数学的基本上都是都在课上学习过了,简单的说这是一种使用替换来描述的非常好用的形式系统。不敢说非常懂这个东西,但是直观上我觉得这个东西和谓词逻辑在很多地方很像。 在离散里学这个的时候,我们说的叫做无类型lambda演算,在foundation里,需要研究一下更加复杂的简单类型lambda演算(Simply typed lambda calculus)。为了方便通称STLC。
    类型系统的引入可以大大提高语义的准确性,而实际中的大多数以lambda演算为核心的编程语言中(函数式编程语言),也有很多是有类型的,比如Haskell。当然Haskell的类型系统远远不是"Simple"的。


    少女抄书中......


    0X00 语法

    接下来我们讨论这种简易的玩具语言中将使用以下语法:

    • 基础类型(base type): bool类型 (为了方便,只添加bool类型,实际上其他的数字等都是可以加入的。)
    • 常量: fls tru,真假两种布尔值
    • 条件语句:test t1 then t2 else t3
    • 变量
    • 函数抽象:\x:T1.t2 .其中\就是lambda演算中的字母\lambda,代表一个匿名的函数, x是函数的参数,: T1是参数x的类型标注,t2是函数体
    • 函数作用: t1 t2. 表示把t1 函数apply到t2上去
    • 箭头类型: * -> * 函数的类型,和大多是函数式语言一样

    Example

    \x: Bool. x                         一个输入x输出x的函数
    (\x:Bool. x) tru                    把上面定义的函数作用到参数true上
    \x:Bool. test x then fls else tru   一个取反的函数
    \f:Bool→Bool. f (f tru)             一个接受函数f作为参数的高阶函数
    

    形式化的有:

    Inductive ty : Type :=
      | Bool : ty
      | Arrow : ty → ty → ty.
    
    Inductive tm : Type :=
      | var : string → tm
      | app : tm → tm → tm
      | abs : string → ty → tm → tm
      | tru : tm
      | fls : tm
      | test : tm → tm → tm → tm.
    

    需要注意的是,在大多数主流语言中比如ML, Haskell中,存在类型推导,可以通过函数体去推测类型,但是为了方便讨论,我们定义的语言中参数的类型标注(type annotation)是不能省略的。

    0X01操作语义

    采用small-step操作语义

    值(value)

    • bool值tru, fls
    • 函数作用,比如f a这样的,如果f是纯函数,那么f a确定的时候,值就已经确定了,所以所有的函数作用当然可以看成值
    • 函数是值

    需要注意的是,在主流的编程语言中,不管是什么函数一般都被看作一个值,但是Coq中并不是,只有函数体是值那么整个函数才是值。我们这里为了验证方便采用前一种方式。

    完备(complete)

    一个不出现自由变量(free varible)的程序,被称为完备程序(complete program)。换句话说一个完整的程序是封闭的(closed)

    我们当前讨论的语言就是完备程序,这其实是为了避开对变量到底是不是值的讨论,因为都是封闭项,所以变量只会出现在我们归约的过程当中。

    替换(substitution)

    lambda calculus的核心思想就是替换,在这里我们当然也需要在操作语义中使用替换。

    来看一个简单的替换

    (\x: Bool. x) tru
    -----------------------
    tru
    

    这个应该不难理解,函数作用的过程本质就是把变量x替换为传给函数的参数。替换的过程可以用[x:=s]t表示,读作“把t中的x替换为s”
    其实这个东西和谓词逻辑中的替换是非常相似的,下面这个例子也会更好的说明这一点。

    [x:=tru] (\x:Bool. x)
    ------------------------
    (\x:Bool. x)
    

    是不是一下没有反应过来和第一个例子有什么不一样23333,第一个例子本质是[x:=tru]x.第二个例子中的x不是自由变量,他被lambda符号给capture了,或者说他是被绑定的(bound)!就好像在谓词逻辑中进行替换时候,被全称量词capture了,就不能被替换了,也是一个道理。替换只能针对自由变量。

    ok,接下来是完整的替换法则

           [x:=s]x               = s
           [x:=s]y               = y                     if x ≠ y
           [x:=s](\x:T11. t12)   = \x:T11. t12
           [x:=s](\y:T11. t12)   = \y:T11. [x:=s]t12     if x ≠ y
           [x:=s](t1 t2)         = ([x:=s]t1) ([x:=s]t2)
           [x:=s]tru             = tru
           [x:=s]fls             = fls
           [x:=s](test t1 then t2 else t3) =
                  test [x:=s]t1 then [x:=s]t2 else [x:=s]t3
    

    形式化的有

    Fixpoint subst (x : string) (s : tm) (t : tm) : tm :=
      match t with
      | var x' ⇒
          if eqb_string x x' then s else t
      | abs x' T t1 ⇒
          abs x' T (if eqb_string x x' then t1 else ([x:=s] t1))
      | app t1 t2 ⇒
          app ([x:=s] t1) ([x:=s] t2)
      | tru ⇒
          tru
      | fls ⇒
          fls
      | test t1 t2 t3 ⇒
          test ([x:=s] t1) ([x:=s] t2) ([x:=s] t3)
      end
    where "'[' x ':=' s ']' t" := (subst x s t).
    

    这里还是有一个问题,如果我们替换的名字虽然没有被当前的环境capture但是比如在全局作用域中,这个名字已经绑定过了。。。这时候就尴尬了,因为我们的变量名应该是不能影响语义的,局部全局重名很麻烦,需要额外规定,现在的语义没考虑这一点。在这里为了方便,暂时不处理。

    归约

    之前说了,有了替换,我们就可以对于函数作用进行归约了,也就是我们在\lambda演算中的\beta-归约(beta-reduction):

    (\x:T.t12) v2 --> [x:=v2]t12

    非形式化的可以写成(我抽空写成\LaTeX

                value v2    
    ------------------------------------
       (\x:T.t12) v2 --> [x:=v2]t12 
    
               t1 --> t1'   
    ------------------------------------
            t1 t2 --> t1' t2    
    
                value v1    
                t2 --> t2'  
    ------------------------------------
             v1 t2 --> v1 t2'   
    
    ------------------------------------
     (test tru then t1 else t2) --> t1
    
    ------------------------------------
     (test fls then t1 else t2) --> t2
    
                            t1 --> t1'  
    ----------------------------------------------------------
     (test t1 then t2 else t3) --> (test t1' then t2 else t3)   
    
    

    形式化的完整small step操作

    Inductive step : tm → tm → Prop :=
      | ST_AppAbs : ∀x T t12 v2,
             value v2 →
             (app (abs x T t12) v2) --> [x:=v2]t12
      | ST_App1 : ∀t1 t1' t2,
             t1 --> t1' →
             app t1 t2 --> app t1' t2
      | ST_App2 : ∀v1 t2 t2',
             value v1 →
             t2 --> t2' →
             app v1 t2 --> app v1 t2'
      | ST_TestTru : ∀t1 t2,
          (test tru t1 t2) --> t1
      | ST_TestFls : ∀t1 t2,
          (test fls t1 t2) --> t2
      | ST_Test : ∀t1 t1' t2 t3,
          t1 --> t1' →
          (test t1 t2 t3) --> (test t1' t2 t3)
    
    where "t1 '-->' t2" := (step t1 t2).
    Hint Constructors step.
    Notation multistep := (multi step).
    Notation "t1 '-->*' t2" := (multistep t1 t2) (at level 40).
    

    0X02 类型

    Q : x y的类型是什么?
    A: 这取决与x和y的类型是什么

    也就是说,在STLC中我们单看符号是看不出两个符号有什么类型的,只有放到一个上下文(contex)中,才能讨论类型,ok,扩充一下我们的类型断言,记作

    Gamma \vdash t ∈ T

    其中Gamma被称为类型上下文,读作“满足Gamma时,t 有类型 T”。
    一般的我们用一个偏射来表示表示上下文, 因此,更新上下文的过程可以记作

    (X \mapsto T1; Gamma)

    靠直觉,来写一下

    Reserved Notation "Gamma '⊢' t '∈' T" (at level 40).
    Inductive has_type : context → tm → ty → Prop :=
      | T_Var : ∀ Gamma x T,
          Gamma x = Some T →
          Gamma ⊢ var x ∈ T
      | T_Abs : ∀ Gamma x T11 T12 t12,
          (x ⊢> T11 ; Gamma) ⊢ t12 ∈ T12 →
          Gamma ⊢ abs x T11 t12 ∈ Arrow T11 T12
      | T_App : ∀ T11 T12 Gamma t1 t2,
          Gamma ⊢ t1 ∈ Arrow T11 T12 →
          Gamma ⊢ t2 ∈ T11 →
          Gamma ⊢ app t1 t2 ∈ T12
      | T_Tru : ∀ Gamma,
           Gamma ⊢ tru ∈ Bool
      | T_Fls : ∀ Gamma,
           Gamma ⊢ fls ∈ Bool
      | T_Test : ∀ t1 t2 t3 T Gamma,
           Gamma ⊢ t1 ∈ Bool →
           Gamma ⊢ t2 ∈ T →
           Gamma ⊢ t3 ∈ T →
           Gamma ⊢ test t1 t2 t3 ∈ T
    
    where "Gamma '⊢' t '∈' T" := (has_type Gamma t T).
    

    试试证明一个符合上面类型规则的东西吧~~
    Example:

    empty ⊢ (\x: Bool→Bool. (\y: Bool → Bool. (\z: Bool. y x z)))有类型
    形式化的有

    Example typing_example_3 :
      ∃ T,
        empty ⊢
          (abs x (Arrow Bool Bool)
             (abs y (Arrow Bool Bool)
                (abs z Bool
                   (app (var y) (app (var x) (var z)))))) ∈
          T.
    

    Proof:
    根据直觉可以猜测存在类型T为(Bool -> Bool) -> (Bool -> Bool) -> Bool -> Bool.
    形式化的有

    (Arrow (Arrow Bool Bool) (Arrow (Arrow Bool Bool) (Arrow Bool Bool)))
    

    根据T_Abs,如果要这个项目有类型,那么T11为(Bool->Bool),此时要有(x ⊢> (Bool -> Bool)) ⊢ t12 ∈ T12,此时再应用T_Abs,goal 变为(x ⊢> (Bool -> Bool); y ⊢> (Bool -> Bool)) ⊢ t12 ∈ T12.
    应用T_Abs,goal 变为(x ⊢> (Bool -> Bool); y ⊢> (Bool -> Bool); z ⊢> Bool ) ⊢ t12 ∈ T12,之后再T_App两次,T_Var两次可以得到。

    相关文章

      网友评论

          本文标题:简单类型Lambda演算(1)

          本文链接:https://www.haomeiwen.com/subject/mnrydctx.html