+,*:1al×nal→nal empty:stack push:nal×stack→stack pop:sack→stack top:stack-→nalt push2(push1(push0emp))是该基调的项，在这个基调的标准解释中它表示有元素0,1 和2的栈。使用栈变量s:stack,表达式push1(push0s)定义把0和1压进s后的栈。口 2.2.3代数以及项在代数中的解释 确定了代数项的语法描述后，需要一种方式将代数项解释到相应代数上的元素。 代数是为代数项提供含义（指称语义）的数学结构。为了显式地表示从项到代数的映射， 需要先把基调的类别和函数符号映射到代数中。如果Σ是一个基调，那么代数A包含： (1)对每个s∈S,正好有一个载体A: (2)一个解释映射T把函数 I(f):A××A→ 指派给函数符号∫：S1×.×sk→s∈F,并且把T(f)eA指派给常量符号∫：s∈F。 如果Σ只有一个类别，那么称它为单类别(single-sorted)代数，否则为多类别(mamm-sorted, muli-sorted)代数。 如果A=〈{4xes,工)是一个Σ代数，并且∫是Σ的函数符号，为方便起见，通常把I) 写成。在函数符号是有限多或可数多的情况下，一般是列出所有的函数，像代数N和A 给出的那样。根据这两个约定，把Σ代数W写成 N=W0W,1N,+V,* 它给出了解释Σ上的项所需的全部信息，因为解释映射工己经由这个代数的函数命名方式给 出。 确定项M∈Trms(E,「)在Σ代数中的含义相对来说是简单的事情。可能唯一不太熟悉的 技术方法是对变量指派载体上的值。代数A的环境？是从变量集合到A的各载体集合的并集 的一个映射7：V→，。需要环境的原因是项M中可能含变量，在确定M的含义前必须 给变量一个值。当然，一个环境必须把每个变量映射到恰当载体上的值。如果对每个x:s∈ 「都有x)e4,就说环境n满足r。 为A给出一个满足T的环境n后，可以定义任何项M∈Trms(E,)在n下的含义AMn 如下（双括号[]在此用来表示求语法项的语义）： Ax]n=mx) A[Mn=f(A[M]n,...,A[Mn) 若∫：s是常量符号，则Af]n=f八。如果代数A在上下文中是清楚的，通常省略A而直 接写[M7。如果M是闭项，那么AM不依赖于7。此时可以省略环境，用AM表示M在 代数A中的含义。 例2.3例2.1的基调Σw有类别nal和函数符号0、1、+、*，可以把该基调上的项解释 到2.3.1节的Σv代数W上。 令是针对W的一个环境，x)=0心。x+1在n下的含义确定如下： x+1]n=+(,I川) =+(7x),1) =+N(0N,1N) =1W ◇ 例2.4例2.2的基调E=(S,F有类别nal与s1ack,有函数符号0、1、、+、*、empty、 44 ,  : nat  nat  nat empty : stack push : nat  stack  stack pop : stack  stack top : stack  nat push 2 (push 1 (push 0 empty) )是该基调的项，在这个基调的标准解释中它表示有元素 0，1 和 2 的栈。使用栈变量 s : stack，表达式 push 1 (push 0 s)定义把 0 和 1 压进 s 后的栈。 ￾ 2.2.3 代数以及项在代数中的解释 确定了代数项的语法描述后，需要一种方式将代数项解释到相应代数上的元素。 代数是为代数项提供含义（指称语义）的数学结构。为了显式地表示从项到代数的映射， 需要先把基调的类别和函数符号映射到代数中。如果是一个基调，那么代数包含： （1）对每个 s  S，正好有一个载体 As ； （2）一个解释映射把函数 (f ) : 1s A  …  k s A  As 指派给函数符号 f : s1  …  sk  s  F，并且把(f )As 指派给常量符号 f : s F。 如果只有一个类别，那么称它为单类别（single-sorted）代数，否则为多类别（many-sorted, multi-sorted）代数。 如果  As sS,  是一个代数，并且 f 是的函数符号，为方便起见，通常把 (f ) 写成 f 。在函数符号是有限多或可数多的情况下，一般是列出所有的函数，像代数和pcf 给出的那样。根据这两个约定，把代数 写成   , 0, 1, ,  它给出了解释上的项所需的全部信息，因为解释映射 已经由这个代数的函数命名方式给 出。 确定项 M  Termss (, )在代数中的含义相对来说是简单的事情。可能唯一不太熟悉的 技术方法是对变量指派载体上的值。代数的环境是从变量集合到的各载体集合的并集 的一个映射 : V  s As 。需要环境的原因是项 M 中可能含变量，在确定 M 的含义前必须 给变量一个值。当然，一个环境必须把每个变量映射到恰当载体上的值。如果对每个 x : s  都有(x)As ，就说环境 满足。 为 给出一个满足的环境后，可以定义任何项 M  Termss (, )在下的含义M 如下（双括号 在此用来表示求语法项的语义）： x  (x) M  f  (M1, …, Mk) 若 f : s 是常量符号，则f   f 。如果代数 在上下文中是清楚的，通常省略而直 接写M。如果 M 是闭项，那么M不依赖于。此时可以省略环境，用M表示 M 在 代数 中的含义。 例 2.3 例 2.1 的基调有类别 nat 和函数符号 0、1、、，可以把该基调上的项解释 到 2.3.1 节的 代数上。 令是针对 的一个环境，(x)  0。x  1 在下的含义确定如下： x  1   (x, 1)   ((x), 1 )   (0, 1 )  1 ￾ 例 2.4 例 2.2 的基调stkS, F有类别 nat 与 stack，有函数符号 0、1、…、、、empty