对于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演算中的字母,代表一个匿名的函数， 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但是比如在全局作用域中，这个名字已经绑定过了。。。这时候就尴尬了，因为我们的变量名应该是不能影响语义的，局部全局重名很麻烦，需要额外规定，现在的语义没考虑这一点。在这里为了方便，暂时不处理。

归约

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

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

非形式化的可以写成（我抽空写成）

            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 t ∈ T

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

(X 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两次可以得到。