幸福迟了一夜才来。

类型系统是指一种根据所计算出值得种类对词语进行分类从而证明某程序行为不会发生的可行语法手段。

# 无类型系统

# 无类型算术表达式

# 语法

  • 项的集合是最小集合T\mathcal{T},满足:
    • {true,false,0}T\{true,false,0\}\subseteq \mathcal{T}
    • 如果t1Tt_1\in\mathcal{T},则{succ  t1,pred  t1  iszero  t1}T\{succ\;t_1,pred\;t_1\;iszero\;t_1\}\subseteq \mathcal{T}
    • 如果t1,t2,t3Tt_1,t_2,t_3\in\mathcal{T},则if  t1  then  t2  else  t3Tif\;t_1\;then\;t_2\;else\;t_3\in\mathcal{T}

# 对项的一些归纳定义

常量集合:

Consts(true)={true};Consts(false)={false};Consts(0)={0};Consts(succ  t1)=Consts(t1);Consts(pred  t1)=Consts(t1);Consts(iszero  t1)=Consts(t1);Consts(if  t1  then  t2  else  t3)=Consts(t1)Consts(t2)Consts(t3)Consts(true)=\{true\};Consts(false)=\{false\};Consts(0)=\{0\};\\ Consts(succ\;t_1)=Consts(t_1);Consts(pred\;t_1)=Consts(t_1);Consts(iszero\;t_1)=Consts(t_1);\\ Consts(if\;t_1\;then\;t_2\;else\;t_3)=Consts(t_1)\cup Consts(t_2)\cup Consts(t_3)

项的长度:

size(true)=size(false)=size(0)=1;size(succ  t1)=size(pred  t1)=size(iszero  t1)=size(t1)+1;size(if  t1  then  t2  else  t3)=size(t1)+size(t2)+size(t3)+1;size(true)=size(false)=size(0)=1;\\ size(succ\;t_1)=size(pred\;t_1)=size(iszero\;t_1)=size(t_1)+1;\\ size(if\;t_1\;then\;t_2\;else\;t_3)=size(t_1)+size(t_2)+size(t_3)+1;

项的深度:

depth(true)=depth(false)=depth(0)=1;depth(succ  t1)=depth(pred  t1)=depth(iszero  t1)=depth(t1)+1;depth(if  t1  then  t2  else  t3)=max(depth(t1),depth(t2),depth(t3))+1;depth(true)=depth(false)=depth(0)=1;\\ depth(succ\;t_1)=depth(pred\;t_1)=depth(iszero\;t_1)=depth(t_1)+1;\\ depth(if\;t_1\;then\;t_2\;else\;t_3)=max(depth(t_1),depth(t_2),depth(t_3))+1;

Consts(t)size(t)|Consts(t)|\leq size(t)

同理,对项上的一个谓词,我们可以对长度或对深度归纳,或结构归纳。

# 求值

  • 语法:

    t::=truefalseif  t  then  t  else  tv::=truefalset::=true|false|if\;t\;then\;t\;else\;t\\ v::=true|false

  • 求值:

    if  true  then  t2  else  t3t2(EIFTRUE)if  false  then  t2  else  t3t3(EIFFALSE)t1t1if  t1  then  t2  else  t3if  t1  then  t2  else  t3(EIF)if\;true\;then\;t_2\;else\;t_3\rightarrow t_2(E-IFTRUE)\\ if\;false\;then\;t_2\;else\;t_3\rightarrow t_3(E-IFFALSE)\\ \frac{t_1\rightarrow t_1'}{if\;t_1\;then\;t_2\;else\;t_3\rightarrow if\;t_1'\;then\;t_2\;else\;t_3}(E-IF)

    ttt\rightarrow t' 表示 “t 一步求值为 t’”,意思是如果 t 是抽象机器在某瞬间的状态,则机器可以做一步计算,并将状态转换为 t’ .

