3.2类型和项 2、和 T M:o InleftM:o+ (什Intro)1 I M:t T Inright,M:o+ (Intro)2 M:o+:卫N:g→pTP： (Elim) Case,PMNP:P
3.2 类型和项 2、和 (+ Intro)1 (+ Intro)2 (+ Elim) M : Inleft, M : + M : Inright, M: + M : + N : → P : → Case, , M N P :
3.2类型和项 初始类型和终结类型 与终结类型wnit有关的唯一的项 unit (unit Intro 终结类型也叫做单位类型 C语言的void类型就是单位类型，因为该类型的 表达式没有能够引起兴趣的值（而不是没有值） -与初始类型nml有关的项形式 Zero:nwll-→o (null Elim 若nwl类型有元素，函数Zero给出使用方式
3.2 类型和项 • 初始类型和终结类型 – 与终结类型unit有关的唯一的项 : unit (unit Intro) 终结类型也叫做单位类型 C语言的void类型就是单位类型，因为该类型的 表达式没有能够引起兴趣的值（而不是没有值） – 与初始类型null有关的项形式 Zero : null → (null Elim) 若null类型有元素， 函数Zero给出使用方式
3.2类型和项 ·有了单位类型与和类型后，b00类型可省略 -boo类型可以定义成 bool unit unit -true和fase可以定义成 true Inleft false Inright -if..then..else可以定义成 if M then Nelse P Casenit,nit,M(K N(Kp unit P) 其中KA,uit 入x:p.入y:unit.x
3.2 类型和项 • 有了单位类型与和类型后，bool类型可省略 – bool类型可以定义成 bool unit + unit – true和false可以定义成 true Inleft false Inright – if … then … else可以定义成 if M then N else P Caseunit, unit, M (K, unit N) (K, unit P) 其中K, unit x:.y:unit.x
3.2类型和项 ·多元函数和高阶函数之间的关系 入f:o×T→p.入x:o入y:fx,y〉 add 入p:nat×nat.Proj1p+(Proj2p） Curry(add)≡ (fnat×nat-→nat.入x:nat.入y:natf(x,Jy）add =入x:nat.入y:nat.add(x,Jy〉》 ≡入x:nat.入y:nat.(入p:nat×nat. (Proj p)+(Proj2 p))<x,y) =入x:at.y:nat.Projx,Jy〉+Proj2(x,y〉 =入x:nat.入y:natx+J
3.2 类型和项 • 多元函数和高阶函数之间的关系 – Curry, f : →.x:.y:.f x, y – add p:nat nat.(Proj1 p) + (Proj2 p) Curry(add) (f:nat nat → nat.x:nat.y:nat.f x, y) add = x:nat.y:nat.add x, y x:nat.y:nat.(p:nat nat. (Proj1 p) + (Proj2 p)) x, y = x:nat.y:nat.Proj1 x, y + Proj2 x, y = x:nat.y:nat.x + y
3.2类型和项 3.2.5定型算法 给定T,M,o,T M:σ是否为可证明的定型断 言 给定T,M,判定是否存在一个G,使得 M:o可证 基调Σ上入预备项 -M:=c|xMM|λx:o.M 该文法可以从定型公理和推理规则得到 类型检查的输入是符合该文法的预备项
3.2 类型和项 3.2.5 定型算法 – 给定, M, ， M:是否为可证明的定型断 言 – 给定，M，判定是否存在一个，使得 M:可证 • 基调上→预备项 – M ::= c | x | MM | x:.M – 该文法可以从定型公理和推理规则得到 – 类型检查的输入是符合该文法的预备项