理论计算机科学电子笔记117（2005）249-261www.elsevier.com/locate/entcs向量空间概念的计算定义Pablo Arrighia和Gilles DowekbaInstitutGaspardMonge，5BdDescrtes，Champs-sur-Marne，77454Marne-la-Vall'eCedex2，法国arrighi@univ-mlv.frbEcolepolytech niqueanddINRIALIX，E'colepolytechnique，91128PalaiseuCedex，FranceGilles. polytechnique.frhttp://www.lix.polytechnique.fr/www.example.com摘要我们通常用一个集合来定义一个代数，在这个集合上定义的一些运算和一些代数必须验证的命题。 在某些情况下，我们可以用一个算法来代替这些命题，这个算法是在代数必须验证的这些运算的基础上构建的。 我们表明，这是向量空间和双线性函数的概念的情况。保留字：重写系统，向量空间，双线性函数，张量积证明两个向量相等的一种方法，二、x + y + 3。X和5。（x + y）+（−4）。y是将这些项转换为未知数的线性组合，并检查以这种方式获得的项是否相同。这种将表示向量的项转换为未知数的线性组合的算法也有助于表达量子计算编程语言的操作语义[1]，因为在这种语言中，程序及其输入值形成表示向量的项，其值，输出，是线性组合常数。更一般地，线性代数中使用的几种算法，例如矩阵乘法算法，将表示具有各种构造的向量的项变换为常数的线性组合。将表示向量的项变换为未知量的线性组合的算法在所有向量空间中都是有效的。本说明1571-0661 © 2005 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2004.06.013250P. Arrighi，G.Dowek/Electronic Notes in Theoretical Computer Science 117（2005）249|α是为了证明，而且它完全定义了向量空间的概念。向量空间概念的计算定义可以扩展到定义其他代数概念，如双线性。1算法和模型定义1.1（重写）设L是一阶语言，R是L上的重写系统。 我们说一个项t R-一步重写为一个项u当且仅当在项t中有一个出现α，在R中有一个重写规则l−→r，和一个替换σ使得t|α= σl和u = t [σr] α。定义1.2（关联-交换重写）设L是一个包含二元函数符号f1，...，fn和R是L上的重写系统。我们说，一项t R/AC（f1，...，fn）-一步重写到项u当且仅当存在项tJ，项tJ中出现Α，a在R中重写规则l−→r，并代入σ，使得tJ=ACt，tJ=σlu=ACTJ[σr]α。注1.3这个概念必须区别于R，AC-重写的概念，在R，AC-重写中，只有当项t具有与重写规则的左手侧的实例等价的子项AC-时，项t才重写为项u例如，对于规则x+x−→2.x，项t+（u+t）R/AC-重写为2.t+u，但是是R，AC-正规的。定义1.4（代数）设L是一阶语言。 一个L-代数是由一个集合M和一个函数f构成的族，对于L的每个n元符号f，从Mn到M。一个赋值φ的项t的符号φ（t）φ按通常定义。定义1.5（重写系统的模型）设L是一阶语言，R是重写系统根据语言L定义的算法。一个L-代数M是算法R的一个模型，或者算法R在模型M中有效，（M |= R），如果对于重写系统的所有重写规则l −→ r和赋值φ，<$l）φ=<$r）φ。例1.6考虑语言L由两个二进制符号+和×和由规则定义的算法R（x+y）×z−→（x×z）+（y×z）x×（y+z）−→（x×y）+（x×z）例如，将项（a+a）×a变换为项a×a+a×a。代数<${0， 1}，min，max<$<$是该算法的一个模型。注释1.7模型中算法有效性的定义扩展了编程语言语义的一些定义，其中语义P. Arrighi，G.Dowek/Electronic Notes in Theoretical Computer Science 117（2005）249251由集合M、将语言的值映射到M的元素的函数[ ]以及将n元程序映射到从Mn到M的函数来定义，使得程序P取值v1，...，vn作为输入产生值w作为输出当且仅当[w] = [P]（[v1]，.，[vn]）。事实上，让我们考虑一种编程语言，其中值的集合由一阶语言定义，其符号称为构造函数。考虑用函数符号p和可能的其他函数符号来扩展这种语言这种语言的程序P由扩展语言上的终止和连续重写系统给出，使得对于任意n个值v1，…， vn，程序P取值v1，...， 当且仅当项p（v1，...， vn）是w。然后，该重写系统的模型由集合M形成，对于ea ccon tru ct或cofari ym，从Mm到M的函数c，从Mn到M的函数p，以及可能的其他函数，使得对于重写系统的所有规则l −→ r和赋值φ，φl）φ= φr）φ。构造函数的表示定义了映射到M的元素的函数[ ]，函数p是函数[P]。 对于值v1 ， . 的 任 意 一 个 元 组 ， vn ， 如 果 项 p （ v1 ， ... ， vn ） 是 值 w ， n<$w ）=p<$（<$v1），. ，vn））和hus[w]=[P]（[v1]，. ，[vn]）。定义1.8（AC重写系统的模型）设L是包含二进制函数符号f1，.的一阶语言，fn，R是由AC（f1，...，fn）-根据语言L重写系统。 L-代数M是算法R（M）的模型|= R）如果• 对于R的所有重写规则l−→r和赋值φ，<$l）φ=<$r）φ，• 对于所有估值φ和指数i<$fi（x，fi（y，z）φ=<$fi（fi（x，y），z））φ<$fi（x，y））φ=<$fi（y，x））φ2向量空间2.1的算法设L是一个2-排序语言，其标量排序为K，向量排序为E，其中包含两个秩为<$K，K，K <$的二进制符号+和×，两个秩为<$K，K，K <$的常数0和1，一个二进制符号，也写作+，秩为<$E，E <$，一个二进制符号。秩为K，E，E，E是一个常数0，排序为E。为了将E类项转换为未知数的线性组合，我们需要求出向量252P. Arrighi，G.Dowek/Electronic Notes in Theoretical Computer Science 117（2005）249λ。（u + v）−→ λ。u+ λ。v但是标量和嵌套积λ。u+ µ。u−→（λ + µ）。uλ。（µ. u）−→（λ × µ）。u我们还需要一些琐碎的规则u+0−→u0的情况。u−→01 .一、u −→u最后，还有三条规则λ。0 −→0λ 。 u+ u −→ （ λ+1）。u u+ u −→（1 + 1）。u因为我们希望能够将因式分解规则应用于形式（3. x + 4。y）+2。x，上述重写系统中的约简必须以+的结合性和交换性为模来定义。这导致了以下定义。定义2.1（重写系统R）重写系统R是AC（+）-重写系统u+0−→u0的情况。u−→01 .一、u −→uλ。0 −→0λ。（µ. u）−→（λ.µ）。uλ。u+µ。u−→（λ + µ）。uλ。u+ u −→（λ+1）。uu+ u −→（1 + 1）。uP. Arrighi，G.Dowek/Electronic Notes in Theoretical Computer Science 117（2005）249253λ。（u + v）−→ λ。u+ λ。v254P. Arrighi，G.Dowek/Electronic Notes in Theoretical Computer Science 117（2005）249为了完整，我们还应该把场论的公理转换成重写系统，这是已知的困难。然而，有许多场，例如有理数场Q，其加法和乘法可以由终止和基连续重写系统表示。因此，我们将不考虑任意域上的任意向量空间。但是，我们考虑一个给定的域K，它由一个终止的和基连通的重写系统S定义，并专注于K-向量空间。定义2.2（标量重写系统）标量重写系统是一种至少包含符号+，×，0和1的语言重写系统，使得：• S是终止和接地电流，• 对于所有闭项λ、μ和ν，· 0+λ和λ，· 0×λ和0，· 1×λ和λ，·λ×（μ+ν）和（λ×μ）+（λ×ν），· （λ+μ）+ν和λ+（μ+ν），· λ+μ和μ+λ，· （λ×μ）×ν和λ×（μ×ν），· λ×µ和µ×λ具有相同的范式，• 0和1是正常项。命题2.3系统R终止。证据 考虑以下解释（与AC兼容）|= 2 +| u|+的|v|v||λ. u|= 1 + 2 |u||=零|= 0每次项t重写为项tJ，我们有|不|>>|TJ|.因此，系统终止。Q命题2.4对于任何标量重写系统S，系统RS终止。证据通过函数的定义||，如果项tS-简化为项tJ，则|不|为|TJ|.考虑一个（SR）-约化序列。在每个R-约化步骤，项的度量严格减小，并且在每个S-约化步骤，项的度量保持相同。因此，序列中只有有限个R-归约步骤，当S终止时，序列是有限的。QP. Arrighi，G.Dowek/Electronic Notes in Theoretical Computer Science 117（2005）249255定义2.5（重写系统S0）系统S0由规则构成0+λ−→λ0×λ−→01×λ−→λλ×（μ+ν）−→（λ×μ）+（λ×ν）其中+和×是AC符号。命题2.6重写系统RS0是一致的。证据当系统终止时，证明所有临界对是闭合的就足够了。这可以机械地检查，例如使用系统CIME1。Q定义2.7（包含）一个终止和继续关系S包含一个关系S0，如果每当t S0u，t和u有相同的S-范式。定义2.8（交换）关系R与关系RJ交换，如果每当tRu1和tRJu2时，存在项w使得u1RJw和u2Rw。命题2.9设R，S和S0是定义在一个集合上的三个关系，使得S是终止的且连续的，R∈S0是连续的，S包含S0，并且关系R与S的自反传递闭包S∈交换。则关系RS是连续的。证据我们把t的S-正规形式写成t↓。我们定义关系S↓bytS↓u，如果u是t的S-正规形;定义关系R;S↓ byt（R;S↓）u，如果存在项v使得tRvS↓u。首先注意，如果tRu，则t↓（R;S↓）u↓。如果t（RS）u，则t↓（R;S↓）<$u↓，如果t（R<$S0）<$u，则t↓（R;S↓）<$u↓。然后我们检查R;S↓是局部连续的。如果t（R;S↓）v1和t（R;S↓）v2，则存在项u1和u2，使得tRu1S↓v1和tRu2S↓v2。因此，相应地，R<$S0存在一项w，使得u1（R<$S0）<$w和u2（R<$S0）<$w。因此，u1↓（R;S↓）<$w↓和u2↓（R;S↓）<$w↓，即v1（R;S↓）<$w↓和v2（R;S↓）<$w↓。由于关系R;S↓是局部连续的和终止的，所以它是连续的。最后，如果我们有t（R<$S）<$u1和t（R<$S）<$u2，那么我们有t↓（R; S↓）<$u1↓和t↓（R; S↓）<$u2↓。因此，存在一项w，使得u1↓（R; S↓）<$w且u2↓（R;S↓）<$w。 因此，u1（RS）w和u2（RS）w。Q1 http://cime.lri.fr/256P. Arrighi，G.Dowek/Electronic Notes in Theoretical Computer Science 117（2005）249命题2.10设S是一个标量重写系统。重写系统RS在包含E类变量但不包含K类变量的项上是连续的。证据我们在半开项的集合上使用命题2.9，即有E类变量但没有K类变量的项。由于S是基连续的，并且终止于它是连续的，并且终止于半开项，S包含S0，因为S是标量重写系统，并且R与S可交换，因为0和1是正规项。Q注2.11半开项上的连续性意味着在语言的任何扩展中，对于向量（通常是基向量）具有常数的命题2.12设t是一个正规项，其变量在x1，...，xn.项t是0或形式为λ 1的项。xi1 +. + λk。xik + xik+1 +. + xik+1，其中索引i1，.，i，k+1是不同的，并且λ1，.，λk既不是0也不是1。证据项t是和u1+... +un不是和的正规项（如果t不是和，则取n= 1不是和的正规项是0、变量或λ形式的项。v.在这种情况下，λ既不是0也不是1，v既不是0，也不是两个向量的和，也不是标量与向量的乘积，因此它是一个变量。由于项t是正态的，如果n>1，则ui中没有一个是0。因此，术语t是0或以下形式的项λ1。xi1 +. + λk。xik + xik+1 +. +xik+l其中λ1，.， λk既不是0也不 是 1。 由于项t是正态的，i1，.，ik+l是不同的。Q2.2向量空间关于模型的概念，算法扮演着与公理集相同的角色：算法在模型中可能有效也可能无效，就像公理集在模型中可能有效也可能无效一样有效性的概念可以用来研究公理集，通常建立模型是证明某些命题不能从公理集证明的一种方式。但是有效性也可以用在另一个方向上：把代数类定义为某些理论的模型类。例如，给定一个域K=K，+，×，0， 1，K-向量空间类可以定义如下。定义2.13（向量空间）代数E，+，.，0是K向量P. Arrighi，G.Dowek/Electronic Notes in Theoretical Computer Science 117（2005）249257空间当且仅当代数<$K，+，×，0，1，E，+，..，0是2-排序公理uuu（u+0=u）u中国（1. u=u）λ（µ. u）=（λ.μ）。u）的λu= λ。u+ µ。u）的λ（u + v）= λ。u+ λ。五）我们现在证明，K-向量空间类可以定义为重写系统R的模型类。命题2.14设K =<$K，+，×，0，1 <$是一个场。 代数E，+，.， 0是K-向量空间当且仅当代数<$K，+，×，0，1，E，+，.， 0是重写系统R的模型。证据 我们首先检查R的所有规则在所有向量空间中都有效，即，（u+v）+w=u+（v+w）u+v=v+uu+0=u0的情况。u=01 .一、u=uλ。0=零λ。（µ. u）=（λ.μ）。uλ。u+ µ。u=（λ + μ）。uλ。u + u =（λ +1）。u u + u =（1+ 1）。uλ。（u + v）= λ。u+ λ。v是向量空间理论的定理。其中七个是向量空间理论的公理，即命题λ。u+ u =（λ + 1）。u和u + u=（1 + 1）。u是1的结果。u = u和λ。u + µ。u =（λ + μ）。联合让我们证明0。u=0。设uJ为使得u+uJ=258P. Arrighi，G.Dowek/Electronic Notes in Theoretical Computer Science 117（2005）2490的情况。然后是0。u = 0。u +0 = 0。u + u + uJ= 0。u + 1。u + uJ= 1。u+uJ=u+uJ=0 。 最 后 是 λ 。 0 = 0 是 0 的 结 果 。 u = 0 和 λ 。 （ µ. u ） =（λ.μ）。联合反过来，我们证明了向量空间的所有公理在R的所有模型中都成立。它们中的每一个的有效性都是重写规则有效性的结果，除了<$u<$uJ（u + uJ= 0）是u+（−1）的结果。u = 0本身是λ的结果。u + µ。u =（λ + μ）。U和0。u=0。Q2.3普遍性命题2.15设t和u是两项，其变量在x 1，...，x n.下列命题是等价的：(i) t和 u的标准形式是相同的模AC，(ii) 方程t=u在所有K-向量空间中成立，(iii) 以及当φ = e1/x1，.时t和u在Kn中的表示，en/xn，其中e1，.，en是Kn的标准基，是相同的。证据命题（i）蕴涵命题（ii），命题（ii）蕴涵命题（iii）。让我们证明命题（iii）蕴涵命题（i）。设t是一个正规项，其变量在x1，...，xn. t沿x1，...，xn是序列α1，...，如果有一个子项的形式为λ。xi在t中，则αi=λ，如果在t中存在形式为xi的子项，则αi= 1，否则αi= 0假设<$t）φ=<$u）φ。设e1，...，en是Kn的标准基，φ = e1/x1，.，n/xn.呼叫α1，...，αn在e1中的φt）φ的坐标，.，en.则t和u的正规形的分解都是α1，...，αn，因此它们模AC相同。Q3双线性3.1的算法定义3.1（重写系统RJ）考虑一种有四种类型的语言：K表示标量，E、F和G表示三个向量空间的向量，符号+、×、0、1表示标量，符号+、. 并且对于每个排序E、F和G为0，以及秩为E、F、G的符号。系统RJ是由系统R的规则和规则（u + v）<$w− →（u <$w）+（v<$w）（λ. u）v −→ λ。（uv）P. Arrighi，G.Dowek/Electronic Notes in Theoretical Computer Science 117（2005）249259u（v+w）−→（uv）+（uw）u（λ. v）−→ λ。（uv）0u −→ 0 u0−→ 0命题3.2重写系统RJ终止。证据 我们将定义2.3的解释扩展为：|=（3）|u|+ 2）（3）|v|+ 2）|+2)Q命题3.3对于任何标量重写系统S，系统RJ=S。证据 如命题2.4。Q命题3.4重写系统RjS0是一致的。证据在命题2.6的证明中，我们通过检查所有临界对闭合来证明局部连续性。Q命题3.5设S是一个标量重写系统。重写系统RjS在包含E、F和G类变量但不包含K类变量的项上是连续的。证据 使用命题2.9。Q命题3.6设t是一个正规项，其E类变量在x1，...，xn，其F类变量在y1，...，y p，并且它没有G和K类变量。 如果t的排序为E或F，则它具有相同的形式 如命题2.12。 如果它有排序G，那么它有以下形式λ1。（xi1 <$yj1）+... + λk。（xik yjk）+（xik+1 yjk+1）+. +（xik+ l <$yjk+l）其中，索引对i=1，j= 1，.，k+l，jk+l是不同的，并且λ1，.，λk既不是0也不是1。证据项t是和u1+... +un不是和的正规项（如果t不是和，则取n= 1不是和的正规项是0、形式为vw的项或形式为λ的项。v.在这种情况下，λ既不是0也不是1，v既不是0，也不是两个向量的和，也不是标量与向量的乘积，因此它的形式是vw。260P. Arrighi，G.Dowek/Electronic Notes in Theoretical Computer Science 117（2005）249在形式为vw的项中，v和w都不是和，不是标量与向量的乘积，也不是0。因此v和w都是变量。由于项t是正态的，如果n>1，则ui中没有一个是0。因此，项t要么是0，要么是形式为λ1的项。（xi1 <$yj1）+... + λk。（xik yjk）+（xik+1 yjk+1）+.+（xik+ lyjk+ l）其中λ1，.，λk既不是0也不是1。因为项t是正态的，所以指数对是不同的。Q3.2双线性定义3.7（双线性函数）设E、F和G是同一域上的三个一个从E×F到G的函数称为双线性的，如果（u+v）w=（uw）+（vw）（λ. u）λ v = λ。（uv）u（v+w）=（uv）+（uw）u（λ. v）= λ。（uv）命题3.8设K =<$K，+，×，0，1 <$是一个场。 这些结构是：0，F，+，.，0，G，+，.，0是K-向量空间，且n是从E × F到G的双线性函数当且仅当nK，+，×，0，1，E，+，.， 0，F，+，.， 0，G，+，.， 0，则Rj是系统Rj的模型。证据系统R的三个副本的规则的有效性表示，0，F，+，.，0，G，+，.，0是K-向量空间。其他六条规则的有效性等于定义3.7中公理的有效性加上作为这些公理的推论的两个额外命题0<$u=0和u<$0=0。Q3.3普遍性定义3.9（张量积）设E和F是两个向量空间，由向量空间G和从E×F到G的双线性函数构成的对是E和F的张量积，如果对E的所有基（ei）i∈I和F的所有基（eJj）j∈J，族（ei<$eJj）<$i，j<$i是G的基。例3.10设k是唯一的双线性函数，使得ei∈ eJj= eJJp（i−1）+j，其中e1，.，en是K n的标准基，eJ1，...，eJp是Kp的，并且eJ J1，...， eJJnp是Knp的。则Knp和Kp是Kn和Kp的张量积。P. Arrighi，G.Dowek/Electronic Notes in Theoretical Computer Science 117（2005）249261命题3.11设t和u是两个项，其E类变量在x 1，.，xn，其F类变量在y 1，...，y p，并且没有G和K类变量。下列命题是等价的：(i) t和 u的标准形式是相同的模AC，(ii) 方程t=u在由三个向量空间和双线性函数形成的所有结构中有效，(iii) 方程t=u在由两个向量空间和它们的张量积形成的所有结构中是有效的(iv) 以及Knp中t和 u的表示，φ = e1/x1，.，en/xn，eJ1/y1，.， 埃日普/伊普其中e1，.，e n是K n的标准基，e J1，...，eJp是Kp的值，是唯一的双线性函数，使得ei<$eJj=eJJp（i−1）+j，其中e JJ1，.，e JJnp是K np的标准基。证据命题（i）蕴涵命题（ii），命题（ii）蕴涵命题（iii），命题（iii）蕴涵命题（iv）。让我们证明命题（iv）蕴涵命题（i）。设t是G类正规项，其变量E类在x1，...， xn，y1，...，yp，并且没有G和K类变量。t沿x1，.， xn，y1，.，yp是序列α1，...， αnp使得如果存在形式为λ的子项。（xi<$yj）在t中，则αp（i−1）+j=λ，如果在t中存在形式为xi<$yj的子项，则αp（i−1）+j= 1，否则αp（i−1）+j= 0。假设<$t）φ=<$u）φ。呼叫α1，...，αnp是在eJJ1，.中的<$t）φ的坐标，eJJnp.则t和u的正规形的分解都是α1，...，αnp，因此它们模AC相同。Q结论我们通常用三个组成部分来定义一个代数：一个集合，在这个集合上定义的一些运算和一些在代数中必须有效的命题。例如，K-向量空间由集合E，运算0，+和定义。 和定义2.13的方程。我们可以用一种更面向计算的方式，通过一个集合、在这个集合上的运算和在这些运算上构造的项上的算法来定义一个代数，这些运算在代数中必须是有效的。例如，K-向量空间由集合E，运算0，+和定义。 和算法R.这个算法是线性代数中的一个著名算法：它是线性代数中的一个算法。262P. Arrighi，G.Dowek/Electronic Notes in Theoretical Computer Science 117（2005）249将任何线性表达式转换为未知数的线性组合的方法。这个算法，乍一看，只是线性代数中使用的众多算法之一，但它完全定义了向量空间的概念：向量空间是这个算法有效的任何代数，它是线性表达式可以这样转换为未知数的线性组合的任何代数。确认作者要感谢伊芙琳·孔特让、克劳德·基什内尔和克劳德·马尔切，感谢他们在他的论文的前一稿中所做的贡献。引用[1] P. Arrighi和G.张文龙，张量演算的操作语义，第二届国际量子程序设计语言研讨会，北京，2004。[2] N.德肖维茨和J. -李文，《计算机系统理论与应用》，清华大学出版社，2001年。[3] G.E.彼得森和法医张文，等，等.
