中国科学技术大学：《程序设计语言理论》课程教学资源（PPT课件讲稿）第3章 简单类型化λ演算

3.2类型和项 例 V:O (入x:Oxy:O 是一个需要用到所有这些定型规则的项 从定型公理x:ox:o开始 根据(-→Intro)规则，得到⑦ 入x:0X:可→O -再由（add var),得到y:o 入x:GX:可→o 由公理y:o v:o 最后，由（→Elim)规则可知y:o (Ax:o.x)y:o 是良类型的

3.2 类型和项 • 例 y: (x:.x)y: 是一个需要用到所有这些定型规则的项 –从定型公理x: x:开始 –根据(→ Intro) 规则，得到 x:. x :  →  –再由（add var），得到y:  x:. x :  →  –由公理y: y: –最后，由(→ Elim)规则可知 y: (x:. x)y: 是良类型的

3.2类型和项 。引理3.1 如果r M:o,那么M中的每个自由变量都出现在 T中 。引理3.2 -如果TM:o, 且T⌒T'包含M中所有的自由变量 ,那么T'Mo 引理3.3 如果TM:o, 并且y不出现在T中，那么[yx yix M:o

3.2 类型和项 • 引理3.1 – 如果 M:，那么M中的每个自由变量都出现在 中 • 引理3.2 – 如果 M:，且包含M中所有的自由变量 ，那么 M: • 引理3.3 – 如果 M:，并且y不出现在中，那么[y/x] [y/x]M:

3.2类型和项 ·引理3.4 如果T1,x:o M:x和T2N:o都是入→项，且 TUT,是良形的类型指派，那么代换实例TUT2 [NxM:是良形项 一证明 基于对定型断言T1,x:o M:x的证明的归纳

3.2 类型和项 • 引理3.4 – 如果1 ,x: M:和2 N:都是 →项，且 12是良形的类型指派，那么代换实例12 [N/x]M:是良形项 – 证明 基于对定型断言1，x: M: 的证明的归纳

3.2类型和项 3.2.4有积与和及相关类型的项 1、笛卡儿积（把入扩展到入×，→） T M:o T N:t T (M,WW:o× (×Intro) M:ox t (x Elim) I M:ox t (×Elim)

3.2 类型和项 3.2.4 有积与和及相关类型的项 1、笛卡儿积（把→扩展到 , →） ( Intro) ( Elim)1 ( Elim)2  M :   N :   M, N :     M :     Proj1 ,  M:   M :     Proj2 ,  M: 

3.2类型和项 积的另一种表示 -对所有的类型σ和，存在项常量 Pair,r:g→t→(oX Proj1o,r:(oX)→o Proj2ot:(oX)→t 〈M,Nar看成Pair,rMN的语法美化 -两种表示的主要区别 第二种表示：Pair、Proj,和Proj2都是项 第一种表示：入x:o.入y:t.Pair x y、x:o×x.Projx 和入x:o×x.Proj2x才是良形的项

3.2 类型和项 • 积的另一种表示 – 对所有的类型和，存在项常量 Pair,  :  →  → ( ) Proj1 ,  : ( ) →  Proj2 ,  : ( ) →  – M, N ,  看成Pair,  M N的语法美化 – 两种表示的主要区别 第二种表示：Pair、Proj1和Proj2都是项 第一种表示：x:.y:.Pair x y、x: .Proj1 x 和x: .Proj2 x 才是良形的项