# 无类型算术表达式

  • 语法形式:

    t::=0succ  tpred  tiszero  ttruefalseif  t  then  t  else  tv::=nvtruefalsenv::=0succ  nvt::=0|succ\;t|pred\;t|iszero\;t|true|false|if\;t\;then\;t\;else\;t\\ v::=nv|true|false\\ nv::=0|succ\;nv

    我们常用阿拉伯数字来记succ  0=1,succ  succ  0=2,...succ\;0=1,succ\;succ\;0=2,...

  • 求值规则:

    if  true  then  t2  else  t3t2(EIFTRUE)if  false  then  t2  else  t3t3(EIFFALSE)t1t1if  t1  then  t2  else  t3if  t1  then  t2  else  t3(EIF)t1t1succ  t1succt1(ESUCC)pred  00(EPREDZERO)pred(succ  nv1)nv1(EPREDSUCC)t1t1pred  t1pred  t1(EPRED)iszero  0true(EISZEROZERO)iszero(succ  nv1)false(EISZEROSUCC)t1t1iszero  t1iszero  t2(EISZERO)if\;true\;then\;t_2\;else\;t_3\rightarrow t_2\quad(E-IFTRUE)\\ if\;false\;then\;t_2\;else\;t_3\rightarrow t_3\quad(E-IFFALSE)\\ \frac{t_1\rightarrow t_1'}{if\;t_1\;then\;t_2\;else\;t_3\rightarrow if\;t_1'\;then\;t_2\;else\;t_3}\quad(E-IF)\\ \frac{t_1\rightarrow t_1'}{succ\;t_1\rightarrow succ t_1'}\quad(E-SUCC)\\ pred\;0\rightarrow 0\quad(E-PREDZERO)\\ pred(succ\;nv_1)\rightarrow nv_1\quad(E-PREDSUCC)\\ \frac{t_1\rightarrow t_1'}{pred\;t_1\rightarrow pred\;t_1'}\quad(E-PRED)\\ iszero\;0\rightarrow true\quad(E-ISZEROZERO)\\ iszero(succ\;nv_1)\rightarrow false\quad(E-ISZEROSUCC)\\ \frac{t_1\rightarrow t_1'}{iszero\;t_1\rightarrow iszero\;t_2}\quad(E-ISZERO)

    项 t 被称为范式当且仅当不存在tt' 使得ttt\rightarrow t'.

    显然,范式就是那些true,false,0,succ(0),succ(succ(0)),...true,false,0,succ(0),succ(succ(0)),.... 注意,若出现了 pred 一定不是范式,因为总可以用 E-PREDZERO 或 E-PREDSUCC 把它消掉.

    我们认为succ  truesucc\;true 是一个错误而不是一个值.

  • 定义,如果一个封闭项是一个范式但不是一个值,则称该项受阻

# 无类型的 lambda 演算

# 基础

  • lambda 演算用最可能纯的形式表示函数的定义和应用。在 lambda 演算中,每个事物均是一个函数:函数接受的参数是函数,一个函数的结果是另一个函数。

  • lambda 演算的语法由 3 种项组成。一个变量 x 本身是一个项;一个变量 x 在项t1t_1 中的抽象,记为λx.t1\lambda x.t_1,是一个项;并且一个项应用到另一个项t1  t2t_1\;t_2 也是一个项。用语法描述,项为:

    t::=xλx.tt  tt::=x|\lambda x.t|t\;t

    我们规定,分析 lambda 演算式子时,从左到右分析,而抽象的顺序是从右到左。即:

    t1  t2  t3=(t1  t2)  t3λx.λy.t=λx.(λy.t)t_1\;t_2\;t_3=(t_1\;t_2)\;t_3\\ \lambda x.\lambda y.t=\lambda x.(\lambda y.t)

# 抽象语法和具体语法

# 辖域

  • 对变量 x,当它出现在抽象λx.t\lambda x.t 的 t 中时,则认为 x 的出现是囿界(或称被界定)的。等价地,也可以说λx\lambda x 是一个绑定器,它的辖域是 t。x 是自由的如果它出现的位置不被任何对 x 的抽象所界定。比如 x 在xyxyλy.xy\lambda y.xy 中式自由的,而在(λx.x)x(\lambda x.x)x 中的第一个出现是囿界的,而第二个是自由的。

  • 一个不含自由变量的项称为封闭项(或称为组合子)。最简单的组合子就是恒等函数:

    id=λx.xid=\lambda x.x

  • 规定,抽象总是尽量向右延展的,而应用是从左到右的。譬如:

    λx.x  y=λx.(x  y)(λx.x)y(λx.x  y)aa  y(λx.x)y  ay  aidx  y=(idx)  y\lambda x.x\;y=\lambda x.(x\;y)\neq(\lambda x.x)y\\ (\lambda x.x\;y)a\rightarrow a\;y\\ (\lambda x.x)y\;a\rightarrow y\;a\\ idx\;y=(idx)\;y

# 操作语义

  • 纯形式的 lambda 演算没有内置的常量或原语算子 —— 没有数、算术运算、条件子、记录、循环、序列、I/O 等到。项计算的唯一含义是将函数应用到参数(而参数本身也是函数)。

    计算的每一步是重写一个左端部分为抽象的应用,用右端部分代换抽象体中的囿变量。

    (λx.t12)t2[xt2]t12(\lambda x.t_{12})t_2\rightarrow [x\mapsto t_2]t_{12}

    其中[xt2]t12[x\mapsto t_2]t_{12} 表示由t2t_2 代换在t12t_{12} 中所有出现的 x 得到的项。例如:

    (λx.x)yy(λx.x(λx.x))(u  r)(u  r)(λx.x)(\lambda x.x)y\rightarrow y\\ (\lambda x.x(\lambda x.x))(u\;r)\rightarrow(u\;r)(\lambda x.x)

    (其中第二个式子实际上是用(u  r)(u\;r) 去代换x(λx.x)x(\lambda x.x) 中所有自由的 x,即为(u  r)(λx.x)(u\;r)(\lambda x.x)。)

  • 考虑项:

    (λx.x)((λx.x)(λz.(λx.x)z))(\lambda x.x)((\lambda x.x)(\lambda z.(\lambda x.x)z))

    λx.x=id\lambda x.x=id,即t,(λx.x)t=idtt\forall t,(\lambda x.x)t=idt\rightarrow t。即为:

    id(id(λz.idz))id(id(\lambda z.idz))

    在全 beta 归约下,任何时刻可以归约任何一个约式。可以选择:

    • 从内到外归约:

      id(id(λz.idz))id(id(λz.z))id(λz.z)λz.zid(id(\lambda z.idz))\\ \rightarrow id(id(\lambda z.z))\\ \rightarrow id(\lambda z.z)\\ \rightarrow \lambda z.z

    • 从外到内归约:

      id(id(λz.idz))id(λz.idz)λz.idzλz.zid(id(\lambda z.idz))\\ \rightarrow id(\lambda z.idz)\\ \rightarrow \lambda z.idz\\ \rightarrow \lambda z.z

    • 我们也可以不允许抽象内部的归约。即λz.idz\lambda z.idz 已经作为一个范式,而不对λz.\lambda z. 抽象内部进行归约。当然应该从外到内归约:

      id(id(λz.idz))id(λz.idz)λz.idzid(id(\lambda z.idz))\\ \rightarrow id(\lambda z.idz)\\ \rightarrow \lambda z.idz

# lambda 演算中的程序设计

我理解的 lambda 演算实际上还是在描述函数。譬如λx.x+1\lambda x.x+1,其中 λ 跟着的是函数参数,“.” 后面跟着函数的内容。然后如果传入一个参数,即作用于 a 时,就会求值得到用 a 去替换函数内容中的自变量 x。

  • 如果想描述的函数有多自变量怎么办?λ(x,y).s\lambda(x,y).s。实际上,我们可以写为λx.λy.s\lambda x.\lambda y.s,这样先传入 y 的值,然后会继续得到一个 lambda 抽象(函数),再求值。譬如:

    λ(x,y).x+y(λx.λy.x+y)3  4(λx.x+3)  44+3\lambda(x,y).x+y\\ (\lambda x.\lambda y.x+y)3\;4\\ \rightarrow(\lambda x.x+3)\;4\\ \rightarrow 4+3

# Church 布尔式

  • 定义:

    tru=λt.λf.tfls=λt.λf.ftest=λl.λm.λn.l  m  ntru=\lambda t.\lambda f.t\\ fls=\lambda t.\lambda f.f\\ test=\lambda l.\lambda m.\lambda n.l\;m\;n

    为什么要定义这些东西?实际上,它用函数来描述了 if 语句:

    test  tru  v  w=(λl.λm.λn.l  m  n)tru  v  w(λm.λn.tru  m  n)v  w(λn.tru  v  n)wtru  v  w=(λt.λf.t)v  w(λf.v)wvtest\;tru\;v\;w\\ =(\lambda l.\lambda m.\lambda n.l\;m\;n)tru\;v\;w\\ \rightarrow(\lambda m.\lambda n.tru\;m\;n)v\;w\\ \rightarrow(\lambda n.tru\;v\;n)w\\ \rightarrow tru\;v\;w\\ =(\lambda t.\lambda f.t)v\;w\\ \rightarrow(\lambda f.v)w\\ \rightarrow v

    test  fls  v  w=(λl.λm.λn.l  m  n)fls  v  w(λm.λn.fls  m  n)v  w(λn.fls  v  n)w  fls  v  w=(λt.λf.f)v  w(λf.f)wwtest\;fls\;v\;w\\ =(\lambda l.\lambda m.\lambda n.l\;m\;n)fls\;v\;w\\ \rightarrow(\lambda m.\lambda n.fls\;m\;n)v\;w\\ \rightarrow(\lambda n.fls\;v\;n)w\;\\ \rightarrow fls\;v\;w\\ =(\lambda t.\lambda f.f)v\;w\\ \rightarrow(\lambda f.f)w\\ \rightarrow w

    实际上,tru  v  wtru\;v\;w 可以归约到wwfls  v  wfls\;v\;w 可以归约到ww。我们用 test 可以判断布尔的真假。即

    test  b  v  wtest\;b\;v\;w 如果归约到 v 了 b 就为真,否则为假。

  • 我们可以定义逻辑联结词:

    and=λb.λc.b  c  flsand=\lambda b.\lambda c.b\;c\;fls

    它的作用是:

    and  tru  tru=(λb.λc.b  c  fls)tru  tru(λc.tru  c  fls)trutru  tru  flstruand  fls  truflsand\;tru\;tru\\ =(\lambda b.\lambda c.b\;c\;fls)tru\;tru\\ \rightarrow (\lambda c.tru\;c\;fls)tru\\ \rightarrow tru\;tru\;fls\\ \rightarrow tru\\ and\;fls\;tru\rightarrow fls

    同理:

    or=λb.λc.b  tru  cnot=λb.b  fls  truor=\lambda b.\lambda c.b\;tru\;c\\ not=\lambda b.b\;fls\;tru

  • 我们能定义值得序对为项:

    pair=λf.λs.λb.b  f  sfst=λp.p  trusnd=λp.p  flspair=\lambda f.\lambda s.\lambda b.b\;f\;s\\ fst=\lambda p.p\;tru\\ snd=\lambda p.p\;fls

    有:

    fst(pair  v  w)=fst((λf.λs.λb.b  f  s)v  w)fst(λb.b  v  w)=(λp.p  tru)  (λb.b  v  w)(λb.b  v  w)  trutru  v  wvfst(pair\;v\;w)\\ =fst((\lambda f.\lambda s.\lambda b.b\;f\;s)v\;w)\\ \rightarrow fst(\lambda b.b\;v\;w)\\ =(\lambda p.p\;tru)\;(\lambda b.b\;v\;w)\\ \rightarrow (\lambda b.b\;v\;w)\;tru\\ \rightarrow tru\;v\;w\\ \rightarrow v

# Church 数值

  • 定义 Church 数值:

    c0=λs.λz.zc1=λs.λz.s  zc2=λs.λz.s  (s  z)c3=λs.λz.s  (s  (s  z)).......c_0=\lambda s.\lambda z.z\\ c_1=\lambda s.\lambda z.s\;z\\ c_2=\lambda s.\lambda z.s\;(s\;z)\\ c_3=\lambda s.\lambda z.s\;(s\;(s\;z))\\ .......

    succ=λn.λs.λz.s  (n  s  z)succ  c3=(λn.λs.λz.s  (n  s  z))c3λs.λz.s  (c3  s  z)=λs.λz.s  ([λs.λz.s(s(s  z))]s  z)λs.λz.s([λz.s(s(s  z))]z)λs.λz.s(s(s(s  z)))=c4succ=\lambda n.\lambda s.\lambda z.s\;(n\;s\;z)\\ succ\;c_3=(\lambda n.\lambda s.\lambda z.s\;(n\;s\;z))c_3\\ \rightarrow\lambda s.\lambda z.s\;(c_3\;s\;z)\\ =\lambda s.\lambda z.s\;([\lambda s.\lambda z.s(s(s\;z))]s\;z)\\ \rightarrow\lambda s.\lambda z.s([\lambda z.s(s(s\;z))]z)\\ \rightarrow\lambda s.\lambda z.s(s(s(s\;z)))=c_4

    这里解释下。还记得抽象式中,λs.λz.s  z\lambda s.\lambda z.s\;z 中 s 和 z 都表示了函数的内容。我们可以理解 s 为一个 “后继函数”。可以记cn=λs.λz.sn  zc_n=\lambda s.\lambda z.s^n\;z。求值为cn  a  ban  bc_n\;a\;b\rightarrow a^n\;b

    那么后继函数实际上就是用了这个求值,使得s  (cn  s  z)s  (sn  z)=sn+1  zs\;(c_n\;s\;z)\rightarrow s\;(s^n\;z)=s^{n+1}\;z

  • 定义加法:

    plus=λm.λn.λs.λz.m  s  (n  s  z)plus=\lambda m.\lambda n.\lambda s.\lambda z.m\;s\;(n\;s\;z)\\

    只看函数内容m  s  (n  s  z)m\;s\;(n\;s\;z),因为求值有:

    ca  s  (cb  s  z)sa  (cb  s  z)sa  (sb  z)=sa+b  zc_a\;s\;(c_b\;s\;z)\rightarrow s^a\;(c_b\;s\;z)\rightarrow s^a\;(s^b\;z)=s^{a+b}\;z

    所以有plus  cn  cmcn+mplus\;c_n\;c_m\rightarrow c_{n+m}

    定义乘法:

    times=λm.λn.m  (plus  n)  c0times=\lambda m.\lambda n.m\;(plus\;n)\;c_0

    只看函数内容m  (plus  n)  c0m\;(plus\;n)\;c_0,因为有:

    ca  (plus  cb)  c0(plus  cb)a  c0=plus  cb  (plus  cb  (...  plus  cb  c0))))ca×bc_a\;(plus\;c_b)\;c_0\rightarrow (plus\;c_b)^a\;c_0=plus\;c_b\;(plus\;c_b\;(...\;plus\;c_b\;c_0))))\\ \rightarrow c_{a\times b}

    因为实际上就是把cbc_bc0c_0 上加了 a 次。

  • 定义判零:

    iszro=λm.m  (λx.fls)  truiszro  c0c0  (λx.fls)  truiszro=\lambda m.m\;(\lambda x.fls)\;tru\\ iszro\;c_0\rightarrow c_0\;(\lambda x.fls)\;tru\\

    \rightarrow(\lambda z.z);tru\
    \rightarrow tru\
    iszro;c_n\rightarrow c_n;(\lambda x.fls);tru\
    =(\lambda s.\lambda z.s^n;z)(\lambda x.fls);tru\
    \rightarrow (\lambda z.(\lambda x.fls)^n;z);tru\
    \rightarrow (\lambda x.fls)^n tru\
    \rightarrow fls\

    返回值也是个Church布尔值。返回值也是个Church布尔值。

    zz=pair  c0  c0ss=λp.pair  (snd  p)  (plus  c1  (snd  p))prd=λm.fst  (m  ss  zz)zz=pair\;c_0\;c_0\\ ss=\lambda p.pair\;(snd\;p)\;(plus\;c_1\;(snd\;p))\\ prd=\lambda m.fst\;(m\;ss\;zz)

    为什么它可以实现前趋呢?不难发现,prd  cnfst  (ssn  zz)prd\;c_n\rightarrow fst\;(ss^n\;zz)

    ss  zzss\;zz 求值其实等于pair  c0  c1pair\;c_0\;c_1。然后ss2  zz=pair  c1  c2ss^2\;zz=pair\;c_1\;c_2。因此ssn  zz=pair  cn1  cnss^n\;zz=pair\;c_{n-1}\;c_n

    所以prd  cnfst  (pair  cn1  cn)cn1prd\;c_n\rightarrow fst\;(pair\;c_{n-1}\;c_n)\rightarrow c_{n-1}

  • 定义减法:

    minus=λm.λn.n  prd  mminus  ca  cbcb  prd  caprdb  cacabminus=\lambda m.\lambda n.n\;prd\;m\\ minus\;c_a\;c_b\rightarrow c_b\;prd\;c_a\rightarrow prd^b\;c_a\rightarrow c_{a-b}

  • 定义判等:

    equal=λm.λn.iszro(minus  m  n)equal=\lambda m.\lambda n.iszro(minus\;m\;n)

