+:nat×nal→nal和*：nal×nal→nal。描述基调的习惯写法如下： sorts nat fetns:0.1 nat +,*:1al×al→nal 在这种表示法中，通常把同样类型的函数符号写在同一行上。 口 定义基调的目的是用于写代数项，但还得考虑项中有变量的情况。假定有一个无穷的符 号集合V,其元素称为变量，并假定这些符号和所有常量符号、函数符号和类别符号都不一 样。变量未指定类型是没有意义的，因此还需要列出变量的类别。类别指派是变量与类别序 对的一个有限集合： 「={：S,,:Sk} 其中任何变量不会被指派多个类别。给定一个基调Σ=S,F)和类别指派T,∑和T上类别s 良形的代数项集合Terms(区，「)定义如下： (1)如果x:s∈「，那么x∈Terms(E,T): (2)如果∫：s1×.×sk→s并且M∈Trms(②，T)(t=1,,),那么fM…M ∈Terms(Σ，T)。 当k=0时，第二个子句应该解释成：如果f:s,那么fe Terms(区，T)。 例如，0∈Tmsa(Es),+01也是Terms"(Es)的项，因为+是Σv上的二元函数符号。 这两个项都不含变量，不含变量的项称为闭项。对任何类别指派T,+01总是Tms(E「) 的项。为了和PC℉一致，把0+1看成是+01的语法美化。如果只有一个类别，则总假定所 有的变量都属于这个类别，这时类别指派可以简化为列出所有的变量即可。下面用(M 表示出现在项M中的变量集合。 因为代数项中无约束变元，因此代换[Wx]M就是简单地把M中x的每个出现都用N代 替。很容易看出，如果项中的一个变量由适当类别的项代替的话，那么可以得到一个良形的 项，其类别和代换之前一样。这可由下面的引理精确地给出。下面用「，x:s表示类别指派 T.x:s=TUx:s 其中x在T中没有出现。 引理2.1如果M eTerms(E,T,x:s')并且N E Terms(E,T),那么[NIx]ME Terms(E,T)。 证明按Tems(区，「，x:s')中项的结构进行归纳。这是本章第一个归纳证明，因此叙述 得详细一些，以后的归纳证明仅给出要点。因为每个项都是变量、常量符号或者函数符号应 用到变元的形式，因此代数项上的归纳只有一种基本情况（变量）和一种归纳步骤（函数符 号)。对基本情况必须直接证明引理，而在归纳步骤中，假定引理对所有子项都成立。这个 假定叫做归纳假设。 对基本情况，考虑变量ye Terms(E,「，x:s)。如果y和x不同，那么[Nxy就是y。在 这种情况下肯定有y:s∈「，因此ye Terms(E,「)。如果项是变量x本身，那么[Nxx的结果 是项N。这时x一定有类别s,则N一定属于Terms(Σ，T)。这就证明了归纳的基本情况。 对于归纳步骤，假定[NWxM∈Trms(②，)(I≤i≤k),并且考察形式为fM.M的 项。在这个项中用N对x进行代换的结果可以写成fNx]MNx]M。因为已经假定fM 4∈Tems(②，「，x:s'),因此f必定有类型s1×.×sk→s。现在有[N/x]M,e Terms(②，T)(1≤ i≤k),因此f[N/x]M[N/xM∈Terms(区，T)。这就结束了该引理的归纳证明。读者应该检 验在归纳步骤中k=0的情况。 0 例2.2可以用基调∑：=S,F)来写自然数和栈表达式，其中S={nal,s1ack},F包含下列 函数符号。 sorts nat,stack fetns 0,1,2,...nat 33 : nat  nat  nat 和: nat  nat  nat。描述基调的习惯写法如下： sorts : nat fctns : 0, 1 : nat ,  : nat  nat  nat 在这种表示法中，通常把同样类型的函数符号写在同一行上。 ￾ 定义基调的目的是用于写代数项，但还得考虑项中有变量的情况。假定有一个无穷的符 号集合 V，其元素称为变量，并假定这些符号和所有常量符号、函数符号和类别符号都不一 样。变量未指定类型是没有意义的，因此还需要列出变量的类别。类别指派是变量与类别序 对的一个有限集合：   x1 : s1, …, xk : sk 其中任何变量不会被指派多个类别。给定一个基调  S，F和类别指派，和上类别 s 良形的代数项集合 Termss (, )定义如下： （1）如果 x : s  ，那么 x  Termss (, )； （2）如果 f : s1 …  sk  s 并且 Mi i s Terms (, ) (i  1, …, k)，那么 f M1 … Mk Termss (, )。 当 k  0 时，第二个子句应该解释成：如果 f : s，那么 f Termss (, )。 例如，0Termsnat(, )，01 也是 Termsnat(, )的项，因为是上的二元函数符号。 这两个项都不含变量，不含变量的项称为闭项。对任何类别指派，01 总是 Termsnat(, ) 的项。为了和 PCF 一致，把 01 看成是01 的语法美化。如果只有一个类别，则总假定所 有的变量都属于这个类别，这时类别指派可以简化为列出所有的变量即可。下面用 Var(M) 表示出现在项 M 中的变量集合。 因为代数项中无约束变元，因此代换NxM 就是简单地把 M 中 x 的每个出现都用 N 代 替。很容易看出，如果项中的一个变量由适当类别的项代替的话，那么可以得到一个良形的 项，其类别和代换之前一样。这可由下面的引理精确地给出。下面用, x : s表示类别指派 , x : s     x : s 其中 x 在中没有出现。 引理 2.1 如果 M Termss (, , x : s)并且 N  s Terms  (, )，那么NxMTermss (, )。 证明 按 Termss (, , x : s)中项的结构进行归纳。这是本章第一个归纳证明，因此叙述 得详细一些，以后的归纳证明仅给出要点。因为每个项都是变量、常量符号或者函数符号应 用到变元的形式，因此代数项上的归纳只有一种基本情况（变量）和一种归纳步骤（函数符 号）。对基本情况必须直接证明引理，而在归纳步骤中，假定引理对所有子项都成立。这个 假定叫做归纳假设。 对基本情况，考虑变量 yTermss (, , x : s)。如果 y 和 x 不同，那么Nx y 就是 y。在 这种情况下肯定有 y : s  ，因此 yTermss (, )。如果项是变量 x 本身，那么Nx x 的结果 是项 N。这时 x 一定有类别 s，则 N 一定属于 Termss (, )。这就证明了归纳的基本情况。 对于归纳步骤，假定NxMi  i s Terms (, )（1 i  k），并且考察形式为 f M1 … Mk的 项。在这个项中用 N 对 x 进行代换的结果可以写成 f NxM1…NxMk。因为已经假定 f M1… Mk Termss (, , x : s)，因此 f 必定有类型 s1 …  sk  s。现在有NxMi is Terms (, )（1 i  k），因此 f NxM1 …NxMkTermss (, )。这就结束了该引理的归纳证明。读者应该检 验在归纳步骤中 k = 0 的情况。 ￾ 例 2.2 可以用基调stk  S, F来写自然数和栈表达式，其中 S  nat, stack，F 包含下列 函数符号。 sorts : nat, stack fctns : 0, 1, 2, … : nat