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 :