# 丰富演算 ——Church 编码和真实值的转换

  • 可以定义抽象,使其可以将 Church 布尔式转化为之前无类型算术表达式中真正的布尔式:

    realbool=λb.b  true  falserealbool  trutrue;realboolflsfalse;realbool=\lambda b.b\;true\;false\\ realbool\;tru\rightarrow true;\\ realbool fls\rightarrow false;

    同理可以反过来转换:

    churchbool=λb.if  b  then  tru  else  flschurchbool  trueif  true  then  tru  else  flstruchurchboolfalseflschurchbool=\lambda b.if\;b\;then\;tru\;else\;fls\\ churchbool\;true\rightarrow if\;true\;then\;tru\;else\;fls\rightarrow tru\\ churchbool false\rightarrow fls

    这里的推导,既可以根据 λ 演算的规则,也可以根据无类型算术表达式的推导规则。

    同样也可以定义,真正判等:(我们如果带了个真正,就表示求值是个 true 或 false,而不是 Church 编码的布尔式)

    realeq=λm.λn.realbool(equal  m  n)realeq=\lambda m.\lambda n.realbool(equal\;m\;n)

    Church 数值转真正数值:

    realnat=λm.m  (λx.succ  x)  0realnat  c3succ  succ  succ  0=3realnat=\lambda m.m\;(\lambda x.succ\;x)\;0\\ realnat\;c_3\rightarrow succ\;succ\;succ\;0=3

    我们不能直接定义realnat=λm.m  succ  0realnat=\lambda m.m\;succ\;0,因为succsucc 只是一个标识而本身没有语法意义。因此我们需要把它包装在一个小函数中,而不能直接当作一个函数来用。

# 递归

  • 有些抽象在归约时,仍是他自己。譬如:

    omega=(λx.x  x)(λx.x  x)omega=(\lambda x.x\;x)(\lambda x.x\;x)

  • 不动点组合式

    fix=λf.(λx.f  (λy.x  x  y))(λx.f  (λy.x  x  y))fix=\lambda f.(\lambda x.f\;(\lambda y.x\;x\;y))(\lambda x.f\;(\lambda y.x\;x\;y))

    这有啥用呢?实际上,它可以解决递归问题。用最简单的阶乘函数来考虑下:

    g=λfct.λn.if  realeq  n  c0  then  c1  else  (times  n  (fct  (prd  n)))factorial=fix  gg=\lambda fct.\lambda n.if\;realeq\;n\;c_0\;then\;c_1\;else\;(times\;n\;(fct\;(prd\;n)))\\ factorial=fix\;g

    先定义g=λf.<...>g=\lambda f.<...><...><...> 内为函数内容。然后再定义F=fix  gF=fix\;g

    以一个例子,考虑下factorial  c3factorial\;c_3

    factorial  c3=fix  g  c3h  h  c3(h:=λx.g  (λy.x  x  y))g  fct  c3(fct:=λy.h  h  y)λn.if  realeq  n  c0  then  c1  else  (times  n  (fct  (prd  n)))  c3if  realeq  c3  c0  then  c1  else  (times  c3  (fct  (prd  c3)))times  c3  (fct  (prd  c3))times  c3  fct  c2times  c3  (g  fct  c2)times  c3  (if  realeq  c2  c0  then  c1  else  times  c2  (fct(prd  c2)))times  c3  (times  c2  c1)c6factorial\;c_3=fix\;g\;c_3\\ \rightarrow h\;h\;c_3\quad (h:=\lambda x.g\;(\lambda y.x\;x\;y))\\ \rightarrow g\;fct\;c_3\quad(fct:=\lambda y.h\;h\;y)\\ \rightarrow \lambda n.if\;realeq\;n\;c_0\;then\;c_1\;else\;(times\;n\;(fct\;(prd\;n)))\;c_3\\ \rightarrow if\;realeq\;c_3\;c_0\;then\;c_1\;else\;(times\;c_3\;(fct\;(prd\;c_3)))\\ \rightarrow^*times\;c_3\;(fct\;(prd\;c_3))\\ \rightarrow^* times\;c_3\;fct\;c_2\\ \rightarrow^* times\;c_3\;(g\;fct\;c_2)\\ \rightarrow^* times\;c_3\;(if\;realeq\;c_2\;c_0\;then\;c_1\;else\;times\;c_2\;(fct(prd\;c_2)))\\ \rightarrow^* times\;c_3\;(times\;c_2\;c_1)\\ \rightarrow^* c_6

    其中关键在于:

    fct  c2h  h  c2g  (λy.h  h  y)  c2g  fct  c2fct\;c_2\rightarrow h\;h\;c_2\rightarrow g\;(\lambda y.h\;h\;y)\;c_2\rightarrow g\;fct\;c_2

    fctfct 是自重复的。

# 形式化定义

其实前面已经用半天了,又回来形式化定义下。

  • 定义项的自由变量,记为FV(t)FV(t),定义如下:

    FV(x)={x}FV(λx.t1)=FV(t1){x}FV(t1  t2)=FV(t1)FV(t2)FV(x)=\{x\}\\ FV(\lambda x.t_1)=FV(t_1)-\{x\}\\ FV(t_1\;t_2)=FV(t_1)\cup FV(t_2)

  • 关于代入,首先,我们约定只是囿变量名称不同的项在所有上下文中可交替使用。即可以 “换名”:

    λx.x+y=λw.w+y\lambda x.x+y=\lambda w.w+y

    对代换的定义为:

    [xs]x=s[xs]y=yif  yx[xs](λy.t1)=λy.[xs]t1if  yx  and  yFV(s)[xs](t1  t2)=([xs]t1)([xs]t2)[x\mapsto s]x=s\\ [x\mapsto s]y=y\quad if\;y\neq x\\ [x\mapsto s](\lambda y.t_1)=\lambda y.[x\mapsto s]t_1\quad if\;y\neq x\;and\;y\notin FV(s)\\ [x\mapsto s](t_1\;t_2)=([x\mapsto s]t_1)([x\mapsto s]t_2)

    其中,第三行可以先把 y 换名换成满足条件的。

  • lambda 演算语义的定义:

    t1t1t1  t2t1  t2t2t2v1  t2v1  t2(λx.t12)  v2[xv2]t12\frac{t_1\rightarrow t_1'}{t_1\;t_2\rightarrow t_1'\;t_2}\\ \frac{t_2\rightarrow t_2'}{v_1\;t_2\rightarrow v_1\;t_2'}\\ (\lambda x.t_{12})\;v_2\rightarrow [x\mapsto v_2]t_{12}

# 项的无名称表示

# 项和上下文

  • 对每个 λ 抽象,我们可以找到对应的 de Bruijn 项,即去掉囿变量,用数字替换:

    λz.(λy.y  (λx.x))  (λx.z  x)=λ.(λ.1  (λ.1))(λ.2  1)\lambda z.(\lambda y.y\;(\lambda x.x))\;(\lambda x.z\;x)=\lambda.(\lambda.1\;(\lambda.1))(\lambda.2\;1)

    1

    而书上是从 0 开始标号的。

    然后自由变量的话,可以用大于囿变量个数的自然数代换它。

  • 形式化的,定义无名项:

    T\mathcal{T} 是最小的集簇{T0,T1,...}\{\mathcal{T_0},\mathcal{T_1},...\},使得:

    • 0k<n,kTn\forall 0\leq k< n,k\in\mathcal{T}_n
    • 如果t1Tn,λ.t1Tn1t_1\in\mathcal{T}_n,\lambda.t_1\in\mathcal{T}_{n-1}
    • 如果t1,t2Tnt_1,t_2\in\mathcal{T}_n,那么t1  t2Tnt_1\;t_2\in\mathcal{T}_n

    仔细想一想,可以发现Tn\mathcal{T}_n 为至多含有 n 个自由变量的项。例如λ.5  0T6\lambda .5\;0\in\mathcal{T}_{6},5 为自由变量。

  • 我们可以对所有的 de Bruijn 变量指派一个 de Bruijn 索引(称为一个命名的上下文),例如:

    Γ=x4y3z2a1b0\Gamma=x\mapsto 4\\y\mapsto 3\\z\mapsto 2\\ a\mapsto 1\\b\mapsto 0

    那么a  λx.a=1  λ.2a\;\lambda x.a=1\;\lambda.2。注意自由变量的索引需要加上非自由变量的个数。

    上面那个指派也可以简写为Γ=x,y,z,a,b\Gamma=x,y,z,a,b

