2.2代数、基调和项 ·代数A的环境n -m:V→xA 环境n满足Γ -如果对每个x:s∈T都有(x)EA ·M∈Ters2,T)的含义AMn是 -Ax7=7x) A M=A(A I M n...,A Mk n -若f:s是常量符号，则Af 刀=丹 若A清楚时，省略A而直接写成M 不依赖于n时，用AM表示M在A中的含义
2.2 代数、基调和项 • 代数A的环境 – : V → s As • 环境 满足 – 如果对每个x : s 都有(x)As • M Termss (, )的含义A M 是 – A x = (x) – A M = f A (A M1 , …, A Mk ) – 若f : s是常量符号，则A f = f A 若A清楚时，省略A而直接写成 M 不依赖于时，用A M 表示M在A中的含义
2.2代数、基调和项 ·例若7x)=0N x+1n=+N(x刀，1 =+N(7c),1N =+N(0N,1 =1N
2.2 代数、基调和项 • 例 若(x) = 0 N x + 1 = + N( x , 1 ) = + N ((x), 1 N) = + N (0 N , 1 N) = 1 N
2.2代数、基调和项 例Ak=〈N,N,0A,1A,,+A,*A,empty, pushA,.popA,t0pA》〉 empA=8,空序列 pushA(n,s)=n :s popA(n :s)=s p0pA(ε)=E top(n :s)n t0pA(ε)=0A 若n把x:nat映射到自然数3，把s:stack映射到2,1〉 pop(push x s)n popA(pushA(x n, 7)) =p0 DA(pusl4(3,〈2,1〉)) =p0pA(3,2,1)〉)
2.2 代数、基调和项 • 例 Astk = N, N , 0 A , 1 A , …, + A , A , emptyA , pushA , pop A , top A emptyA = , 空序列 pushA(n, s) = n :: s popA(n :: s) = s popA( ) = topA(n :: s) = n topA( ) = 0 A 若把x:nat映射到自然数3，把s:stack映射到2, 1 pop(push x s) = popA(pushA( x , s ) ) = popA(pushA(3, 2, 1 ) ) = popA( 3, 2, 1 ) = 2, 1
2.2代数、基调和项 ·引理2.2 令A是Σ代数，M∈Ters∑，T),并且是满足T 的环境，那么Mn∈As 证明根据Ters2,)中项的结构进行归纳 引理2.3 令x1,,x是由出现在M∈Ters②，T)中的所有 变量构成的变量表，刀，和2是满足T的两个环境，并 且对i1,,k有n1(x)=72c,那么M刀1= Mm 证明基于项结构的归纳
2.2 代数、基调和项 • 引理2.2 令A是代数，MTermss (, )，并且是满足 的环境，那么 M As 证明 根据Termss (, )中项的结构进行归纳 • 引理2.3 令x1 , …, xk是由出现在MTermss (, )中的所有 变量构成的变量表，1和2是满足的两个环境, 并 且对i=1, …, k有 1 (xi ) =2 (xi ), 那么 M 1 = M 2 证明 基于项结构的归纳
2.2代数、基调和项 2.2.4代换引理 。引理2.4 令M∈Terms∑，T,x:s')并且N∈Terms(2,T),那 么[N/x]Me Terms②，)。并且对任何环境，有 [N/x]M n=M (7x-→a]), 其中a=Nm,它是N在n下的含 义 证明 根据项M的结构进行归纳
2.2 代数、基调和项 2.2.4 代换引理 • 引理2.4 令MTermss (, , x:s)并且N Termss (, )，那 么NxMTermss (, )。并且对任何环境，有 NxM = M (x a)， 其中a = N ，它是N在下的含 义 证明 根据项M的结构进行归纳