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

3.2类型和项 类型检查算法 TCTT,c)=o 若c:o是该基调的一个常量 fail否则 TCT,x)=o 若x:o∈T 否则fail TCT,MN)= 若TCT,M)=o→t且TCT,)=o 否则fail TCT,入x:o.M)=o-→T 若TC(TA:G M,x:o,M)=T 否则fai讥

3.2 类型和项 • 类型检查算法 TC(, c) =  若 c:  是该基调的一个常量 fail 否则 TC(, x) =  若 x:   否则 fail TC(, MN) =  若TC(, M) =  →  且 TC(, N) =  否则 fail TC(, x:.M) =  →  若TC((x:.M , x:), M) =  否则 fail

3.2类型和项 命题3.5 算法TCT,M0终止且得到类型σ，当且仅当定型 断言TM:o是可推导的 若对于T和M,不存在可推导的定型断言，则算 法停机，报告失败

3.2 类型和项 • 命题3.5 – 算法TC(, M)终止且得到类型，当且仅当定型 断言 M:是可推导的 – 若对于和M，不存在可推导的定型断言，则算 法停机，报告失败

33证明系统 3.3.1等式和理论 等式 泛代数：M=NT,只有平凡的永真等式 类型化演算： M=N:x,有非平凡的永真 等式，和代数不同的是，等式包含类型，它用于 等式证明系统 代数系统中和类型有关的规则（作为副条件》 M=N[T,x:s]P=0[T] P,Q∈Ters∑，T [PIx]M=[Ox]N [T]

3.3 证明系统 3.3.1 等式和理论 • 等式 – 泛代数：M = N []，只有平凡的永真等式 – 类型化演算： M = N  ，有非平凡的永真 等式，和代数不同的是，等式包含类型，它用于 等式证明系统 – 代数系统中和类型有关的规则（作为副条件） P , Q Termss (, ) M = N , x : s P = Q  P/xM = Q/xN 

33证明系统 3.3.1等式和理论 等式 -泛代数：M=NT, 只有平凡的永真等式 类型化演算：r M=N:x,有非平凡的永真 等式，和代数不同的是，等式包含类型，它用于 等式证明系统 等式的另一种表示方式是 Vx:o1...xk:o M=N:t -若某个类型为空，则该等式无意义地成立

3.3 证明系统 3.3.1 等式和理论 • 等式 – 泛代数：M = N []，只有平凡的永真等式 – 类型化演算： M = N  ，有非平凡的永真 等式，和代数不同的是，等式包含类型，它用于 等式证明系统 – 等式的另一种表示方式是 x1 :1… xk :k .M = N – 若某个类型为空，则该等式无意义地成立

33证明系统 ·公理和推理规则 T M=N:o (add var) T,x:t M=N:o M=M:o M=N:o T N=M:o (sym) T M=N:o T N=P:o TM=P:σ (trans)

3.3 证明系统 • 公理和推理规则 (add var)  M = M : (ref) (sym) (trans)  M = N :  , x :  M = N :   M = N :   N = M :   M = N :   N = P :   M = P : 