# 移位和代换

  • 定义移位:

    cd(k)={kif  k<ck+dif  kccd(λ.t1)=λ.c+1d(t1)cd(t1  t2)=cd(t1)  cd(t2)\uparrow^d_c(k)=\begin{cases}k&if\;k<c\\k+d&if\;k\geq c\end{cases}\\ \uparrow^d_c(\lambda.t_1)=\lambda.\uparrow^d_{c+1}(t_1)\\ \uparrow^d_c(t_1\;t_2)=\uparrow^d_c(t_1)\;\uparrow^d_c(t_2)

    默认从 0 开始移位,例:

    2(λ.0  1  (λ.0  1  2))=λ.120  1  (λ.0  1  2)=λ.0  121  (λ.0  1  2)=λ.0  3  (λ.220  1  2)=λ.0  3  (λ.0  1  4)\uparrow^2(\lambda.0\;1\;(\lambda.0\;1\;2))=\lambda.\uparrow^2_10\;1\;(\lambda.0\;1\;2)\\ =\lambda.0\;\uparrow^2_11\;(\lambda.0\;1\;2)\\ =\lambda.0\;3\;(\lambda.\uparrow^2_2 0\;1\;2)\\ =\lambda.0\;3\;(\lambda.0\;1\;4)

  • 定义代换:

    [js]k={sif  k=jkelse[js](λ.t1)=λ.[j+11s]t1[js](t1  t2)=[js]t1  [js]t2[j\mapsto s]k=\begin{cases}s&if\;k=j\\k&else\end{cases}\\ [j\mapsto s](\lambda.t_1)=\lambda.[j+1\mapsto \uparrow^1 s]t_1\\ [j\mapsto s](t_1\;t_2)=[j\mapsto s]t_1\;[j\mapsto s]t_2

    譬如对全局上下文Γ=a,b\Gamma=a,b,有

    [ba  (λz.a)](b  (λx.b))=[01  (λ.2)](0  (λ.1))=(1  λ.2)  [01  (λ.2)](λ.1)=(1  λ.2)  λ.[0+101(1  λ.2)]1=(1  λ.2)  λ.[1(2  λ.3)]1=(1  λ.2)  λ.(2  λ.3)=(a  λz1.a)  (λz2.a  λz3.a)[b\mapsto a\;(\lambda z.a)](b\;(\lambda x.b))=[0\mapsto 1\;(\lambda.2)](0\;(\lambda.1))\\ =(1\;\lambda.2)\;[0\mapsto 1\;(\lambda.2)](\lambda.1)\\ =(1\;\lambda.2)\;\lambda.[0+1\mapsto\uparrow^1_0(1\;\lambda.2)]1\\ =(1\;\lambda.2)\;\lambda.[1\mapsto(2\;\lambda.3)]1\\ =(1\;\lambda.2)\;\lambda.(2\;\lambda.3)\\ =(a\;\lambda z_1.a)\;(\lambda z_2.a\;\lambda z_3.a)

# 求值

t1t1t1  t2t1  t2t2t2v1  t2v1  t2(λ.t12)  v201([001v2]t12)\frac{t_1\rightarrow t_1'}{t_1\;t_2\rightarrow t_1'\;t_2}\\ \frac{t_2\rightarrow t_2'}{v_1\;t_2\rightarrow v_1\;t_2'}\\ (\lambda.t_{12})\;v_2\rightarrow \uparrow^{-1}_0([0\mapsto\uparrow^1_0 v_2]t_{12})

例如

(λ.1  0  2)(λ.0)0  (λ.0)  1(\lambda.1\;0\;2)(\lambda.0)\rightarrow 0\;(\lambda.0)\;1

而不是1  (λ.0)  21\;(\lambda.0)\;2,因为需要对自由变量重新编排。

# 简单类型

# 类型算术表达式

# 类型关系

  • 语法定义:

    T::=Booltrue:Boolfalse:Boolt1:Boolt2:Tt3:Tif  t1  then  t2  else  t3:TT::=Nat0:Natt1:Natsucc  t1:Natt1:Natpred  t1:Natt1:Natiszro  t1:BoolT::=Bool\\ --------------\\ true:Bool\\ false:Bool\\ \frac{t_1:Bool\quad t_2:T\quad t_3:T}{if\;t_1\;then\;t_2\;else\;t_3:T}\\ --------------\\ T::=Nat\\ --------------\\ 0:Nat\\ --------------\\ \frac{t_1:Nat}{succ\;t_1:Nat}\\ \frac{t_1:Nat}{pred\;t_1:Nat}\\ \frac{t_1:Nat}{iszro\;t_1:Bool}\\

    注,T 表示类型。而 if 语句里表示t2,t3t_2,t_3 和 if 语句最后都是同一类型。(而非必须是 Bool,只是目前我们类型只定义了 Bool)

  • 定义,形式地,算术表达式的类型关系是项和类型之间的最小二元关系。如果存在某个 T,使得t:Tt:T,则称项 t 是可类型化的,或良类型的。

  • 定理,如果一个项是可类型化的,那么它的类型是唯一的。(t 的生成树唯一。)

# 安全性 = 进展 + 保持

  • 进展:一个良类型的项不会受阻。(要么它是一个值,要么它根据求值规则做下一步)

    保持:一个良类型的项做一步求值,所得的项仍是良类型的。

# 简单类型的 lambda 演算

  • 定义,类型 Bool 上的简单类型集合是由下列语法产生的:

    T::=BoolTTT::=Bool|T\rightarrow T

    类型构造子\rightarrow 是右结合的。可以把它理解为 “函数类型”。譬如BoolBoolBool\rightarrow Bool 就是一个布尔到布尔的函数类型,可以说λx.true:BoolBool\lambda x.true:Bool\rightarrow Bool

  • 我们可以对抽象确定参数类型:λx:T.t\lambda x:T.t,其中相当于要求了函数的自变量(参数)x 是 T 类型的。

  • 像上面直接用注释的形式t:Tt:T 标出项的类型的语言称为显式类型化语言。要求类型检查其自己推导类型的称为隐式类型化语言。显然我们主要讨论前者。

  • 定义抽象类型的推导规则:

    x:T1t2:T2λx:T1:t2:T1T2\frac{x:T_1\vdash t_2:T_2}{\vdash \lambda x:T_1:t_2:T_1\rightarrow T_2}

    中文说就是,如果确定参数 x 的类型为T1T_1 可以推导出函数体t2t_2 会返回一个T2T_2 类型的话,那么抽象λx:T1:t2\lambda x:T_1:t_2 也可以被推导出是一个T1T2T_1\rightarrow T_2 的函数。

  • 定义,一个类型环境(或称类型化的上下文)Γ\Gamma 是一个 变量 + 类型的序列。而逗号表示引入新的变量 + 类型来扩展Γ\Gamma

    譬如:Γ:{x:Nat}\Gamma:\{x:Nat\},则有Γiszro(x):Bool\Gamma\vdash iszro(x):Bool。相当于整了个假设大前提。显然{true:Bool}\emptyset\vdash\{true:Bool\},可以简写省略空集符号。

    我们用dom(Γ)dom(\Gamma) 表示Γ\Gamma 中规定了类型的变量的集合。

  • 抽象的类型规则一般表示为:

    Γ,x:T1t2:T2Γλx:T1.t2:T1T2(TAbs)\frac{\Gamma,x:T_1\vdash t_2:T_2}{\Gamma\vdash\lambda x:T_1.t_2:T_1\rightarrow T_2}\quad (T-Abs)

    中文说就是,如果Γ{x:T1}\Gamma\cup\{x:T_1\} 下可以推出t2:T2t_2:T_2,那么Γ\Gamma 下就可以推出λx:T1.t2:T1T2\lambda x:T_1.t_2:T_1\rightarrow T_2

  • 根据定义,也有:

    x:TΓΓx:T(TVar)\frac{x:T\in\Gamma}{\Gamma\vdash x:T}\quad(T-Var)

    前提x:TΓx:T\in\Gamma 读作 “在Γ\Gamma 中假设 x 的类型为 T”。

  • 定义应用的类型规则:

    Γt1:T1T2Γt2:T1Γt1  t2:T2(TApp)\frac{\Gamma\vdash t_1:T_1\rightarrow T_2\quad\Gamma\vdash t_2:T_1}{\Gamma\vdash t_1\;t_2:T_2}\quad(T-App)


  • 纯简单类型 lambda 演算的语法定义:

    t::=xλx:T.tt  tv::=λx:T.tT::=TTΓ::=Γ,x:Tt::=x|\lambda x:T.t|t\;t\\ v::=\lambda x:T.t\\ T::=T\rightarrow T\\ \Gamma::=\emptyset|\Gamma,x:T

    语义定义:

    t1t1t1  t2t1  t2(EApp1)t2t2v1  t2v1  t2(EApp2)(λx:T1.t1)  v2[xv2]t1(EAppAbs)x:TΓΓx:T(TVar)Γ,x:T1t2:T2Γλx:T1.t2:T1T2(TAbs)Γt1:T1T2Γt2:T1Γt1  t2:T2(TApp)\frac{t_1\rightarrow t_1'}{t_1\;t_2\rightarrow t_1'\;t_2}\quad(E-App_1)\\ \frac{t_2\rightarrow t_2'}{v_1\;t_2\rightarrow v_1\;t_2'}\quad(E-App_2)\\ (\lambda x:T_1.t_1)\;v_2\rightarrow [x\mapsto v_2]t_1\quad(E-AppAbs)\\ \frac{x:T\in\Gamma}{\Gamma\vdash x:T}\quad(T-Var)\\ \frac{\Gamma,x:T_1\vdash t_2:T_2}{\Gamma\vdash\lambda x:T_1.t_2:T_1\rightarrow T_2}\quad (T-Abs)\\ \frac{\Gamma\vdash t_1:T_1\rightarrow T_2\quad\Gamma\vdash t_2:T_1}{\Gamma\vdash t_1\;t_2:T_2}\quad(T-App)\\

    我们用λ\lambda_\rightarrow 来表示简单类型的 lambda 演算。

# 类型的性质

  • 定理,类型唯一性:在一个给定的类型环境Γ\Gamma 中,一个项 t (FV(t)dom(Γ)FV(t)\in dom(\Gamma)),至多有一个类型。

  • 定理 [进展]:若 t 是一个封闭的,良类型的项(即存在 T,使得t:T\vdash t:T),则 t 要么是一个值,要么存在tt' 使ttt\rightarrow t'

  • 引理 [置换]:如果Γt:T\Gamma\vdash t:TΔ\DeltaΓ\Gamma 的一个置换,则Δt:T\Delta\vdash t:T。(感觉是废话,因为集合是无序的)

  • 引理 [弱化]:如果Γt:T\Gamma\vdash t:Txdom(Γ)x\notin dom(\Gamma),则Γ,x:St:T\Gamma,x:S\vdash t:T。(即加了个没用的绑定)

  • 引理 [类型在代换下保持]:如果Γ,x:St:T\Gamma,x:S\vdash t:TΓs:S\Gamma\vdash s:S,则Γ[xs]t:T\Gamma\vdash[x\mapsto s]t:T

  • 定理 [保持]:如果Γt:T\Gamma\vdash t:Tttt\rightarrow t',则Γt:T\Gamma\vdash t':T

# Curry-Howard 对应

  • 关于T1T2T_1\rightarrow T_2 这样的类型有两种类型规则:

    • 引入规则(T-Abs),描述该类型的元素是如何产生的。
    • 消去规则(T-App),描述该类型的元素是如何使用的。
  • Curry-Howard 对应(Curry-Howard 同构):

    逻辑 程序语言
    命题 类型
    命题PQP\supset Q 类型PQP\rightarrow Q
    命题PQP\wedge Q 类型P×QP\times Q
    命题 P 的证明 类型 P 的一个项 t
    命题 P 是可证明的 有一个项 t 是类型 P 的

# 抹除和类型性

  • 可以定义 erase 函数去抹除对项的类型注释:

    erase(x)=xerase(λx:T1.t2)=λx.erase(t2)erase(t1  t2)=erase(t1)  erase(t2)erase(x)=x\\ erase(\lambda x:T_1.t_2)=\lambda x.erase(t_2)\\ erase(t_1\;t_2)=erase(t_1)\;erase(t_2)

  • 定理,若ttt\rightarrow t',则erase(t)erase(t)erase(t)\rightarrow erase(t')。若erase(t)merase(t)\rightarrow m,则存在tt',使得tt,erase(t)=mt\rightarrow t',erase(t')=m

  • 定义,无类型 lambda 演算中一个项 m,如果存在某个简单类型项 t,类型 T 和上下文Γ\Gamma 使得erase(t)=merase(t)=mΓt:T\Gamma\vdash t:T,则 m 在λ\lambda_\rightarrow 中是可类型化的

# 简单扩展

  • 我们用 A 表示基本类型(String,Float,Nat,Bool 等),用 Unit 表示单位类型。于是有扩展:

    T::=...AUnitt::=...unitv::=...unitΓunit:Unitt1;t2=(λx:Unit.t2)  t1,xFV(t2)T::=...|A|Unit\\ t::=...|unit\\ v::=...|unit\\ ----------------\\ \Gamma\vdash unit:Unit\\ t_1;t_2=(\lambda x:Unit.t_2)\;t_1,x\notin FV(t_2)

    Unit 的作用类似于 C 和 Java 中的 void 类型。

# 序列和通配符

  • 定义序列:t::=...t1;t2t::=...|t_1;t_2

  • 定义对序列t1;t2t_1;t_2 的求值规则和类型规则:

t1t1t1;t2t1;t2(ESeq)unit;t2t2Γt1:UnitΓt2:T2Γt1;t2:T2(TSeq)\frac{t_1\rightarrow t_1'}{t_1;t_2\rightarrow t_1';t_2}\quad(E-Seq)\\ unit;t_2\rightarrow t_2\\ \frac{\Gamma\vdash t_1:Unit\quad \Gamma\vdash t_2:T_2}{\Gamma\vdash t_1;t_2:T_2}\quad(T-Seq)

​ 这时候,会发现这个求值规则实际上是符合t1;t2=(λx:Unit.t2)  t1t_1;t_2=(\lambda x:Unit.t_2)\;t_1 的定义的。我们可以把序列看作这样一个 λ 抽象的缩写。

  • 定理,用λE\lambda^E 表示带序列的简单类型 lambda 演算,λI\lambda^I 表示只带 Unit 类型的简单类型 lambda 演算。

    eλEλIe\in\lambda^E\rightarrow\lambda^I,e 表示用(λx:Unit.t2)  t1(\lambda x:Unit.t_2)\;t_1 去替换t1;t2t_1;t_2。于是对λE\lambda^E 中的每个项,都有:

    • tEtt\rightarrow_E t' 当且仅当e(t)Ie(t)e(t)\rightarrow_I e(t')
    • ΓEt:T\Gamma\vdash^E t:T 当且仅当ΓIe(t):T\Gamma\vdash^I e(t):T

    其实序列是我们写程序时常用的顺序结构。上述定理说明了序列可以用更基本的类型和求值行为推导出。注意到我们用λI\lambda^I 去替换序列时,有要求xFV(t2)x\notin FV(t_2),所以有时候也会写成(λ_:Unit.t2)  t1(\lambda\_:Unit.t_2)\;t_1

# 归属

  • 定义 “将类型 T 归属到项 t”:

    t::=...t  as  Tt::=...|t\;as\;T

  • 定义对应的求值规则:

    v1  as  Tv1(EAscribe)t1t1t1  as  Tt1  as  T(EAscribe1)v_1\;as\;T\rightarrow v_1\quad(E-Ascribe)\\ \frac{t_1\rightarrow t_1'}{t_1\;as\;T\rightarrow t_1'\;as\;T}\quad (E-Ascribe1)\\

  • 定义对应的类型规则:

    Γt1:TΓt1  as  T:T(TAscribe)\frac{\Gamma\vdash t_1:T}{\Gamma\vdash t_1\;as\;T:T}\quad(T-Ascribe)

归属可以用来做 typedef。譬如:

UU  as  UnitUnit;(λf:UU.f  unit)(λx:Unit.x);UU\;as\;Unit\rightarrow Unit;\\ (\lambda f:UU.f\;unit)(\lambda x:Unit.x);

就可以很容易推导出:(λf:UU.f  unit)(λx:Unit.x):Unit(\lambda f:UU.f\;unit)(\lambda x:Unit.x):Unit

# let 绑定

  • 语法定义:

    t::=...let  x=t  in  tt::=...|let\;x=t\; in\;t

  • 求值规则:

    let  x=v1  in  t2[xv1]t2(ELETV)t1t1let  x=t1  in  t2let  x=t1  in  t2(ELET)let\;x=v_1\;in\;t_2\rightarrow [x\mapsto v_1]t_2\quad(E-LETV)\\ \frac{t_1\rightarrow t_1'}{let\;x=t_1\;in\;t_2\rightarrow let\;x=t_1'\;in\;t_2}\quad(E-LET)

  • 类型规则:

    Γt1:T1Γ,x:T1t2:T2let  x=t1  in  t2:T2(TLET)\frac{\Gamma\vdash t_1:T_1\quad\Gamma,x:T_1\vdash t_2:T_2}{let\;x=t_1\;in\;t_2:T_2}\quad(T-LET)

这东西的理解,首先应该把它看成let  (x=t1)  in  t2let\;(x=t_1)\;in\;t_2,意思为在表达式t2t_2 中,绑定xxt1t_1 的求值。譬如let  x=3+5  in  x2let\;x=3+5\;in\;x-2

也可以用一个 lambda 抽象来等价地表示它:let  x=t1  in  t2=(λx:T1.t2)  t1let\;x=t_1\;in\;t_2=(\lambda x:T_1.t_2)\;t_1

在出现 let 绑定时,类型检查器一定会有一个推导:

...Γt1:T1...Γ,x:T1t2:T2let  x=t1  in  t2:T2(TLET)\frac{\frac{...}{\Gamma\vdash t_1:T_1}\quad\frac{...}{\Gamma,x:T_1\vdash t_2:T_2}}{let\;x=t_1\;in\;t_2:T_2}\quad(T-LET)

这个推导就对应了 lambda 抽象的一个推导:

...Γ,x:T1t2:T2Γλx:T1.t2:T1T2...Γt1:T1Γ(λx:T1.T2)  t1:T2\frac{\frac{\frac{...}{\Gamma,x:T_1\vdash t_2:T_2}}{\Gamma\vdash\lambda x:T_1.t_2:T_1\rightarrow T_2}\quad\frac{...}{\Gamma\vdash t_1:T_1}}{\Gamma\vdash(\lambda x:T_1.T_2)\;t_1:T_2}

# 序对

  • 语法定义:

    t::=...{t,t}t.1t.2v::=...{v,v}T::=T1×T2t::=...|\{t,t\}|t.1|t.2\\ v::=...|\{v,v\}\\ T::=T_1\times T_2

  • 求值规则:

    {v1,v2}.1v1(EPAIRBETA1){v1,v2}.2v2(EPAIRBETA2)t1t1t1.1t1.1(EPROJ1)t1t1t1.2t1.2(EPROJ2)t1t1{t1,t2}{t1,t2}(EPAIR1)t2t2{v1,t2}{v1,t2}(EPAIR2)\{v_1,v_2\}.1\rightarrow v_1\quad(E-PAIRBETA1)\\ \{v_1,v_2\}.2\rightarrow v_2\quad(E-PAIRBETA2)\\ \frac{t_1\rightarrow t_1'}{t_1.1\rightarrow t_1'.1}\quad(E-PROJ1)\\ \frac{t_1\rightarrow t_1'}{t_1.2\rightarrow t_1'.2}\quad(E-PROJ2)\\ \frac{t_1\rightarrow t_1'}{\{t_1,t_2\}\rightarrow\{t_1',t_2\}}\quad(E-PAIR1)\\ \frac{t_2\rightarrow t_2'}{\{v_1,t_2\}\rightarrow\{v_1,t_2'\}}\quad(E-PAIR2)

  • 类型规则:

    Γt1:T1Γt2:T2Γ{t1,t2}:T1×T2(TPAIR)Γt1:T1×T2Γt1.1:T1(TPROJ1)Γt1:T1×T2Γt1.2:T2(TPROJ2)\frac{\Gamma\vdash t_1:T_1\quad \Gamma\vdash t_2:T_2}{\Gamma\vdash\{t_1,t_2\}:T_1\times T_2}\quad(T-PAIR)\\ \frac{\Gamma\vdash t_1:T_1\times T_2}{\Gamma\vdash t_1.1:T_1}\quad(T-PROJ1)\\ \frac{\Gamma\vdash t_1:T_1\times T_2}{\Gamma\vdash t_1.2:T_2}\quad(T-PROJ2)\\

    这就是平常用的 C++ 里的 pair。用它可以扩展成元组,数组。要注意的是,无论求 1 还是 2,或者代入函数时,都必须把两项都算出值:

    (λx:Nat×Nat.x.2){pred  4,pred  5}(λx:Nat×Nat.x.2){3,pred  5}(λx:Nat×Nat.x.2){3,4}{3,4}.22(\lambda x:Nat\times Nat.x.2)\{pred\;4,pred\;5\}\\ \rightarrow(\lambda x:Nat\times Nat.x.2)\{3,pred\;5\}\\ \rightarrow(\lambda x:Nat\times Nat.x.2)\{3,4\}\\ \rightarrow\{3,4\}.2\\ \rightarrow 2

