之前讨论的都是狭义上的STLC,广义上往往还包括一些STLC的扩展类型和扩展语法。

0X00 let 绑定

这个在ML系的语言中非常的常见， Haskell中也有这个东西。简单的说就是给一些重复出现的东西取一个别称。在OCaml ，这里的操作语义一般是使用标准的"call-by-value".

语法：

  (* let *)
  | tlet : string -> tm -> tm -> tm
   (* i.e., let x = t1 in t2 *)

操作语义：

    (* let *)
    | ST_Let1 : ∀ x t1 t1' t2,
        t1 --> t1' ->
        (tlet x t1 t2) --> (tlet x t1' t2)
    |ST_LetValue : ∀ x v1 t2,
        value v1 ->
        (tlet x v1 t2) --> (subst x v1 t2)

我们这里和OCaml类似使用先对let中定义的绑定内容求值，再带入的做法（call by value）

替换规则

    (* let *)
    (* if x = y, nothing need to be changed in body*)
    | tlet y t1 t2 =>
      tlet y (subst x s t1) (if eqb_string x y then t2 else (subst x s t2))

类型关系

| T_Let : ∀ Gamma x t1 t2 T1 T2,
        Gamma ⊢ t1 ∈ T1 ->
        (x |-> T1; Gamma) ⊢ t2 ∈ T2 ->
        Gamma ⊢ (tlet x t1 t2) ∈ T2

参考Abs这个其实不是很难写，不过我第一次写的时候没有更新上下文，导致后面证明过程中卡了好久。。。。。还是理解不到位。

0X01 元组（对）

sf里面把这个称做Pair,有不少语言里也叫tuple一个意思.基本上就是lisp里面那个，表示一个值对，fst可以访问左侧的值，snd可以取出右侧的值。

Example

\x : Nat*Nat.
          let sum = x.fst + x.snd in
          let diff = x.fst - x.snd in
          (sum,diff)

语法

(* pairs *)
  | pair : tm -> tm -> tm
  | fst : tm -> tm
  | snd : tm -> tm

值关系

| v_pair : ∀ v1 v2,
        value v1 ->
        value v2 ->
        value (pair v1 v2).

操作语义

(* pairs *)
    | ST_Pair1 : ∀ t1 t2 t1',
        t1 --> t1' ->
        (pair t1 t2) --> (pair t1' t2)
    | ST_Pair2 : ∀ t1 t2 t2',
        t2 --> t2' ->
        (pair t1 t2) --> (pair t1 t2')
    | ST_Fst1 : ∀ t1 t1',
        t1 --> t1' ->
        (fst t1) --> (fst t1')
    | ST_FstPair : ∀ v1 v2,
        value v1 ->
        value v2 ->
        (fst (pair v1 v2)) --> v1
    | ST_Snd1 : ∀ t1 t1',
        t1 --> t1' ->
        (snd t1) --> (snd t1')
    | ST_SndPair : ∀ v1 v2,
        value v1 ->
        value v2 ->
        (snd (pair v1 v2)) --> v2

类型关系

    (* pairs *)
    | T_Pair : ∀ Gamma t1 t2 T1 T2,
        Gamma |- t1 ∈ T1 ->
        Gamma |- t2 ∈ T2 ->
        Gamma |- (pair t1 t2) ∈ (Prod T1 T2)
    | T_Fst : ∀ Gamma t T1 T2,
        Gamma |- t ∈ (Prod T1 T2) ->
        Gamma |- (fst t) ∈ T1
    | T_Snd : ∀ Gamma t T1 T2,
        Gamma |- t ∈ (Prod T1 T2) ->
        Gamma |- (snd t) ∈ T2

这中Pair的类型也被称为积类型(Product Type)，记作Nat * Nat，不难理解，相当于两个集合的卡式积。

替换规则

(* lists *)
    | tnil T =>
           tnil T
    | tcons t1 t2 =>
            tcons (subst x s t1) (subst x s t2)
    | tlcase t1 t2 y1 y2 t3 =>
             tlcase (subst x s t1) (subst x s t2) y1 y2
             (if eqb_string x y1 then
                t3
              else if eqb_string x y2 then t3
                   else (subst x s t3))

0X02 和类型

有的时候我们希望一个变量可以在不同的情况下拥有不同的类型， 比如c语言就提供了union,Java，Rust之类的语言可能会没有联合体，但是往往也会在标准库之类的东西里提供Either类之类的工具，这个在表示异常的时候会比较有效，go这种把err直接放到tuple里返回的，在我看来逻辑上就很怪异.....

STLC中我们定义inl为取左侧类型，inr取右侧类似， 使用case关键字可以对取不同类型时候的情况进行匹配。

Example

getNat ∈ Nat+Bool -> Nat
    getNat =
      \x:Nat+Bool.
        case x of
          inl n => n
        | inr b => test b then 1 else 0

值关系

(* A tagged value is a value:  *)
    | v_inl : forall v T,
        value v ->
        value (tinl T v)
    | v_inr : forall v T,
        value v ->
        value (tinr T v)

语法

(* sums *)
  | tinl : ty -> tm -> tm
  | tinr : ty -> tm -> tm
  | tcase : tm -> string -> tm -> string -> tm -> tm

操作语义

(* sums *)
    | ST_Inl : ∀ t1 t1' T,
        t1 --> t1' ->
        (tinl T t1) --> (tinl T t1')
    | ST_Inr : ∀ t1 t1' T,
        t1 --> t1' ->
        (tinr T t1) --> (tinr T t1')
    | ST_Case : ∀ t0 t0' x1 t1 x2 t2,
        t0 --> t0' ->
        (tcase t0 x1 t1 x2 t2) --> (tcase t0' x1 t1 x2 t2)
    | ST_CaseInl : ∀ v0 x1 t1 x2 t2 T,
        value v0 ->
        (tcase (tinl T v0) x1 t1 x2 t2) --> [x1:=v0]t1
    | ST_CaseInr : ∀ v0 x1 t1 x2 t2 T,
        value v0 ->
        (tcase (tinr T v0) x1 t1 x2 t2) --> [x2:=v0]t2

替换规则

(* sums *)
    | tinl T t1 =>
           tinl T (subst x s t1)
    | tinr T t1 =>
           tinr T (subst x s t1)
    | tcase t0 y1 t1 y2 t2 =>
            tcase (subst x s t0)
            y1 (if eqb_string x y1 then t1 else (subst x s t1))
            y2 (if eqb_string x y2 then t2 else (subst x s t2))

类型关系

(* sums *)
    | T_Inl : ∀ Gamma t1 T1 T2,
        Gamma |- t1 ∈ T1 ->
        Gamma |- (tinl T2 t1) ∈ (Sum T1 T2)
    | T_Inr : ∀ Gamma t2 T1 T2,
        Gamma |- t2 ∈ T2 ->
        Gamma |- (tinr T1 t2) ∈ (Sum T1 T2)
    | T_Case : ∀ Gamma t0 x1 T1 t1 x2 T2 t2 T,
        Gamma |- t0 ∈ (Sum T1 T2) ->
        (update Gamma x1 T1) |- t1 ∈ T ->
        (update Gamma x2 T2) |- t2 ∈ T ->
        Gamma |- (tcase t0 x1 t1 x2 t2) ∈ T

0X03 Unit

这个其实就相当于空指针的null类型，这是一个只有一个元素的类型。

操作语义
这个东西没法再步进了

值关系

| v_unit : value unit

类型关系

| T_Unit : forall Gamma,
        Gamma |- unit ∈ Unit

0X04 列表List

lisp like list没什么好多说的， nil表示空， cons表示后继； 和haskell,ml一样，这里支持对list进行模式匹配。不过话说这个东西其实可以用前面说的product type来模拟，毕竟pair只要一遍放值一边放后继其实也差不多，毕竟都是二元。

Example

\x:List Nat.
      lcase x of nil   => 0
               | a::x' => lcase x' of nil    => a
                                    | b::x'' => a+b

 (* lists *)
  | tnil : ty -> tm
  | tcons : tm -> tm -> tm
  | tlcase : tm -> tm -> string -> string -> tm -> tm

值关系

(* A list is a value iff its head and tail are values: *)
    | v_lnil : ∀ T, value (tnil T)
    | v_lcons : ∀ v1 vl,
        value v1 ->
        value vl ->
        value (tcons v1 vl)

操作语义

(* lists *)
    | ST_Cons1 : ∀ t1 t1' t2,
        t1 --> t1' ->
        (tcons t1 t2) --> (tcons t1' t2)
    | ST_Cons2 : ∀ v1 t2 t2',
        value v1 ->
        t2 --> t2' ->
        (tcons v1 t2) --> (tcons v1 t2')
    | ST_Lcase1 : ∀ t1 t1' t2 x1 x2 t3,
        t1 --> t1' ->
        (tlcase t1 t2 x1 x2 t3) --> (tlcase t1' t2 x1 x2 t3)
    | ST_LcaseNil : ∀ T t2 x1 x2 t3,
        (tlcase (tnil T) t2 x1 x2 t3) --> t2
    | ST_LcaseCons : ∀ v1 vl t2 x1 x2 t3,
        value v1 ->
        value vl ->
        (tlcase (tcons v1 vl) t2 x1 x2 t3)
          --> (subst x2 vl (subst x1 v1 t3))

替换规则

(* lists *)
    | tnil T =>
           tnil T
    | tcons t1 t2 =>
            tcons (subst x s t1) (subst x s t2)
    | tlcase t1 t2 y1 y2 t3 =>
             tlcase (subst x s t1) (subst x s t2) y1 y2
             (if eqb_string x y1 then
                t3
              else if eqb_string x y2 then t3
                   else (subst x s t3))

类型规则

 (* lists *)
    | T_Nil : ∀ Gamma T,
        Gamma |- (tnil T) ∈ (List T)
    | T_Cons : ∀ Gamma t1 t2 T1,
        Gamma |- t1 ∈ T1 ->
        Gamma |- t2 ∈ (List T1) ->
        Gamma |- (tcons t1 t2) ∈ (List T1)
    | T_Lcase : ∀ Gamma t1 T1 t2 x1 x2 t3 T2,
        Gamma |- t1 ∈ (List T1) ->
        Gamma |- t2 ∈ T2 ->
        (update (update Gamma x2 (List T1)) x1 T1) |- t3 ∈ T2 ->
        Gamma |- (tlcase t1 t2 x1 x2 t3) ∈ T2

0X05 递归

为了实现可以验证的递归操作，直接使用带递归的函数显然是不行的。这里使用类似Coq中Fixpoint的做法。
引入fix操作符， 不再把递归函数看成函数，其类型为fix。实现的要点在于为了能够在fix操作步进的过程中不断的进行打开，需要把fix 内做一个包裹的函数，其输入和输出类型变得一致，这样就能在验证过程中通过大量的unfold操作(不停的添加函数抽象，替换入函数体 )把递归函数展开成一个一层套一层的函数。

Example

fact =
          fix
            (\f:Nat->Nat.
               \x:Nat.
                  test x=0 then 1 else x * (f (pred x)))

操作语义

(* fix *)
    | ST_Fix1 : ∀ t1 t1',
        t1 --> t1' ->
        (tfix t1) --> (tfix t1')
    | ST_FixAbs : ∀ xf t2 T1,
        (tfix (abs xf T1 t2)) -->
        (subst xf (tfix (abs xf T1 t2)) t2)

替换规则

(* fix *)
    | tfix t1 =>
      tfix (subst x s t1)

类型关系

(* fix *)
    | T_Fix : ∀ Gamma t1 T1,
        Gamma |- t1 ∈ (Arrow T1 T1) ->
        Gamma |- (tfix t1) ∈ T1

0X06 Record类型

这个和haskell里的record差不多， 在c里的话就是结构体。使用 . 操作符可以把以一个record中某个Lable的值给取出来

Example

a:
{i1:T1, ..., in:Tn}       
                   
a . i1

这里可以把record 作为pair + list的语法糖来实现， 简单的说就是list里放一堆pair, fst是label, snd是值。

这一章节大部分的证明和定义我都写完了，完整的代码在这，证明性质的code 和过程比较长，但是和之前并没有本质区别：
https://github.com/StarGazerM/my-foolish-code/blob/master/plf/MoreStlc.v