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