# 元组

  • 语法定义:

    t::=...{ti,i1..n}t.iv::={vi,i1..n}T::={Ti,i1..n}t::=...|\{t_i,i\in1..n\}|t.i\\ v::=\{v_i,i\in1..n\}\\ T::=\{T_i,i\in1..n\}

  • 求值规则:

    {vi,i1..n}.jvjt1t1t1.it1.itjtj{vi,i1..j1,vj,vi,ij+1..n}{vi,i1..j1,vj,vi,ij+1..n}\{v_i,i\in1..n\}.j\rightarrow v_j\\ \frac{t_1\rightarrow t_1'}{t_1.i\rightarrow t_1'.i}\\ \frac{t_j\rightarrow t_j'}{\{v_i,i\in1..j-1,v_j,v_i,i\in j+1..n\}\rightarrow\{v_i,i\in1..j-1,v_j',v_i,i\in j+1..n\}}

  • 类型规则:

    foreach  i,Γti:T1Γ{ti,i1..n}:{Ti,i1..n}Γt1:{Ti,i1..n}Γt1.j:Tj\frac{foreach\;i,\Gamma\vdash t_i:T_1}{\Gamma\vdash\{t_i,i\in1..n\}:\{T_i,i\in1..n\}}\\ \frac{\Gamma\vdash t_1:\{T_i,i\in 1..n\}}{\Gamma\vdash t_1.j:T_j}

    这就是最常用的元组类型(允许不同类型放在一起)。实例:

    {1,2,3,true,false}\{1,2,3,true,false\}

