偏微分方程的逻辑规则及完备性的研究

可在www.sciencedirect.com在线获取理论计算机科学电子笔记352（2020）211-232www.elsevier.com/locate/entcs偏微分方程的完全公理化戈登·D Plotkin1Google Research山景城，美国摘要我们正式的部分diffierentiation在一个版本的方程逻辑与函数变量和绑定结构的著名规则。我们证明了所得到的理论关于多项式解释是完备的。证明利用塞维里我们还提出了一些相关的结果，如可判定性和方程的完整性。关键词：偏微分，二阶方程逻辑，完备性，Hermite插值1介绍最近，人们对微分结构的范畴公理化越来越感兴趣例如，对于前向定向，参见[2];对于反向定向，参见[4];对于切线结构，参见[3]。一个自然的问题是公理是否被很好地选择。作者通常表明它们在自然结构中保持不变例如，在carbohydia dia范畴的情况下，它们对实数和光滑函数的有限幂范畴成立。所以这些公理在这个意义上是正确的。但是人们还可以问，它们是否完备，或者在什么意义上完备，即是否有缺失的公理。在这里，我们对一个相关的基本逻辑问题感兴趣，我们希望它能帮助我们解决分类问题：操作偏导数的标准规则是完备的吗？这些规则确实是众所周知的：乘积和和的导数由简单的公式给出，包括它们的直接子表达式和它们的偏导数;实常数和实变量的导数是0或1;链式规则负责函数的应用;关于不同变量的偏导数可交换。他们肯定是完整的。1电子邮件：plotkin@google.comhttps://doi.org/10.1016/j.entcs.2020.09.0111571-0661/© 2020作者。出版社：Elsevier B.V.这是一篇基于CC BY-NC-ND许可证的开放获取文章（http://creativecommons.org/licenses/by-nc-nd/4.0/）。212G.D. Plotkin/电子笔记在理论计算机科学352（2020）211为了证明这一点，我们首先使用一种合适的等式逻辑形式化部分微分的标准规则。我们的公理系统由环公理、实数加法乘法表和四个偏微分公理组成。由于部分微分涉及变量绑定，我们超出了标准等式逻辑的范围。所以我们使用一个扩展版本，它允许绑定构造并使用函数变量。这类等式逻辑称为二阶等式逻辑，由菲奥雷、胡尔和马哈茂德提出[6，7]。我们采用了他们的逻辑的一个次要的，虽然完全相同的变体。由此产生的部分微分理论自然是用光滑函数来解释的，但是，为了完整起见，它只能用多项式函数。事实上，即使函数变量的解释仅限于自然数多项式函数，并且变量的解释仅限于自然数，该理论也是完整的。如果常数被限制为有理数或0和1（等价于整数），情况仍然如此。为了建立完备性，我们采用了一个插值定理，一个著名的塞维里定理[12]关于埃尔米特插值问题的可解性Hermite插值是Lagrange插值的推广。Lagrange插值是求在指定点取指定值的实多项式，这对多元Lagrange插值有明显的推广。在多变量埃尔米特插值中，人们还规定了（可能更高阶）偏导数的值定理5.4建立了相对于函数变量的自然数多项式解释和变量的自然数解释的完备性(The多项式是实多项式的适应，解决了合适的Hermite插值问题。）我们也给出了一些其他的结果。定理5.5用标准型之间的等价关系刻画了我们方程理论的定理.定理5.8表明等价关系成立，当且仅当它可以只用一个部分可导性公理来建立，即两个变量的部分可导性的顺序无关紧要（当不需要部分可导性公理时，用规范型的稍微更精细的概念可以消除这个公理）。定理5.9表明，该理论不仅在实数上的标准解释方面是完备的，而且它也是方程完备的（也称为希尔伯特-波斯特完备），也就是说，它没有方程相容的真扩张，见[14]。如果常数仅限于有理数，情况仍然如此，但如果它们仅限于整数，情况就不同了。定理5.10表明，其中常数仅限于有理数的子理论是可判定的，而且，在一个方程不成立的情况下，可以找到它的一个反例。一个重要的遗留问题是判定问题的复杂性。G.D. Plotkin/电子笔记在理论计算机科学352（2020）211213. 1阿克斯阿吉耶x=e1x=xx n−1. 100万n−1100万（虽然更自然，但该表达式掩盖了变量x的作用）。我们写为∂......这是什么？你好2偏微分我们假设不相交的变量集，范围为x，y，z，...。. . ，以及函数变量，范围为f，g，h，. . . 每个函数变量都有一个给定的元数n≥0，记为f：n。假设变量的集合是可数的，每个arity的函数变量的集合也是可数的。表达式具有以下形式：e：：= r（r∈R）|X|e0+ e1|e0e1|f（e0，.， en−1）（f：n）|PDi（x.e0，e1）表达式PDi（x.e0，e1）被读作e 0相对于下式的偏导数：x，在e1处评估。在这个表达式中，变量x对e0有约束力，但对e没有约束力。下面，我们使用更熟悉，更自然的表达方式“0”。ne为。 ，并注意到x的最后一次出现是自由的;我们写e自由变量和α-等价像通常一样定义，并且，像通常一样，我们识别α-等价表达式。我们写FV（e）表示表达式e的自由变量集，FnV（e）表示它的函数变量集。每个表达式e都有一个大小|e|以一种明显的方式定义。同时替代e [eJ0/x0， . ，eJn−1/xn−1]变量表达式的定义可以预期，其中PDi（x.e0，e1）的子句及其绑定变量为：PDi ∈（x，e0，e1）[eJ0/x0， . ，eJn−1/xn−1]=PDi（x.e0[eJ0/x0， . ，EJn-1/xn-1]，e1[EJ0/x0， . ，eJn−1/xn−1]）其中x∈/FV（EJ0）<$. . . F V（eJn−1）. 也有抽象行为替代的概念（x0，.，xn−1）.eJ为函数变量。对于f：n，我们定义e [（x0，.，xn−1）.eJ/f]通过对e的结构归纳如下：r [（x0，.， xn−1）.eJ/f]= rx [（x0，.，x n − 1）. e j/f]= x（e0 + e1）[（x0，.， xn−1）.eJ/f] =e0 [（x0，.， xn−1）.eJ/f]+ e1[（x0，.， xn−1）.eJ/f]（e0e1）[（x0，...， xn−1）.eJ/f]=e0 [（x0，.， xn−1）.eJ/f] e1 [（x0，.，xn−1）.eJ/f]阿克斯214G.D. Plotkin/电子笔记在理论计算机科学352（2020）211−..[e0[（x0， . ，xn−1）.eJ/f]/x0， . ，en−1[（x0， .. . ，xn−1）.eJ/f]/xn−1]⎪g（e0，.，en−1）[（x0，...，xn−1）.eJ/f]=（g =f）g（e0[（x0，.，xn−1）.eJ/f]，.，en−1 [（x0，.， xn−1）.eJ/f]）PDi（x. e0，e1）[（x0， . ，xn1）.eJ/f]（g/=f）= PDi（x. e0 [（x0，.，xn−1）.eJ/f]，e1 [（x0，.，xn−1）.eJ/f]）（x∈/F V（eJ）\{x0， . ，xn−1}）还有一种更一般的、定义类似的同时替换几个摘要的方法：e [（x11，. ，x1n1）.eJ1/f1， . ，（xk1， . ，xknk）.eJk/fk]其中fi：ni，对于i= 1，k.偏微分理论的公理包括交换环的公理、实常数的加法和乘法表以及四个偏微分公理。这四个公理是加法和乘法微分的通常规则，二元函数的链式规则，以及关于不同变量的部分微分的可交换性。x+y= 1个阿克斯阿龙=y阿克斯n（g0（x），g1（x））n（x0，g1（x））=（x）n =0（x）n = 0（x）n+1（x）x.x0=g0（x）<$x1号线.x1=g1（x）<$x∂ ∂f（x，y）=∂ ∂f（x，y）∂y ∂x ∂x ∂y偏微分理论的定理是通过在等式、同余和两种替换的明显规则下封闭公理而得到的，遵循等式系统的通常模式。特别地，部分微分的全等规则如下：e0=e1eJ0=eJ1PDi（x. e0，eJ0）= PDi（x. e1，EJ1）如果方程e0 = e1在这个理论中成立，我们写► e0=e1接下来，我们建立了一些公理的预期结果，包括G.D. Plotkin/电子笔记在理论计算机科学352（2020）211215I=m链式法则的一般形式。 我们使用一个明显的缩写词nei，有限和表达式。216G.D. Plotkin/电子笔记在理论计算机科学352（2020）211n−1阿克斯.阿克斯引理2.1下列方程在偏微分理论中是可证明的：（一）（二）阿克斯阿克斯f（x）+g（x）= 1个f（x）g（x）（三）其他事项阿克斯f（x）g（x）=+阿克斯f（x）阿克斯g（x）（四）阿克斯（x），...，gn−1（x））阿克斯=g（x）阿克斯+f（x）阿克斯n（x），n（x），gi−1（x），xi，gi+1（x），.， gn−1（x））。第一（十）条（五）=i=0阿斯克斯岛埃莱.xi=gi（x）<$x证据n=0（x∈FV（e））(i) 这是由加法公理得出的，用0代替y。(ii) 这是由加法公理和二进制链式法则得出的。(iii) 这是由乘法公理和二进制链式法则得出的。(iv) 首先，注意，在乘法公理中用0代替y，我们得到0= 0。 接下来，对于链式规则中n = 0的情况，替换为（x0，x1）。对于f和（z），h（）。在二元链式法则中，对于g0和g1都是0，以得到以下可证明的方程：阿夫赫阿克斯（）00x0=0G.D. Plotkin/电子笔记在理论计算机科学352（2020）211217.阿克斯.阿克斯.阿克斯.阿克斯+h（）1100x1=0100 x（）0=零x0=0阿夫赫1号线0x1=0接下来，将一元链式法则替换为（x0，x1）。h（x0）对于f和（z）。0为g1在二元链规则中得到以下可证明的方程：h（g0（x0））阿克斯=0.00000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000=0.00000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000x0=g0（x）x0=g0（x）0（x）阿克斯0（x）阿克斯0+.218G.D. Plotkin/电子笔记在理论计算机科学352（2020）211.阿克斯+单位h（x0）1100x1=0100 x最后，当n≥2时，我们用归纳法进行公理提供了基础假设n为归纳假设，我们证明了n+ 1。次G.D. Plotkin/电子笔记在理论计算机科学352（2020）211219阿克斯. =. +. =. +..n01Σ.阿克斯阿克斯x′=xX′00x0（x′0）X′0n（x′1）191用（z）.z代替二进制链式规则中的g0和g1，并使用x= 1，我们得到以下等式：n（x，x）n（x，J，0）n（x，xJ1）x.x′0=xJ1.x′1=x然后代入（x，y）。h（g0（x），g1（y），.，gn（y））对于f，我们得到：（x），g1（x），.， gn（x））h（g0（xJ0），g1（x），.， gn（x））x.x′0=x对于这两个求和项中的第一个，我们有：J1.x′1=xn（g0（x′0），g1（x），.，gn（x））=h（g0（x′0），g1（x），.，gn（x））[x/xJ]0。.Σ=x0=g0（x′）[x/xJ0]（x，g（x），.）g（x））=00（x）0.0000。x0=g0（x）<$x其中第二个等式是一元链式规则的应用，另外两个等式是句法恒等式（第二个直到α-等价）。对于其中的第二个，利用归纳假设（n元链规则），我们有：n（g0（x），g1（x′1），.，gn（x′1））=h（g0（x），g1（x′1），.，gn（x′1））[x/xJ]阿克斯.=x′1=x1991年.Σxi=gi（x′）[x/xJ1]- 是的n=1=1（x），g1（x），.，gi−1（x），xi，gi+1（x），.，gn（x））阿斯克斯岛.xi=gi（x）第一（十）条阿克斯结合结果，我们得出了预期的结论。(v) 当n = 0时，链式法则是<$f（）= 0，其中f：0。 将（）.e替换为f，得到εe=0asx∈/FV（e）。Q了解差异化和替代之间的相互作用将被证明是有用的：..（g0（x），g1（xJ1）， . ，gn（xJ1））X′01（x，x ，x，x）gn（x））100万ni=1n（g0（x），g1（x′1），.，gi−1（x′1），xi，gi+1（x′1），.，gn（x′1））阿斯克斯岛11220G.D. Plotkin/电子笔记在理论计算机科学352（2020）211引理2.2下列等式等价：(i) 一般链式法则。(ii) 下面的替换原理，对于所有表达式e和e 0，.， n−1G.D. Plotkin/电子笔记在理论计算机科学352（2020）211221Σn−1阿克斯00n−1阿克斯.=阿克斯阿克斯0i=0阿斯克斯岛xi=ei阿克斯xi=ei（当f∈/Fn V（ei），对于i=0， . ，n−1）i=0阿斯克斯岛i=0阿斯克斯岛（当f∈/Fn V（e0， . . . ，ei−1，ei+1， . ，en−1））i=0阿斯克斯岛阿克斯i=0阿斯克斯岛阿克斯i=0 阿斯克斯岛阿克斯我们有：► [e0/x0， .] ，en−1/xn−1]n−1=埃莱[e/x，.，e/x[英语泛读材料i=0当rex0， . ，xn−1是不同的变量使得x∈/F V（e）\{x0， . ，xn−1}。证据在一个方向上，假设一般链式法则。选择f：n不在任何FnV（ei）中。使用一般的链式法则，我们有：n（e0，.，en−1）f（e0，.，ei−1，xi，ei+1，.，en−1）。i=0阿斯克斯岛埃雷岛阿克斯然后，代入（x0，...，xn−1）.e对于左边的f，我们有以下恒等式（回想一下，我们识别了α-等价表达式）：n（e0，.，en−1）[（x， . . . ， X）的。 e/f]=f（e0，...，en−1）[（x0，...，xn−1）。 e/f]（as x∈/F V（e）\{x， . ， x}）100万n−1阿克斯=e[e0/x0，.，en−1/xn−1]0（如f∈/Fn V（e， . ，en−1））接下来，在右边代入，我们得到恒等式：.n−1ei−1，xi，ei+1，...，en−1）。eixn−1）。英/法]=n−1。n（e0，.，ei−1，xi，ei+1，...，en−1）。[（x0，.，xn−1）。e/f]阿罗夫伊=n−1。n（e0，.，ei−1，xi，ei+1，...，en−1）[（x0，...，xn−1）。 e/f]。埃莱岛阿克斯（如xi∈/FV（e）\{x0， . ，xn−1}）=n−1e[e0/x0，...，ei−1/xi−1，xi/xi，ei+1/xi+1，.，en−1/xn−1]。埃雷岛阿克斯=n−1e[e0/x0，...，ei−1/xi−1，ei+1/xi+1，.，en−1/xn−1]。埃雷岛阿斯克斯岛n−1►xi=ein−1xi=eixi=eixi=ei222G.D. Plotkin/电子笔记在理论计算机科学352（2020）211n−1阿斯克斯岛阿克斯00阿克斯=n−1e[e0/x0， . ，en−1/xn−1]结论如下。在另一个方向上，假设替换原理，取e为f（x0， .. . ，xn−1）（whenFV（e）\{x0， . ，xn-1}=n），并且对于i=0， n-1，将ei定义为bgi（x），以获得：► （x），...，gn−1（x））=f（x0，.，xn−1）[g （x）/x，.，Gi=0（x）/x[i（x）n−1n−1G.D. Plotkin/电子笔记在理论计算机科学352（2020）211223.（x），...，gi−1（x），xi，gi+1（x），.， gn−1（x））作为n（x0，.， xn−1）[g（x）/x 、...、G（x）/x ]和阿斯克斯岛0 0n−1n−1阿斯克斯岛.xi=gi（x）是α等价的，我们就完成了。Q一个（实）多项式（通常）是一个不包含函数变量或部分微分的表达式;如果它的所有常数都是自然数，则它是一个自然数多项式。我们写P（x0，.，xn−1）来表示P是一个实多项式，其（必然自由的）变量包含在{x0，.，xn−1};对于表达式e0，...，en-1， 我们可以写P（e0，...，en−1）为 P [e0/x0，.，en−1/xn−1]。我们写PPJ是指多项式P和PJ模交换环的轴和实常数的加法和乘法表是相等的。我们注意到，我们的等式系统是二阶约束等式逻辑的一个实例该逻辑具有形式为（b0，.， bn−1; m）（bi，m ≥ 0）. 这些被用来从n个抽象中形成一个复合表达式，分别为b0，...，bn-1，和m表达式。有了这个符号，+ 有arity（; 2），PDi有arity（1; 1）。这个系统是单排序的;有一个自然的推广到多排序的版本。在[6]中，Fiore和Hur给出了一个多排序的二阶方程逻辑，在[7]中，Fiore和Mahmoud考虑了单排序的情况。他们的系统和我们的系统之间的差异是不重要的：我们称之为“函数变量”，他们称之为“元变量”;而我们的函数变量带有预先分配的arity，他们没有，他们宁愿利用合适的环境;他们的arity具有更简单的形式（b 0，...，bn-1），但它们的通用性并不差，因为额外的参数变成了0元抽象;虽然我们有函数变量的替换操作和上下文规则，但它们采用了一个等价的规则。其等价规则的一个替换版本是：e0=e1e0 [（x0，.， xn−1）.eJ/f]=e1 [（x0，.， xn−1）.eJ/f]他们采用了这个规则的同时替换版本，在任何情况下，它都等同于单一替换规则。回到我们的二阶方程逻辑的单排序版本，我们说，如果x=y是一个定理（其中x，y不同），我们说一个方程理论是方程完备的，如果它的任何扩展由一个单一的非定理是方程不一致的。请注意，这是一个语法标准，独立于任何特定的模型。多项式提供了方程完备性的一个例子，尽管它没有约束算子。这个理论是交换环的常数为所有实数和加法和乘法表（即，我们的理论少部分的偏差）。证明的思想是不同的多项式有不同的值224G.D. Plotkin/电子笔记在理论计算机科学352（2020）211为它们的变量选择合适的值。这可以在逻辑中形式化，因此，给定不同多项式之间的方程，可以证明两个不同的实数相等，这反过来又使人们能够证明x=y。λβη-演算提供了一个具有绑定算子的部分例子。 可以形式化为二阶理论，具有二元应用算子ap：（; 2）和一元lambda抽象算子λ：（1;0），以及两个方程ap（λ（（x）.f（x）），y）= f（y）λ（（y）. ap（x，y））= x虽然在等式上不完全，但在某种意义上是部分完全的，即根据Büohm定理[ 1 ]，没有两个不同的Beta-Bernoulli过程的理论[13]也有约束算子;它是用一个方程逻辑来表述的，这个逻辑与我们的逻辑有点不同，以适应代数效应。这个理论几乎是方程完备的，因为它只有一个相容的延拓。在这种扩展中，所有关于概率的定量信息都丢失了，因此可以排除掉。3语义我们给出了我们用光滑函数h：Rn→R表示的偏微分表达式的一个语义.环境ρ是一个从变量到实数的函数;函数环境ρ是一个从函数变量到光滑函数的函数，它将n元的函数变量发送到Rn上的光滑函数。我们写ρ[r0/x0， . ，rn−1/xn−1]对于enn nt，其中valueri在xi上（对于i=0，n−1），valueeρ（x）在ny个其他变量x上;函数e nnttsn[h0/f0， . ，hn−1/fn−1]，其中hi是m元的，如果fi：m，定义类似。我们将0写为恒定为0的环境和产生恒定为0的函数的函数环境我们通过以下子句定义表达式相对于函数环境和环境的表示S[[e]] expS[[r]] ρS[[x]] ρ==Rρ（x）S[[e+eJ]] ρ=S[[e]] ρ+S[[eJ]] ρS[[eeJ]] ρ=S[[e]] ρ×S[[eJ]] ρS[[f（e0， . ，en−1）]]ρ=（f）（S[[e0]] ，S[[en−1]]<$ρ）S [[PDi]（x. e，eJ）]]=D（r∈R <$→S[[e]]<$ρ[r/x]）（S[[eJ]]<$ρ）初步看来，这个定义可能是不恰当的，因为最后一个子句依赖于函数r∈R<$→S[[e]]<$ρ[r/x]是可导的。然而，人们通过结构归纳法证明了这个定义是正确的，而且 ， 对 于 任 何 变 量 x0 ， .. . . . .， xn−1 函 数 发 送 r0 ， .， rn−1∈RtoS[[e]]<$ρ[r0/x0， . ，rn−1/xn−1]是光滑的。G.D. Plotkin/电子笔记在理论计算机科学352（2020）211225一个表达式的符号S[[e]] ρ只取决于由赋予它的自由函数变量的值，以及由ρ赋予它的自由变量的值。当e没有函数变量时，我们只写S[[e]]ρ作为它的表示，省略，当它是封闭的（没有任何类型的自由变量）时，我们只写S[[e]。像往常一样，我们写|= e0 = e1 to mean that e0 and e1 have the same denotation, given any function环境和任何环境。我们省略了以下标准替换引理的证明：引理3.1（i）变量代换和表示交换，即我们有：S[[e[e0/x0， . ，en−1/xn−1]<$ρ=S[[e]]<$ρ[S[[e0]]<$ρ/x0， . ，S[[en−1]]<$ρ/xn−1](ii) 函数变量代换和表示交换，即我们有：S [[e [（x0，.，xn−1）.eJ/f] ρ为S[[e]][u0， . ，un−1<$→S[[eJ]]<$ρ [u0/x0， . ，un−1/xn−1]/f]ρ使用这个引理，可以直接证明一致性：定理3.2（一致性）对于任何表达式e0和e1，我们有：►e0= e1=|= e0= e1任何多项式P（x0，.， xn−1）定义实数上的n元多项式函数，也写作P（x0，...，xn−1）。注意P（r0， . ，rn−1）=S[[P]]0[r0/x0， . ，rn−1/xn−1]我们还记得P（x0，...，xn−1）<$PJ（x0，.， xn−1）当且仅当两个函数P（x0，.，xn−1）和PJ（x0，...，n-1）相等。我们说一个函数环境是一个（自然数）多项式环境，如果它的所有值都是（自然数）多项式函数，并且一个环境是一个自然数环境，如果它的所有值都是自然数。我们写|= Ne0 = e1意味着给定任何自然数多项式函数环境和任何自然数环境，e0和e1我们的语义的理论部分diffierentiation采用了一个具体的概念的功能，即光滑的功能，在实数。对于二阶逻辑的一般理论，需要一个更抽象的，因而也更一般的函数概念这可以用抽象克隆[5]，Lawvere理论，或者更概念化的，在上下文的前层范畴中的幺半群来表达，见[8，6，7]。226G.D. Plotkin/电子笔记在理论计算机科学352（2020）211Σ阿克斯0阿克斯阿克斯阿克斯Pandexi1.Kazakh00n−1n−1i=0阿克斯Pandexi1.Kazakh00n−1i=0阿克斯i=0i=04标准形为了证明完备性，我们需要适当的标准型c;直到适当的等价关系c<$cJ，它们为我们的理论提供标准型设x0，x1，. 是不同变量的可数无穷序列。对于任何函数变量f：n，参数序列m= i1，...，ik∈ [n]<$（其中[n] ={0，.，n-1}），以及表达式e0，...，n−1we 设置：kf（x0，.， xn−1）fm（e0，.，en−1）为我们注意到BARIXI1...Kazakhstanik[e0/x0， . ，en−1/xn−1]n−1n −1FV（fm（e0，.， en−1））=F V（e，i） 和FnV（f，m（e，...，en−1））={f}<$FnV（ei）并且fm（e0， . ，en−1）[e/x]=fm（e0[e/x]， . ，en−1[e/x]）我们注意到，如果两个这样的表达式fm （e0， . ，en−1）andndfmJ′（eJ0 ， . ，eJn′−1）are相等，则f和fJ;m和mJ;n和nJ;以及ei和eJi，对于i= 1，n;这在下面隐式地使用以确保表达式case分析的唯一性我们还注意到，正如可以预料的那样，对于任意的π和ρ，我们有：S[[fm（e0， . ，en−1）]] ρ=Dm（（f））（S[[e0]]ρ， . ，S[[en−1]]<$ρ）对于函数的偏导数的这种应用，链式法则采用以下形式引理4.1我们有：► 如果m（e0，.，en−1）n−1=f（e）、...、e）eii=0证据 假设m = i1，...，ik∈ [n]<$，则我们有如果m（e0，.，en−1）=1。kf（x0，.，xn−1）[e/x， . ， e/x]= n−1。kf（x0，.，xn−1）<$[e /x，.，e/x[英语泛读材料 阿克斯（引理2.2）=n−1fim（e0，.，en−1）imn−1n−1G.D. Plotkin/电子笔记在理论计算机科学352（2020）211227其中第二个恒等式是一个可证明的等式，另外两个恒等式是句法的。Q我们通过联立归纳法定义一组标准型c和一组原子表达式a（两组表达式）：(i) (a)任何原子表达式都是规范表达式。228G.D. Plotkin/电子笔记在理论计算机科学352（2020）211.阿克斯.阿克斯i=0阿克斯i=0阿克斯(b) 任何r∈R都是正则表达式，如果c和cJ是，则c+cJ和ccJ也是(ii) (a)任何变量x都是一个原子表达式。(b) 对任意f：n，m∈ [n] n，和标准型c0，.，cn−1，fm（c0，...，cn-1）是一个原子表达式。标准型c的直接原子子表达式的集合由结构递归定义：Im（a）={a}Im（r）=Im（c+cJ）= Im（ccJ）= Im（c）<$Im（cJ）我们注意到标准型在替换下是封闭的：c[cJ/x]是标准型，如果c和cJ是，正如通过c上的结构归纳法直接证明的那样。引理4.2对于任何标准型c和c，存在标准型CJ使得：布拉奇► 你好X=c =cJFnV（cJ）<$FnV（c）<$FnV（c）和FV（cJ）<$FV（c）<$FV（c）。证据 证明是通过归纳法对c的大小。 c是常数、变量、和或积的情况利用了引理2.1。 这留下了原子表达式fm（c0，.，cn−1），我们可以证明：如果m（c0，.，cn−1）阿克斯X=c=fm（c0，.，c n−1）[c/x]=.n=1fi m（c0， . ，cn−1）<$ci<$[c/x]（by引理4.1）=n−1fi m（c0[c/x]， . ，cn−1[c/x]）<$ci.并回忆标准型在替换下是封闭的，并将归纳假设应用于ci。Q引理4.3（规范化）对于任何表达式e，存在一个规范形式CF（e），使得f（e）= CF（e），并且FnV（CF（e））<$FnV（e）和FV（CF（e））<$FV（e）。证据 我们证明了这一点的结构归纳E。 如果e是一个变量或常数，它已经是一个标准形式。e是和或积的情况是由标准形在和和积下是封闭的这一事实得出的。其中e具有形式f（e0， . ，en−1）是im m。 从归纳总结的观点出发。最后，当e的形式为0时，使用引理4.2处理，并且x=e1归纳假说Q我们有以下的规范化引理的推论：推论4.4对于任何闭表达式e，我们有：►e=S[[e]].X=cG.D. Plotkin/电子笔记在理论计算机科学352（2020）211229证据因为e是闭的，所以根据引理4.3，CF（e）也是如此，因此后者必须没有直接的原子子表达式或自由变量，因此是一个闭多项式。因此，存在一个实数r使得<$CF（e）=r，因此，根据引理，<$e=r。 我们有r=S[[e]]。Q接下来，我们定义等价关系，它将允许我们证明规范形式之间的相等性我们还定义了多项式，将用于制定我们的埃尔米特插值问题。对于任意的m，mJ∈[n]<$，我们写m<$mJ表示m是mJ的置换。对于任何原子表达式a，a，J，我们写a，a，J表示，• a和aJ是相同的变量，否则• 对于某个函数变量f：n，对于某个m≠mJ，它们具有以下形式：fm（c0， .. . ，cn−1）andndfm′（cJ0， . ，cJn−1）with<$ci=cJifori=0， n−1.我们显然有：aaJ=a=aJ（1）我们现在将变量（称为分离变量）赋值给原子表达式，使得：va=va′ ⇐⇒a≈aJ对于任何标准型c，我们通过结构归纳法定义它的节点多项式PcPr=r（r∈R）Pa=vaPc+c′=Pc+Pc′Pcc′=PcPc′出现在Pc中的分离变量是va，a是c的直接原子子表达式。然后，我们通过以下方式定义规范形式之间的等价关系ccjPcPc′注意，这个关系只取决于c和CJ的直接原子表达式va的选择。也请注意，该关系扩展了原子表达式之间的关系，即，a，a，J与a，a，J作为原子表达式i成立，当它们作为规范形式时，它成立。引理4.5（i）对于任何具有节点多项式的正则表达式cPc（va0，.，vam−1），对于原子表达式a0，...，am-1，我们有：► c = Pc（a0，.，am−1）(ii) 对于任何规范表达式c和cJ，我们有：ccJ=c=cJ证据第一部分是由一个简单的结构归纳建立的。在c是原子表达式a的情况下，我们有va= Pc= va0，因此aa0，因此a = a0，即，C = Pc（a0）。230G.D. Plotkin/电子笔记在理论计算机科学352（2020）211对于第二部分，假设我们有规范表达式c和cJ，使得c<$cJ（因此Pc<$Pc′）。 设v为0，...，vam−1（j = 0，m）包含所有变量Pc和Pc′的关系。作为Pc<$Pc′，我们有：►Pc [a0/va0，.，am−1/vam−1] = Pc′ [a0/va0，.，am−1/vam−1]将第一部分应用于c和cJ，可以根据需要得出c=cJQ5完整性为了建立完备性，我们使用区分非等价正则形式的环境，即，标准型c和cJ使得c/c ∈cJ.我们首先需要能够区分非等价多项式的有限集合（这些将是c或cJ的次标准型的节点多项式）：引理5.1令Pi（x0，.，xm-1）是n个互不等价的多项式。然后，对于x0，...，xm−1，它们具有不同的值。证据没有一个多项式Qij= Pi−Pj是相同的0（i/= j），所以Q= P i jQij也不是。所以对于某些自然数x0，.，xm−1。 该选择区分不同的Pi。Q接下来我们需要能够解决多变量Hermite插值问题，以便为原子表达式提供指定的值。多维Hermite插值问题的维数d≥0由下式给出：• 一个有限的节点集xi∈Rd（i= 1.k），且• 对于每个节点xi，函数h：Rd→R的偏导数存在有限个条件Dmij（h）（xi）=rij（mij∈[d]R，rij∈R）。条件集必须是一致的，在这个意义上，每个rij都由节点xi和m ij的置换等价类确定。这个问题的一个解决方案是一个d元多项式函数满足所有的条件。 根据Severi [12]的一个定理（参见[9，10]），每个这样的问题都有一个f次多项式k（max（|MI J|）+1）−1。标准型的有限集合C是饱和的，如果以下两个条件成立：(i) 对于任何标准型c和c的直接原子子表达式ac∈C=A∈C(ii)（二）fm（c0，...，cn−1）∈C=c0，.，cn−1∈C显然，每一个标准形的有限集合都可以扩展为标准形的有限定理5.2（多项式分离）设C是标准型的有限集合。然后有一个多项式函数环境和一个环境区分C的任何两个不等价的元素