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

3.2类型和项 3.2.1类型的语法 ·简单类型化)演算的类型表达式文法 o:=b null|unit|o+oo×oo-→o b:类型常量 nnll:初始类型 unit:终结类型 和、积与函数类型 类型表达式中不含类型变量 用入、入×，→和入+，×，来命名所讨论的演算

3.2 类型和项 3.2.1 类型的语法 • 简单类型化演算的类型表达式文法  ::= b | null | unit |  + |   |  → b：类型常量 null：初始类型 unit：终结类型 和、积与函数类型 类型表达式中不含类型变量 • 用→ 、 →和 +→来命名所讨论的演算

3.2类型和项 3.2.2上下文有关语法 不存在上下文无关文法，它正好产生)→良类 型的项 ·用一种基于逻辑的形式系统来定义类型语言 一用公理和推理规则来同时定义表达式及其类型 -定型公理C:无 推理规则 M1:61...Mk:Ok T1 M:01...Tk MKOK N:t T N:t 定型断言工 M:t,其中T=1:O,,xx:O}

3.2 类型和项 3.2.2 上下文有关语法 • 不存在上下文无关文法，它正好产生→良类 型的项 • 用一种基于逻辑的形式系统来定义类型语言 – 用公理和推理规则来同时定义表达式及其类型 – 定型公理 c : – 推理规则 – 定型断言  M : , 其中 = {x1 :1 , …, xk :k } M1 :1 … Mk :k N : 1 M1 :1 … k Mk :k  N :

3.2类型和项 3.2.3入→项的语法 ,一个入基调Σ=〈B,C)包含 一个集合B,其元素叫做基本类型或类型常量 形式为c:o的项常量集合C,其中σ是B上的入→类 型表达式 多类代数的基调Σ=S,F万)的基调很容易变换 成入基调Σ=〈B,C) -令B就等于S 若F有f:S1×.×Sk→S,则在C中包含项常量 f:S1→…Sk→S

3.2 类型和项 3.2.3 →项的语法 • 一个→基调 = B, C包含 – 一个集合B，其元素叫做基本类型或类型常量 – 形式为c的项常量集合C，其中是B上的→类 型表达式 • 多类代数的基调 = S, F 的基调很容易变换 成→基调 = B, C – 令B就等于S – 若F有f : s1  …  sk → s，则在C中包含项常量 f : s1 → … → sk → s

3.2类型和项 项的语法及类型按如下方式描述 -首先用BNF定义类型表达式的语法(3.2.1节) 然后用定型公理和定型规则同时定义Σ上的入→项 和它们的类型（良形的项就是良类型的项） 良形(wel-formed)和良类型(well-yped) 良形的项x+3在x是整型时才是良类型的 ·定型公理 C: 一X:O x:O

3.2 类型和项 • 项的语法及类型按如下方式描述 – 首先用BNF定义类型表达式的语法（3.2.1节） – 然后用定型公理和定型规则同时定义上的→项 和它们的类型（良形的项就是良类型的项） – 良形（well-formed）和良类型（well-typed） 良形的项x + 3在x是整型时才是良类型的 • 定型公理 –  c   (cst) – x   x   (var)

3.2类型和项 ·定型规则 M:o (add var) T,x:t M:o T,x:o M:t (>Intro） (入x:o.)：σ→E TM:o→TN:o (→Elim) T MN:t ·定型断言的证明叫做定型推导

3.2 类型和项 • 定型规则 (add var) (→ Intro) (→ Elim) • 定型断言的证明叫做定型推导  M : , x : M :  M : →  N :  MN : , x : M :  ( x : . M) :  →