# 记录

  • 语法定义

    t::=...{li=ti,i1..n}t.lv::=...{li=vi,i1..n}T::=...{li:Ti,i1..n}t::=...|\{l_i=t_i,i\in1..n\}|t.l\\ v::=...|\{l_i=v_i,i\in 1..n\}\\ T::=...|\{l_i:T_i,i\in 1..n\}

  • 求值规则

    {li=vi,i1..n}.ljvjt1t1t1.lt1.ltjtj{li=vi,i1..j1,lj=tj,li=ti,ij+1..n}{li=vi,i1..j1,lj=tj,li=ti,ij+1..n}\{l_i=v_i,i\in1..n\}.l_j\rightarrow v_j\\ \frac{t_1\rightarrow t_1'}{t_1.l\rightarrow t_1'.l}\\ \frac{t_j\rightarrow t_j'}{\{l_i=v_i,i\in 1..j-1,l_j=t_j,l_i=t_i,i\in j+1..n\}\rightarrow\{l_i=v_i,i\in 1..j-1,l_j=t_j',l_i=t_i,i\in j+1..n\}}

    注意这里面从左到右求值的含义,左侧都是值了,才能求值。

  • 类型规则

    foreach  i,Γti:TiΓ{li=ti,i1..n}:{li:Ti,i1..n}Γt1:{li:Ti,i1..n}Γt1.lj:Tj\frac{foreach\;i,\Gamma\vdash t_i:T_i}{\Gamma\vdash\{l_i=t_i,i\in1..n\}:\{l_i:T_i,i\in1..n\}}\\ \frac{\Gamma\vdash t_1:\{l_i:T_i,i\in1..n\}}{\Gamma\vdash t_1.l_j:T_j}

这其实有些类似 map。但是它支持了不同类型放在一起。给出实例一个:

{patato:100,tomato:true}:{patato:Nat,tomato:Bool}\{patato:100,tomato:true\}:\{patato:Nat,tomato:Bool\}

#

  • 语法定义:

    t::=...inl  tinr  t(case  t  of  inl  xtinr  xt)v::=...inl  vinr  vT::=...T+Tt::=...|inl\;t|inr\;t|(case\;t\;of\;inl\;x\Rightarrow t|inr\;x\Rightarrow t)\\ v::=...|inl\;v|inr\;v\\ T::=...|T+T

  • 求值规则:

    case  (inl  v0)  of  inl  x1t1inr  x2t2[x1v0]t1case  (inr  v0)  of  inl  x1t1inr  x2t2[x2v0]t2t0t0case  t0  of  inl  x1t1inr  x2t2case  t0  of  inl  x1t1inr  x2t2t1t1inl  t1inl  t1t1t1inr  t1inr  t1case\;(inl\;v_0)\;of\;inl\;x_1\Rightarrow t_1|inr\;x_2\Rightarrow t_2\\ \rightarrow[x_1\mapsto v_0]t_1\\ case\;(inr\;v_0)\;of\;inl\;x_1\Rightarrow t_1|inr\;x_2\Rightarrow t_2\\ \rightarrow[x_2\mapsto v_0]t_2\\ \frac{t_0\rightarrow t_0'}{case\;t_0\;of\;inl\;x_1\Rightarrow t_1|inr\;x_2\Rightarrow t_2\rightarrow case\;t_0'\;of\;inl\;x_1\Rightarrow t_1|inr\;x_2\Rightarrow t_2}\\ \frac{t_1\rightarrow t_1'}{inl\;t_1\rightarrow inl\;t_1'}\\ \frac{t_1\rightarrow t_1'}{inr\;t_1\rightarrow inr\;t_1'}

  • 类型规则:

    Γt1:T1Γinl  t1:T1+T2Γt1:T2Γinr  t1:T1+T2Γt0:T1+T2Γ,x1:T1t1:T1Γ,x2:T2t2:T2Γcase  t0  of  inl  x1t1inr  x2t2:T\frac{\Gamma\vdash t_1:T_1}{\Gamma\vdash inl\;t_1:T_1+T_2}\\ \frac{\Gamma\vdash t_1:T_2}{\Gamma\vdash inr\;t_1:T_1+T_2}\\ \frac{\Gamma\vdash t_0:T_1+T_2\quad\Gamma,x_1:T_1\vdash t_1:T_1\quad\Gamma,x_2:T_2\vdash t_2:T_2}{\Gamma\vdash case\;t_0\;of\;inl\;x_1\Rightarrow t_1|inr\;x_2\Rightarrow t_2:T}

  • 怎么理解这个类型呢?根据我的理解,这实际上是在 “取并集”。譬如两个记录类型:

    PhysicalAddr={firstlast:String,addr:String}VirtualAddr={name:String,email:String}PhysicalAddr=\{firstlast:String,addr:String\}\\ VirtualAddr=\{name:String,email:String\}

    Addr=PhysicalAddr+VirtualAddrAddr=PhysicalAddr+VirtualAddr。那么对于任意一个AddrAddr 类型的项 t,t 要么是 Physical 的,要么是 Virtual 的,因为它的生成规则一定是:

    tinl  (t:PhysicalAddr):Addrortinr  (t:VirtualAddr):Addrt\equiv inl\;(t':PhysicalAddr):Addr\\ or\\ t\equiv inr\;(t':VirtualAddr):Addr

    就是对于两个不同的类型,把它们并起来获得一个新的大类型。但对这个大类型,我们又可以根据其中项究竟属于哪个小类型来操作:

    getName=λa:Addr.case  a  of  inl  xx.firstlastinr  yy.namegetName=\lambda a:Addr.case\;a\;of\;inl\;x\Rightarrow x.firstlast|inr\;y\Rightarrow y.name

    getNamegetName 是一个AddrStringAddr\rightarrow String 的函数,它的输入值相当于放宽了类型,无论是 Physical 还是 Virtual 都可以传进去,然后分类进行取 name。

  • 此时其实会破坏类型的唯一性。即确定项t=inl  t:T1t=inl\;t':T_1 的类型不再唯一。例如inl  5inl\;5 可以为Nat+NatNat+Nat 也可以为Nat+BoolNat+Bool。所以可以更改语法规则:

    t::=...inl  t  as  T...t::=...|inl\;t\;as\;T|...

    这样要求了inl  tinl\;t 的类型。inl  5  as  Nat+Natinl\;5\;as\;Nat+Nat。然后求值和类型规则都需要重写。

# 变式

  • 语法定义:

    t::=...<l=t>  as  Tcase  t  of  <li=xi>ti,i1..nT::=...<li:Ti>,in1..nt::=...|<l=t>\;as\;T|case\;t\;of\;<l_i=x_i>\Rightarrow t_i,i\in1..n\\ T::=...|<l_i:T_i>,in\in1..n

  • 求值规则:

    case  (<lj=vj>  as  T)  of  <li=xi>ti,i1..n[xjvj]tjt0t0case  t0  of  <li=xi>ti,i1..ncase  t0  of  <li=xi>ti,i1..ntiti<li=ti>  as  T<li=ti>  as  Tcase\;(<l_j=v_j>\;as\;T)\;of\;<l_i=x_i>\Rightarrow t_i,i\in1..n\rightarrow[x_j\mapsto v_j]t_j\\ \frac{t_0\rightarrow t_0'}{case\;t_0\;of\;<l_i=x_i>\Rightarrow t_i,i\in1..n\rightarrow case\;t_0'\;of\;<l_i=x_i>\Rightarrow t_i,i\in1..n}\\ \frac{t_i\rightarrow t_i'}{<l_i=t_i>\;as\;T\rightarrow <l_i=t_i'>\;as\;T}\\

  • 类型规则:

    Γtj:TjΓ<lj=tj>  as  <li:Ti>,i1..n:<li:Ti>,i1..nΓt0:<li:Ti>,i1..nforeach  i  Γ,xi:Titi:TΓcase  t0  of  <li=xi>ti,i1..n:T\frac{\Gamma\vdash t_j:T_j}{\Gamma\vdash<l_j=t_j>\;as\;<l_i:T_i>,i\in1..n:<l_i:T_i>,i\in1..n}\\ \frac{\Gamma\vdash t_0:<l_i:T_i>,i\in1..n\quad foreach\;i\;\Gamma,x_i:T_i\vdash t_i:T}{\Gamma\vdash case\;t_0\;of\;<l_i=x_i>\Rightarrow t_i,i\in 1..n:T}

  • 变式实际上是和的推广。inl  t  as  Tinl\;t\;as\;T 扩展成了<li=ti>  as  T<l_i=t_i>\;as\;T

    于是之前在和那里的例子可以为:

    Addr=<physical:PhysicalAddr,virtual:VirtualAddr>;Addr=<physical:PhysicalAddr,virtual:VirtualAddr>;\\

    那么 Addr 的一个实例 a,生成形式一定是:

    a<physical=t>  as  Addrora<virtual=t>  as  Addra\equiv <physical=t>\;as\;Addr\\ or\\ a\equiv <virtual=t>\;as\;Addr

    然后仍然可以 getName:

    getName=λa:Addr.case  a  of<physical=x>x.firstlast<virtual=y>y.namegetName=\lambda a:Addr.\\ case\;a\;of\\ <physical=x>\Rightarrow x.firstlast\\ |<virtual=y>\Rightarrow y.name

    getName:AddrStringgetName:Addr\rightarrow String

  • 此外,变式可以用来选值。考虑这样一个变式类型:

    OptionalNat=<none:Unit,some:Nat>OptionalNat=<none:Unit,some:Nat>

    于是实际上可以进行查询:

    query=λa:OptionalNat.case  a  of<none=x>1<some=y>yquery=\lambda a:OptionalNat.\\ case\;a\;of\\ <none=x>\Rightarrow-1\\ |<some=y>\Rightarrow y

    这实际上就是一个查询query:OptionalNatNatquery:OptionalNat\rightarrow Nat,就是对OptionalNatOptionalNat 类型的变量确定它究竟是个 Nat 还是个 Unit。这里 Optional 我认为理解为可以是若干类型中的一个。

  • 还有单字段的变式:<t1:T1><t_1:T_1>。他有什么用呢?它可以用来区分 “不同意义的相同类型”。譬如,我的钱无论是美元,还是欧元,都可以用浮点数表示。那怎么区分它是欧元还是美元呢,实际上可以用单字段变式来定义新的类型,来加 “单位”:

    dollarAmount=<amount:Float>euroAmout=<amount:Float>dollarAmount=<amount:Float>\\ euroAmout=<amount:Float>

    那么,美元转欧元的话,就必须输入是美元类型:

    dollar2euro=λa:dollarAmount.case  a  of<amount=x><amount=times  x  1.03>  as  euroAmountdollar2euro:dollarAmounteuroAmountdollar2euro=\lambda a:dollarAmount.\\ case\;a\;of\\ <amount=x>\Rightarrow <amount=times\;x\;1.03>\;as\;euroAmount\\ dollar2euro:dollarAmount\rightarrow euroAmount

# 枚举

  • 枚举是变式的退化,其中每个字段都是 Unit 类型。譬如:

    Weekday=<monday:Unit,tuesday:Unit,wednesday:Unit,thursday:Unit,friday:Unit>Weekday=<monday:Unit,tuesday:Unit,wednesday:Unit,\\thursday:Unit,friday:Unit>

    然后譬如就可以有:

    nextBusinessDay=λw:Weekday.case  w  of  <monday=x><tuesday=unit>  as  Weekday<tuesday=x><wednesday=unit>  as  Weekday<wednesday=x><thursday=unit>  as  Weekday<thursday=x><friday=unit>  as  Weekday<friday=x><monday=unit>  as  WeekdaynextBusinessDay:WeekdayWeekdaynextBusinessDay=\lambda w:Weekday.\\ case\;w\;of\;<monday=x>\Rightarrow<tuesday=unit>\;as\;Weekday\\ |<tuesday=x>\Rightarrow<wednesday=unit>\;as\;Weekday\\ |<wednesday=x>\Rightarrow<thursday=unit>\;as\;Weekday\\ |<thursday=x>\Rightarrow<friday=unit>\;as\;Weekday\\ |<friday=x>\Rightarrow<monday=unit>\;as\;Weekday\\ nextBusinessDay:Weekday\rightarrow Weekday

# 一般递归

  • 语法形式:

    t::=...fix  tt::=...|fix\;t

  • 求值规则:

    fix  (λx:T1.t2)[x(fix  (λx:T1.t2))]t2t1t1fix  t1fix  t1fix\;(\lambda x:T_1.t_2)\rightarrow[x\mapsto(fix\;(\lambda x:T_1.t_2))]t_2\\ \frac{t_1\rightarrow t_1'}{fix\;t_1\rightarrow fix\;t_1'}

  • 类型规则:

    Γt1:T1T1Γfix  t1:T1\frac{\Gamma\vdash t_1:T_1\rightarrow T_1}{\Gamma\vdash fix\;t_1:T_1}

  • 导出式:

    letrec  x:T1=t1  in  t2=deflet  x=fix  (λx:T1.t1)  in  t2letrec\;x:T_1=t_1\;in\;t_2\\=_{def} let\;x=fix\;(\lambda x:T_1.t_1)\;in\;t_2

  • 解释一下。fix 直接定义成了一个语法,并且给出了它的规则。fix 其实作用是给出函数的不动点。譬如g:NatNatg:Nat\rightarrow Nat,则g  (fix  g)=fix  gg\;(fix\;g)=fix\;g。所以g:(NatNat)Natg:(Nat\rightarrow Nat)\rightarrow Nat

    在之前,其实给出了无类型的 fix:

    fix=λf.(λx.f  (λy.x  x  y))(λx.f  (λy.x  x  y))fix=\lambda f.(\lambda x.f\;(\lambda y.x\;x\;y))(\lambda x.f\;(\lambda y.x\;x\;y))

    然而类型环境下是需要考虑不动点是否存在的。然后再写一个产生器。以阶乘为例:

    ff=λg:NatNat.λn:Nat.if  iszro(n)  then  1  else  g(pred(n));ff:(NatNat)NatNatff=\lambda g:Nat\rightarrow Nat.\lambda n:Nat.if\;iszro(n)\;then\;1\;else\;g(pred(n));\\ ff:(Nat\rightarrow Nat)\rightarrow Nat\rightarrow Nat

    那么 ff 的不动点是啥?实际上,就是g=λx:Nat.x!g=\lambda x:Nat.x!。所以对 ff 求不动点,本质上就是把递归函数 g 的显形式解出来。

    F=fix  ffff  F=FF=fix\;ff\\ ff\;F=F

    当然,这个显形式如果fixfix 就按上面的定义的话,本质就是一层一层展开,导致很长。

# 引用

# 基础

  • 我们定义新算子 ref,表示为新的单元提供一个初始值:

    r=ref  5;r=ref\;5;

    它的类型表示为:r:Ref  Natr:Ref\;Nat

  • 同样可以定义反引用算子!:

    !r;!(ref  5):Nat!r;\\ !(ref\;5):Nat

  • 定义赋值算子:

    r:=7;r:=7;

    整个赋值式的结果就是一个 Unit 类型(平凡类型):

    (r:=7)unit:Unit(r:=7)\rightarrow unit:Unit

    回顾之前,其实赋值语句类型是 unit 很好地符合了 “序对” 的要求,即我们可以很好地顺序执行:

    (r:=7;!r)7:Nat(r:=7;!r)\rightarrow 7:Nat

    来替换:

    (λ_:Unit.!r)(r:=succ(!r))9:Nat(\lambda\_:Unit.!r)(r:=succ(!r))\rightarrow 9:Nat

# 引用和别名

  • 考虑引用 r,s:

    r=ref  5;s=r;r=ref\;5;\\ s=r;

    s:Ref  Nats:Ref\;Nat。而且他们指向同一单元。于是有:

    s:=83;!r83s:=83;\\ !r\rightarrow 83

    引用 r 和 s 称为是同一个单元的别名。

# 复合类型的引用

NatArray=Ref  (NatNat)NatArray=Ref\;(Nat\rightarrow Nat)

表示数组类型。

newarray=λ_Unit.ref  (λn:Nat.0)newarray=\lambda\_Unit.ref\;(\lambda n:Nat.0)

然后newarray  unit;newarray\;unit; 就实现了新建一个全为 0 的数组的引用。

lookup=λa:NatArray.λn:Nat.(!a)  n;lookup=\lambda a:NatArray.\lambda n:Nat.(!a)\;n;

表示查询数组的第 n 位。

update=λa:NatArray.λm:Nat.λv:Nat.letoldf=!aina:=(λn:Nat.if qual m n then v else oldf n);update=\lambda a:NatArray.\lambda m:Nat.\lambda v:Nat.\\ let\,oldf=!a\,in\\ a:=(\lambda n:Nat.if\ qual\ m\ n\ then\ v\ else\ oldf\ n);\\

update:NatArrayNatNatUnitupdate:NatArray\rightarrow Nat\rightarrow Nat\rightarrow Unit。是一个更新操作。

# 引用的类型规则

Γt1:T1Γ:ref t1:Ref T1Γt1:Ref T1Γ!t1:T1Γt1:Ref T1Γt2:Ref T1Γt1:=t2:Unit\frac{\Gamma\vdash t_1:T_1}{\Gamma:ref\ t_1:Ref\ T_1}\\ \frac{\Gamma\vdash t_1:Ref\ T_1}{\Gamma\vdash !t_1:T_1}\\ \frac{\Gamma\vdash t_1:Ref\ T_1\quad \Gamma\vdash t_2:Ref\ T_1}{\Gamma\vdash t_1:=t_2:Unit}


# 引用的规则汇总

  • 定义一个存储μ\mu,表示存储单元到值得映射μ(l)=v\mu(l)=v。一个类型上下文Γ\Gamma。一个存储类型Σ\Sigma 是存储单元到类型得映射Σ(l)=T\Sigma(l)=T。如果有dom(μ)=dom(Σ)dom(\mu)=dom(\Sigma) 且对每个ldom(μ),ΓΣμ(l):Σ(l)l\in dom(\mu),\Gamma|\Sigma\vdash\mu(l):\Sigma(l) 成立,则称μ\mu 是良类型的,记为ΓΣμ\Gamma|\Sigma\vdash\mu。一个存储μ\mu 和一个存储类型Σ\Sigma 是一致的。

  • 语法定义:

    t::=x|\lambda x:T.t|t\ t|unit|ref\ t|!t|t:=t|l\ v::=\lambda x:T.t|unit|l\\ T::=T\rightarrow T|Unit|Ref\ T\\ \Gamma::=\emptyset|\Gamma,x:T\\ \mu::=\emptyset|\mu,l=v\\ \Sigma::=\emptyset|\Sigma,l:T

    其中ll 表示存储位置,μ,l=v\mu,l=v 表示新的存储绑定。

  • 类型规则:

    x:TΓΓΣx:TΓ,x:T1Σt2:T2ΓΣλx:T1.t2:T1T2ΓΣt1:T1T2ΓΣt2:T1ΓΣt1 t2:T2ΓΣunit:UnitΣ(l)=T1ΓΣl:Ref T1ΓΣt1:T1ΓΣref t1:Ref T1ΓΣt1:Ref T1ΓΣ!t1:T1ΓΣt1:Ref T1ΓΣt2:T1ΓΣt1:=t2:Unit\frac{x:T\in \Gamma}{\Gamma|\Sigma\vdash x:T}\\ \frac{\Gamma,x:T_1|\Sigma\vdash t_2:T_2}{\Gamma|\Sigma\vdash\lambda x:T_1.t_2:T_1\rightarrow T_2}\\ \frac{\Gamma|\Sigma\vdash t_1:T_1\rightarrow T_2\quad \Gamma|\Sigma\vdash t_2:T_1}{\Gamma|\Sigma\vdash t_1\ t_2:T_2}\\ \Gamma|\Sigma\vdash unit:Unit\\ \frac{\Sigma(l)=T_1}{\Gamma|\Sigma\vdash l:Ref\ T_1}\\ \frac{\Gamma|\Sigma\vdash t_1:T_1}{\Gamma|\Sigma\vdash ref\ t_1:Ref\ T_1}\\ \frac{\Gamma|\Sigma\vdash t_1:Ref\ T_1}{\Gamma|\Sigma\vdash !t_1:T_1}\\ \frac{\Gamma|\Sigma\vdash t_1:Ref\ T_1\quad\Gamma|\Sigma\vdash t_2:T_1}{\Gamma|\Sigma\vdash t_1:=t_2:Unit}

  • 求值规则:

    t1μt1μt1 t2μt1 t2μt1μt1μv t1μv t1μ(λx:T1.t2) v2μ[xv2]t2μldom(μ)ref v1μl(μ,lv1)t1μt1μref t1μref t1μμ(l)=v!lμvμt1μt1μ!t1μ!t1μ......\frac{t_1|\mu\rightarrow t_1'|\mu'}{t_1\ t_2|\mu\rightarrow t_1'\ t_2|\mu'}\\ \frac{t_1|\mu\rightarrow t_1'|\mu'}{v\ t_1|\mu\rightarrow v\ t_1'|\mu'}\\ (\lambda x:T_1.t_2)\ v_2|\mu\rightarrow[x\mapsto v_2]t_2|\mu\\ \frac{l\notin dom(\mu)}{ref\ v_1|\mu\rightarrow l|(\mu,l\mapsto v_1)}\\ \frac{t_1|\mu\rightarrow t_1'|\mu'}{ref\ t_1|\mu\rightarrow ref\ t_1'|\mu'}\\ \frac{\mu(l)=v}{!l|\mu\rightarrow v|\mu}\\ \frac{t_1|\mu\rightarrow t_1'|\mu'}{!t_1|\mu\rightarrow !t_1'|\mu'}\\ ......

    注意现在求值会附带个μ\mu,求值可能引起μ\mu 的改变。


  • 定理 [保持]:

    如果

    ΓΣt:TΓΣμtμtμ\Gamma|\Sigma\vdash t:T\\ \Gamma|\Sigma\vdash\mu\\ t|\mu\rightarrow t'|\mu'

    则对某个ΣΣ\Sigma'\supseteq\Sigma,有

    ΓΣt:TΓΣμ\Gamma|\Sigma'\vdash t':T\\ \Gamma|\Sigma'\vdash \mu'

    为什么会要求ΣΣ\Sigma'\supseteq \Sigma 呢?因为对于一个新的项tt',他可能比 t 多的是一个ref 10ref\ 10 的部分,那么根据求值规则就会:

    ref 10μl(μ,l10)ref\ 10|\mu\rightarrow l|(\mu,l\mapsto 10)

    会扩大μ\mu,新分配一个地址 l。那么那 “某个Σ\Sigma'” 就是(Σ,lT1)(\Sigma,l\mapsto T_1) 了。否则如果没有新开地址 l,那就可以是Σ\Sigma

  • 引理 [代换]:

    如果

    Γ,x:SΣt:TΓΣs:S\Gamma,x:S|\Sigma\vdash t:T\\ \Gamma|\Sigma\vdash s:S

    那么

    ΓΣ[xs]t:T\Gamma|\Sigma\vdash[x\mapsto s]t:T

  • 引理:

    如果

    ΓΣμΣ(l)=TΓΣv:T\Gamma|\Sigma\vdash\mu\\ \Sigma(l)=T\\ \Gamma|\Sigma\vdash v:T

    那么

    ΓΣ[lv]μ\Gamma|\Sigma\vdash[l\mapsto v]\mu

  • 定理 [进展]:

    如果

    t 是一个封闭的、良类型的项(即对某个 T 和Σ\Sigma,有Σt:T\emptyset|\Sigma\vdash t:T

    t 要么是一个值,要么对任何存储μ\mu 使Σμ\emptyset|\Sigma\vdash\mu,存在某个项tt' 和存储μ\mu',使得tμtμt|\mu\rightarrow t'|\mu'

# 异常

# 提出异常

  • 语法形式:

    t::=...errort::=...|error

  • 求值规则:

    error  t2errorv1  errorerrorerror\;t_2\rightarrow error\\ v_1\;error\rightarrow error

  • 类型规则:

    Γerror:T\Gamma\vdash error:T

    errorerror 允许是任何类型,在任何上下文中出现。所以它破坏了类型的唯一性原理。

# 异常处理

  • 语法形式:

    t::=...try  t  with  tt::=...|try\;t\;with\;t

  • 求值规则:

    try  v1  with  t2v1try  error  with  t2t2t1t1try  t1  with  t2try  t1  with  t2try\;v_1\;with\;t_2\rightarrow v_1\\ try\;error\;with\;t_2\rightarrow t_2\\ \frac{t_1\rightarrow t_1'}{try\;t_1\;with\;t_2\rightarrow try\;t_1'\;with\;t_2}

  • 类型规则:

    Γt1:T1Γt2:TΓtry  t1  with  t2:T\frac{\Gamma\vdash t_1:T_1\quad\Gamma\vdash t_2:T}{\Gamma\vdash try\;t_1\;with\;t_2:T}

# 带值得异常

  • 语法形式:

    t::=...raise  ttry  t  with  tt::=...|raise\;t|try\;t\;with\;t

  • 求值规则:

    (raise  v1)  t2raise  v1v1  (raise  v2)raise  v2t1t1raise  t1raise  t1raise  (raise  v1)raise  v1try  v1  with  t2v1try  raise  v1  with  t2t2  v1t1t1try  t1  with  t2try  t1  with  t2(raise\;v_1)\;t_2\rightarrow raise\;v_1\\ v_1\;(raise\;v_2)\rightarrow raise\;v_2\\ \frac{t_1\rightarrow t_1'}{raise\;t_1\rightarrow raise\;t_1'}\\ raise\;(raise\;v_1)\rightarrow raise\;v_1\\ try\;v_1\;with\;t_2\rightarrow v_1\\ try\;raise\;v_1\;with\;t_2\rightarrow t_2\;v_1\\ \frac{t_1\rightarrow t_1'}{try\;t_1\;with\;t_2\rightarrow try\;t_1'\;with\;t_2}

  • 类型规则:

    Γt1:TexnΓraise  t1:TΓt1:TΓt2:TexnTΓtry  t1  with  t2:T\frac{\Gamma\vdash t_1:T_{exn}}{\Gamma\vdash raise\;t_1:T}\\ \frac{\Gamma\vdash t_1:T\quad\Gamma\vdash t_2:T_{exn}\rightarrow T}{\Gamma\vdash try\;t_1\;with\;t_2:T}

    其中,TexnT_{exn} 表示了可能出现的异常的种类。它可以是 Nat(对异常编码),或者 String 等。