基于等式匹配的数学软件库服务贸易交易算法研究.

理论计算机科学电子笔记151（2006）161-177www.elsevier.com/locate/entcs基于等式匹配Aurélie Hurault和Marc PantelIRIT - ENSEEIHT，2 rue Camichel，B.P. 7122，F-31071 TOULOUSE CEDEX 7{Aureliee. 你好，马克。你看我。fr摘要数学软件库提供许多计算服务。数学运算符属性可用于组合多个服务，以提供更复杂的服务或使给定服务适应略微不同的用途。计算网格为用户提供了对大多数可用软件库的访问。服务贸易，即寻找能够满足用户需求的服务，因此很难，因为来自不同图书馆的许多不同服务和服务组合可以满足相同的需求。商业建议依赖于使用服务接口和/或特定于域的元数据和本体。 这些框架中定义的服务语义要么易于使用，但太差或依赖于应用程序（接口和元数据）;要么对于普通用户来说太复杂和复杂（本体逻辑）。 我们的工作的目的是提供一个交易框架，这是既易于使用的应用程序的专家， 在交易过程中，我们需要足够精确的服务来适应和组合服务。我们的建议是基于领域和服务描述的代数规范（与OpenMath相关）以及服务交易，适应和组合的等式匹配。本文提出了我们的框架建议和相关的交易算法，这是既健全和完整的：它可以找到所有适当的服务和组合，根据给定的语义。关键词：代数规范，方程匹配，数学软件库，服务贸易。1我们的工作目前，网格上的计算服务可以通过不同的中间件来实现，如Globus2提供的Web Services及其Open Grid扩展OGSA/OGSI1、Net.1http：//www. 格湾org/2http：//www. 我的天啊。org/1571-0661 © 2006 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2005.11.029162A. Hurault，M.Pantel/Electronic Notes in Theoretical Computer Science 151（2006）161解决方案3，Ninf4或DIET5），Corba6，Babel7，.然而，这些服务通常是为某些特定目的而设计的，需要与其他服务进行一些调整或组合，以便用于其他目的。因此，需要一个复杂的交易算法，以便根据用户的需求找到、调整和组合最合适的服务。大多数当前可用的交易框架中的服务描述都是基于服务签名（其参数名称和类型，请参阅Corba IDL、DII和DSI、Web Service WSDL、BabelSIDL等）。和元数据（通常是关键字，请参阅XML RDF8、Corba TradingService、Web Service XML，...）.这些描述通常需要使用本体来同意关键字的含义（参见OWL9，...）的。论文的其余部分组织如下。在接下来的部分中，它将详细介绍我们工作的目的和现有解决方案的局限性。然后，通过实例说明了该框架：服务描述和交易算法。然后说明它的现实性，并与其他作品进行比较它最终为我们未来的工作提供了见解。2我们工作我们的工作的主要目的是提出一个框架的服务贸易，允许给一个准确的语义服务，从而使他们的适应和组合。一个关键点是，这个框架将由应用领域的专家使用，而不需要对交易算法中使用的底层技术有任何了解。为了说明本文提出的交易者类型，我们将给出一些线性代数的例子标量将被标记为：α、β、x和矩阵：A、B、C、R、S、X、Y。第一个例子：可用的服务是R=α<$A<$B+β<$C。用户想要执行X=Y+Z。交易者必须回答R=X，α= 1，β= 1， （A=I和B=Y ）或（A=Y和B=I），C=Z。为此，交易者必须使用以下属性：1<$x=x，x<$1 =x，I<$X=X和X<$I=X。第二个例子：涉及各种运算符的属性（分布性，相等性，.）也必须使用，如以下示例所示：可用服务为R=AB+CD，请求的服务为X=U（Y+Z），3http://icl.cs.utk.edu/netsolve/第http://ninf.apgrid.org/5http://graal.ens-lyon.fr/DIET/6http://www.corba.org/7http://www.llnl. 我的意思是，我的意思是，HTML8http://www.w3.org/RDF/9http://www.w3.org/2001/sw/WebOnt/A. Hurault，M.Pantel/Electronic Notes in Theoretical Computer Science 151（2006）161163交易者必须回答R=X，A=U，B=Y，C=U，D=Z。为此，交易者必须使用属性X（Y+Z）=XY+XZ。第 三 个 例 子 ： 服 务 也应 该 使 用 前 面的 属 性 自 动 组合 。 给 定 乘 法M=C<$D和加法S=A+B服务，如果用户想执行R=Y（X+Z），有几种组合可用。交易者必须建议将一个乘法和一个加法结合起来，或者一个加法和两个乘法（Y<$X+Y<$Z）。为此，应用域、可用服务和用户请求的描述基于代数规范。定义域运算符的语义由相关代数的项之间的等式定义交易算法是基于等式匹配，它使用运营商的属性，以适应和组合可用的服务，以满足用户的需求。等式匹配通常是一个不可判定的过程，交易算法依赖于解决方案树的广度优先遍历（根是用户请求，叶子是可用的服务，分支是等式的应用该遍历受交易能量的量的约束，该交易能量的量对应于在所请求的服务和可用服务的匹配期间允许的等式应用或服务组合交易通常是一种交互活动，用户，无论是人类还是程序，都会提供一定的能量。然后，交易者将产生第一组解决方案。如果这些解决方案不能满足用户，这一个可以重新启动交易者提供更多的能量。交易算法是完整的，在这个意义上，给定无限数量的能量，它将产生所有可能的解决方案，最终花费有限的时间产生无限数量的解决方案。然而，如果它被给予有限的能量，它总是会终止3交易框架目前大多数用于交易服务的描述都基于三种方法：签名、元数据（大多数时候只有关键字）和本体。Corba、RDF和OpenMath将被用作示例。将开发以下示例所有的元素都是矩阵。• 可用的服务是：服务1（A，B）=A+B，服务2（C，D）=CD，服务3（E，F，G，H）=EF+GH。• 用户服务请求为：req（X，Y，Z）=X<$（Y+Z）。• 一些解决方案是：serv3（X，Y，X，Z）和serv2（X，serv1（Y，Z））。164A. Hurault，M.Pantel/Electronic Notes in Theoretical Computer Science 151（2006）1613.1基于签名的方法在CORBA框架中，对接口的IDL描述的分析，或者DII和DSI内省机制的使用[7]，提供了对接口的每个服务的参数列表及其类型的访问。然后可以比较所请求的和所提供的服务接口这种比较可以使用类型同构来改进。矩阵serv 1（在矩阵A中，在矩阵B中）;矩阵serv 2（在矩阵C中，在矩阵D中）;矩阵serv 3（在矩阵E中，在矩阵F中，在矩阵G中，在矩阵H中）;矩阵req（在矩阵X中，在矩阵Y中，在矩阵Z中）;这个例子说明了基于签名的方法的局限性：首先，不可能区分加法和乘法。第二，有了签名，可以说，前两个服务不能回答这个问题。第三种可能解决这个问题，但是请求的参数不能分配给服务的参数并且，应该分配给附加的第四参数的值第三，没有足够的信息来了解如何将各种服务结合起来。Web服务WSDL和Babel SIDL也会出现同样的问题3.2元数据方法OMG Corba Trading Service是一个黄页服务，它将属性列表添加到通常的IDL接口中。这些属性通过一系列对（属性名称、值）来描述服务然后，通常通过指定属性所需的值来在我们的示例中，我们选择使用比servi更明确的名称来描述服务。serv1.name（“addition”）; serv2.name（“multiplication”）;serv3.name（“addmultiplications“）;现在可以区分加法和乘法，但每个潜在用户必须知道每个服务的确切名称。可以添加属性«描述»，但描述服务功能的方式将因人而异，因应用程序而异。描述的语言可以是不同的。本体是一种在概念和相关词汇上达成一致的方式，但不允许基于功能语义的此外，如果可以描述第一种服务，那么对于第三种服务和用户请求来说，这将更加困难，因为这两种服务都结合了两个运营商。同样的问题也出现在Web Services中。让我们考虑XML RDF（资源描述框架），它是W3C元数据描述标准。描述以XML格式A. Hurault，M.Pantel/Electronic Notes in Theoretical Computer Science 151（2006）161165文档（然后可以使用XQuery10与Corba Trading Service一样，它基于对（属性名称，值）。因此，它具有同样的缺点。下面的例子提出了第一个服务的描述。 rdf：li type=“Matrix”/> rdf：li type=“Matrix”/>/rdf：Seq>矩阵/r：result>addition/n：name>基于签名或元数据的比较可以提供服务列表，然后用户可以基于其名称、文档和关键字选择适当的服务然而，没有办法使用运算符的数学属性来组合服务3.3基于本体的方法元数据是一种描述格式，通常不提供任何语义。语义由使用元数据的应用程序给出每个应用程序可以提供不同的语义。每个属性的名称和值由用户选择多个用户可以为相同的属性或属性值选择不同的名称本体为每个域提供了预定义的名称分类，并提供了一个逻辑来管理类之间的关系，从而减少了问题。OWL（Web Ontology Language）是一种W3C标准，它允许通过使用适用于其处理的本体和逻辑来定义更准确的语义然而，这种方法似乎并不适合我们的目标。实际上，控制逻辑证明引擎是困难的完整的OWL是不可判定的。有些部分（DAML+OIL，OWL-DL）是可判定的。但是，根据初步的实验，作者似乎很难定义一种枚举算法，它将有效地并以适当的顺序提供所有的解决方案，用于使用等式和服务组合来比较所请求的因此，我们需要一个基于运营商属性描述的交易框架OpenMath可以提供与代数规范方法相关的属性的适当描述第10http://www.w3.org/XML/Query166A. Hurault，M.Pantel/Electronic Notes in Theoretical Computer Science 151（2006）1613.4基于代数规范的方法半形式化描述不允许定义复杂的基于语义交易者，因此需要更准确的描述，例如代数规范[8]提供的描述用户提供用于描述服务的操作符如前所示，还提供了链接这些运算符的等式（如OpenMath中所示运算符签名和等式是代数数据类型规范的基础 服务和请求描述将是代数的术语。服务族将由一对（E，E）来描述，其中：• 签名是签名，即a couple（F，ar）其中ar将整数与F的每个元素相关联。• E是一组等式公理。下一节中的示例将使用这种形式来描述应用程序域和服务。OpenMath 11框架与W3C标准MathML 12关系密切，它使用XML文档表示数学实体。运算符在内容字典中由自然语言描述和OpenMath中的运算符属性描述这种描述与以前的代数形式主义密切相关下面的例子描述了运算符plus和交换性属性：<名称>加/名称><描述>表示n元交换函数的符号。<产品描述<联系我们然后，第一个服务将描述如下：http://www.openmath.org/cocoon/openmath/index.html12http://www.w3.org/Math/A. Hurault，M.Pantel/Electronic Notes in Theoretical Computer Science 151（2006）161167这些性质主要用来描述一个网络上的运算符对数学知识的获取。我们的目的是将其用于服务贸易。4拟议框架中的说明和交易本节将使用线性代数中的一个小例子来展示交易算法原型的输入和输出本例中的操作员数量将保持在最低限度，以方便读者所有的运算符都将应用于矩阵。4.1运算符和常量必须指定用于描述服务和请求的运算符和常量的名称、属性和符号我们还需要指定操作符是否是可交换的。可交换性可以被视为涉及更多交易步骤的共同财产。op*：2 infix.op O：cst.OP +：2infix com.//交换opI：cst.集合F定义为F={x，+，O，I}，函数ar（运算符签名）定义为：{ar（mult）= 2，ar（add）= 2，ar（O）= 0，ar（I）=0}。4.2的等式然后给出了描述和连接算子和常数的等式它们可以有任何结构，但它们的数量必须有限。1. （a+0）=a.4. （a*O）=O.7. （a*（b+c））=（（a*b）+（a*c））。2. （a*I）=a.5. （O*a）=O.8. （（b+c）*a）=（（b*a）+（c*a））。3. （I*a）=a.6. （（a+b）+c）=（a+（b+c））。方程公理的集合E则：E= {add（a，O）=a，mult（O，a）=O，mult（ a，I）= a，add（ add（ a，b），c）= add（ a，add（ b，c）），mult（ a，a）= a，mult（ a，add（ b，c））= add（ mult（ a，b），mult（ a，c）），mult（ a，O）= O， mult（ add（ b，c），a）= add（ mult（ b，a），mult（ c，a））}添加add的交换性：add（a，b）=add（b，a）。4.3服务和请求可用服务和用户请求必须使用上述指定的操作符进行描述1. serv1（a，b）=（a+b）.3. serv3（a，b，c，d）=d-（（a*b）+168A. Hurault，M.Pantel/Electronic Notes in Theoretical Computer Science 151（2006）161（c*d））。2. serv2（a，b）=（a*b）.A. Hurault，M.Pantel/Electronic Notes in Theoretical Computer Science 151（2006）161169请求：（x*（y+z））。第三个示例serv3显示了交易者使用通过引用传递的这是有用的，因为线性代数中的许多库都提供这种服务，例如BLAS [2]，它是目前用于该交易者的主要测试平台之一4.4结果交易者返回允许解决给定问题的服务集和服务组合 它被赋予有限的能量产生有限数量的解决方案，因为重复使用等式和服务组合可能导致无限数量的答案。在本示例的上下文中，它将提供以下解决方案：1. p2=serv1（y，z）;p1=serv2（x，p2）;p1;// x、y和z是用户的参数。//p2是用于实现组合的中间变量// p1是返回的2. p2=serv1（z，y）;p1=serv2（x，p2）;p1;3. serv3（x，y，x，p1=z）;p1;4. serv3（x，z，x，p1=y）;p1;5. p2=serv2（x，y）;p3=serv2（x，z）;p1=serv1（p2，p3）;p1;6. p2=serv2（x，z）;p3=serv2（x，y）;p1=serv1（p2，p3）;p1;7. p2=serv1（y，z）;serv3（x，p2，Any x1，p1=O）;p1;8. p2=serv1（z，y）;serv3（x，p2，Any x1，p1=O）;p1;+ 其他结果与组合每个解决方案都对应于一个服务执行序列，从而导致所需的结果。这个例子表明，交易者可以提出不同的可能性来执行相同的服务。当使用组合时，必须给出计算服务的顺序。当参数的值无关紧要时，它被标记为«Any»。5E匹配和E统一：算法交易算法依赖于用户请求和使用等式的可用服务必须找到响应请求的所有服务或服务组合（及其参数值 对于一个服务，s = f（v1，. v s）和请求r，必须决定服务是否等于请求的模E，以及如何计算变量v i的值（表示为请求常数的函数）。那么，布景替代品{|σ（s）=Er}，这是s和r的E-匹配子的完备集的定义（见[3]和[5]）。必须提醒读者，关于方程理论我们一无所知，也不能假定任何性质用户不了解170A. Hurault，M.Pantel/Electronic Notes in Theoretical Computer Science 151（2006）161∗重写理论，所以没有工作可以要求他把他的理论变成一个重写系统。他也不能被期望为一个完备算法（也可能不会终止）提供一个项然后，作者选择使用E-匹配的一般方程理论和计算一个完整的匹配集所做的工作。一些工作已经完成了特定的理论E-匹配，例如见[4，13]。但是，据作者所知，没有一个人在不需要重写系统或术语排序的情况下处理一般情况。在一般情况下定义的完全E-统一是唯一合适的解决方案。在大多数情况下，电子统一是不可判定的此外，E-单位元的集合不一定是有限的。关于E-匹配，人们已经针对特定的理论做了大量的工作（综述见[1]）。但是，据提交人所知，一般情况是需要的。因此，作者在一般方程理论的情况下，提出了一个完整的数学模型。Gallier和Snyder [6]定义了一个构建完整解决方案集的过程。交易算法主要基于他们的推理系统，该推理系统依赖于一组变换BT。他们证明了这个集合是完备的（«A setTis completei），对于每个等式集合 E，可以使用在T中的变换）。 他们还证明，它是健全的（«如果S~SJ与SJ当σSJ∈U（S）»）时，他们的一个缺点在于在一组问题上以任何顺序进行变换，直到不能应用更多相反，我们建议使用特定的顺序和变换次数的界限。6交易算法交易算法为BT转换的应用顺序实现了特定的启发式该启发式算法基于由用户提供的能量量（可以应用以产生E-均匀器的等式和服务组合的数量）控制的广度优先树这个启发式仍然是完整的，给出了一个未绑定的能量。系统BT，它与我们的交易算法的链接和完整性结果在[9]中描述。完整性意味着算法将找到所有可能的服务或服务组合，如果它被赋予足够的能量（可能是无限的）。这源于Gallier和Snyder的BT系统的完整性一方面，我们的算法中使用的转换被证明是等价于BT的，另一方面，我们的算法所建立的转换序列的语言被证明是等价于BT中所有可能的转换序列。在我们的交易算法中，应用的等式不是随机选择严重度-A. Hurault，M.Pantel/Electronic Notes in Theoretical Computer Science 151（2006）161171所有的等式应用被分组在称为变换的一个步骤中（相当于BT中的根重写的几个应用）。所有的等式都是预处理的，以便构建这些变换。这允许知道是否存在从一个根符号到另一个根符号的变换，所应用的变换是在所有可能的变换中选择的，只保留可能导致提供正确根符号的解的变换。事实上，项分解允许问题的简化，所以很自然地尝试用具有相同根符号的项来建立对6.1交易算法示例原理相当简单。它对应于Gallier和Snyder在本文中，我们将只给出交易过程的例子：pi~pi+1。这将通过解释导致4.4节的解1、2和3的步骤来说明。出发点是：• S1， 2={Sserv2（a，b），x<$（y+z）<$}~{S serva<$b，x<$（y+z）<$}•S3={Sserv3（a，b，c，d），x<$（y+z）<$}~{<$（a<$b）+（c<$d），x<$（y+z）<$}有了这些出发点，就能找到更多的解，但对这个例子的描述将集中在获得这些解的方法6.1.1分解两个术语的比较从它们的根符号的比较开始如果它们是相同的，它们的孩子将被比较（BT中的术语分解），并将应用保持根符号的转换（BT中的根重写），这是完整性所需的。在第一个例子中，根符号是«»，并且没有将«»保持为根符号的等式。稍后将给出一个例子。因此：S1， 2~{a，x∈，b，y+z∈}6.1.2转型如果根是不同的，将应用允许将一个运算符转换为另一个运算符的转换（BT中的根重写）。转换将具有以下形式：（e1，1，e1，2），.，（en，1，en，2）其中：给定服务的s根符号，请求的r根符号，常数和变量的Nop根符号，Root（e1， 1）=（rorNop），Rai∈[i，n−1]Root（ei，2）=Root（ei+1， 1） orRoot（ei+1， 1）=Nop，Root（en，2）=s。通过选择合适的变换，可应用的相等-172A. Hurault，M.Pantel/Electronic Notes in Theoretical Computer Science 151（2006）161f（. ）x 1g（. ）a xby+ zCBX2yX1x一DX3z在不失去解决方案的情况下限制了ities因此：S3~{<$ （ a<$b ） + （ c<$d ） ， （ x1<$x2 ） + （ x1<$x3 ） <$ ，<$x1<$（x2+x3），x<$（y+z）<$}6.1.3去除根的分解（以比较孩子）和transformations应用程序将把问题分解为更简单的子问题。这些规则将被应用，直到不能再应用，并且直到在开始时提供的所有能量的量已经被使用（该量可以由可以应用的等式或服务组合的数量来• S1， 2~{a，x∈，b，y+z∈}•S3~{（ab）+（cd），（x1x2）+（x1x3），x1（x2+x3），x（y+z）}S3~{a b，x1x2，c d，x1x3，x1，x，x2+x3，y+z}S3~{a，x1，b，x2，c，x1，d，x3，x1，x，x2，y，x3，z}当问题被切割成不可分割的子问题或搜索因能量耗尽而停止时，中间变量（xi）被移除以获得最终结果。使用变量构建有向图。 出现在分支中间的中间变量将被抑制。当所有的中间变量都被抑制后，将相关的替代应用于不同的问题进行求解。在示例中，构建了以下约束图结果将在遍历图形后给出S1，2~{a，x，b，y+z<$}~{x ›→ a，y+z ›→b}S3~{x <$a，x<$b，y<$b，y <$c，x<$d，z<$c}~{x<$→a，y<$→b，x<$→c，z<$→d}图的结构像铅运行的算法在这个问题上，（）），g（. 如果还有能量可用的话。《变量删除》等同于BT中变量删除的几个应用。因此，交易算法是一个定点算法，它将变换应用于一组E-统一问题，最终添加子问题，直到不能应用更多的变换或能量耗尽。一旦获得这些结果，如果所有的服务参数都与请求的参数相关联，则返回解决方案：S3~[serv3（x，y，x，p1=z）;p1;]这个结果是通过应用由E匹配给出的替换来获得的。A. Hurault，M.Pantel/Electronic Notes in Theoretical Computer Science 151（2006）161173算法，对服务的参数当替代值不是常量而是一个术语时，需要一个组合，并且参数的值将是执行与该术语匹配的另一个服务的结果（交易算法必须以该术语作为新请求运行）。为此，引入变量pi来存储中间结果。如果服务是一个函数，pi将存储返回值，如果它是一个过程，pi将接受修改后的参数的值。如果问题需要使用服务组合来解决，并且如果未达到最大深度，则算法将再次运行允许的组合深度是用户为解决其交易请求而SJ1， 2={sjserv1（a，b），y+z<$}~{sjserva+b，y+z<$}• SJ1，2~SJ1= {a，y，b，z}~{y ›→ a，z ›→b}•SJ1， 2~SJ2= {a+b，x1+x2<$，x2+x1，y+z<$}~{a，x1，b，x 2，x2，y，x1，z}~{z ›→ a，y ›→b}然后返回解决方案• S1， 2<$SJ1~[p2=serv1（y，z）;p1=serv2（x，p2）;p1;]• S1， 2<$SJ2~[p2=serv1（z，y）;p1=serv2（x，p2）;p1;]7绩效评价用户不能被期望知道任何关于重写和术语排序的约束导致作者选择了一个非常通用的E-统一算法，执行成本很高。本节给出了关于这些成本和算法可伸缩性的一些元素。7.1形式估计复杂度该算法的复杂度将由两项的根符号的互补数目来表示。这种复杂性很难表达，因为“最坏情况”并不真正现实（每次都可以应用所有变换而不会产生解决方案，因此无论能量的量如何，能量都将被释放而不会提供任何解决方案），并且复杂性取决于许多参数。特别是，术语（服务、请求和平等）的高度很重要。必须考虑服务的数量ns、等式的数量ne、允许的等式的数量m、组合的深度d更多细节见[9]。在下文中，我们将限制性地假设服务、请求和等式的深度为1：它们是变量、常量或174A. Hurault，M.Pantel/Electronic Notes in Theoretical Computer Science 151（2006）161项f（x1，. 其中xi是常数或变量。如果d=0（没有组合）和m=0（没有应用等式），复杂度是O（ns）：算法将只比较请求的根符号和每个服务的根符号不需要相等应用或服务组合的请求则表现为通常的交易框架。如果d= 0（无组合）且m= 0，则复杂度为O（ns<$nem）：对于每个服务，该算法可以应用nem个等式，并且对于每个等式，应用的根符号将被比较的子问题。设p是服务的参数的最大数量，并且Cd是组合深度d的复杂度。Cd=C0+（p<$ns）<$Cd−1：当没有组合时计算解，然后算法可能再次运行所有服务的所有参数。所以复杂度是O（nsd+1<$nem）。因此，最昂贵的请求将是需要大量平等应用程序和服务组合的请求。重要的是要注意：• 使用受限的应用域应导致少量的适当的等式ne。• 允许的等式数量m和允许的组合深度d通常很小，更重要的是，对解的搜索将从m= 0开始，然后m= 1，.并且d= 0则d= 1，...，这样就能更快地找到第重要的一点是用户控制这些参数的值。• 因此，服务的数量ns是网格上唯一可以很大的参数，并且算法复杂度是次数为d+1的多项式。该算法根据服务的数量很好地扩展一些服务可以预先计算，以提高可扩展性，根据平等的应用和服务组合的数量服务的数量增加，应用和组合的数量减少。同样重要的是要记住，如果算法没有找到任何适当的解决方案，它将在能量耗尽时停止，并允许用户通过提供更多能量来重新开始交易因此，用户将始终控制交易过程。最重要的一点是，网格上可用的服务是相当粗粒度的。大多数计算应该在服务内部完成，而不是使用服务属性。因此，这些性质不应该描述递归计算，比如整数的代数指定该框架将能够处理这种域和服务描述，但通过交易进行计算的成本将非常高。这个算法显然不是为了这个目的而设计的。A. Hurault，M.Pantel/Electronic Notes in Theoretical Computer Science 151（2006）1611757.2实验当确定要找到所有的解决方案时，交易算法可能需要很长时间才能找到一个简单的例子。所有给出的时间指示都是通过使用Pentium 4，1.8 GHz，512Mo运行以下具有O'CaML原型的示例获得的op ^-1：1后缀。opO：cst.OP ^T：1后缀。执行部分一：科技委。op *：2 infix.op 'n'：cst.OP+：2 infix com.op 't'：cst.opope：2 prefix.（a*（b + c））=（（a*b）+（a*c））。（a*I）= a.（（b + c）*a）=（（b*a）+（c*a））。（I*a）= a.（（a + b）^T）=（（a ^T）+（b ^T））。（a * O）= O.（（a * b）^T）=（（b ^T）*（a ^T））。（O * a）= O.（（a*b）^-1）=（（b ^-1）*（a ^-1））。（I^T）=I.（（a + b）+ c）=（a +（b + c））。（a +0）= a.（ope'n（op't'a（O ^T）= O.（I^-1）=I.（（a^-1）*a）=I.（a*（a^-1））=I.dist（e，f，g，h）=（（e * f）+（g * h））。 加上（a，b）=（a + b）。fois3（e，c，d）=（e *（c * d））。fois（c，d）=（c * d）.plus3（a，b，c）=（（a + b）+c）.transs（a）=（a ^T）。transplus2（a，b，c）=（a ^T）+b）+c）。inv（a）=（a ^-1）。invplus2（a，b，c）=（a ^-1）+b）+c）.plusid（a）=（a + a）.plus4（a，b，c，d）=（a+（b+（c + d）。invplus（a，b）=（（a ^-1）+b）.transfois（a，b）=（（a ^T）* b）。sgemm（m，n，k，ta，tb，a，b，c）=（opetaa）*（opetbb））+ c）-> c。（x *（y + z））。对于本例，该算法需要14m51.770s才能找到57258个解具有1和3个允许等式的组合深度7.3交易算法改进大多数用户交易服务来执行它们。一些交易结果应该被拒绝。例如，如果建议的组合服务的参数之一与初始请求相同，则组合执行将不会修改子服务的结果。必须拒绝此解（例如，0+t或1t）。该算法现在需要14m15.320s来找到56734个解决方案。例如，解plus（O，dist（x，y，x，z））被拒绝。前面的测试在没有使用等式的情况下比较了期限结构用户可以在没有任何重写知识的情况下命令一些等式（例如a+O→176A. Hurault，M.Pantel/Electronic Notes in Theoretical Computer Science 151（2006）161a）。然后使用此重写规则来简化术语并改进术语比较。为了找到所有的解决方案，仍然需要完全的平等当等式的一边是常量或变量时，可以自动推导出这种排序的一部分，然后将常量或变量作为结果（右部分）对规则进行排序这种自动化的简化目前正在我们的原型中使用用户将能够在下一个版本中指示重写顺序该算法现在需要0m28.080s找到5226个解决方案。溶液fois（x，plus3（y，z，plus（O，O）被拒绝。重写理论的结果，例如自动建立术语排序时，他们是可用的，将在以后用于改善这一部分。请注意，当两个相等的项被决定为不同的时，不会造成任何损害，因为它只会降低性能。大多数情况下，第一个结果会让用户满意。因此，寻找其他人是没有用的。必须在寻找服务所需的时间和执行服务所需的时间之间找到一个折衷方案。使用能量的数量，也可以要求交易者一步一步地提供结果，并在产生满意的结果时停止。更重要的是，如果应用更少的等式和组合，解决方案将更接近于要求并且不那么复杂。第一个解决方案通常是最有趣的。这只是根据所举例子得出的意见，需要进行深入研究。该算法的第一步仅需不到1 s的时间，即可找到23个解（其中fois（x，plus（y，z）））。第二步在不到5s的时间内获得，并计算1014个解（其中dist（x，y，x，z））。7.4与网格调度器的我们的工作重点是服务的功能属性。稍后，它将扩展非功能属性及其与GRID-TLSE1314项目中参数值的关系（参见[11，12]）。这将允许考虑到一些算法针对参数的特定值进行了优化，从而减少了可能应用的服务数量并提高了交易框架的性能解决方案生产顺序可以使用有序遍历进行修改，该遍历基于用户根据他对应用领域中运营商成本的了解为等式和服务定义的权重在线性代数的情况下，交易员目前正在集成在GridRPCDIET中间件中，这使得复杂的调度成为可能。13项由法国国家科学基金通过ACI GRID14http://www.enseeiht.fr/lima/tlseA. Hurault，M.Pantel/Electronic Notes in Theoretical Computer Science 151（2006）161177伊茨。DIET将根据网格的计算和通信性能提供动态权重（详见[10]），从而提高第一结果的质量。这种交互允许在功能方面和执行条件上交易服务。DIET将逐步运行算法，使用所有以前的改进，并使用自己的指标重新评估解决方案的质量它会要求更多的要求，直到满足为止。它有自己的缓存，这将有助于可扩展性。由于集成目前正在进行中，因此没有性能结果8与同类作品在Monet15和HELM16项目中，计算服务的描述是基于MathML和OpenMath的，它们提供了对服务的准确描述，并部分地激励了我们作为平等来源的工作但是服务的比较是基于RDF和本体的，这不允许在交易过程中容易地调整和组合服务NASA的Amphion项目[14]，特别是定理证明器SNARK遵循相同的方法。但是，这些项目依赖于“项重写和关于等式推理的调节规则”。假设，«当应用域理论被公式化时，提供递归路径排序»。这个约束打破了用户不需要了解任何底层技术的要求9结论和未来工作本文描述了在服务交易框架中实现该算法的原型是可操作的。但是，它需要一些包装，以便集成到真正的组件交易商中。XML输入应该简化与其他应用程序的通信OpenMath等式格式描述可以用于此目的。这将允许作者对实际大小的问题进行实验。运算符的描述将被丰富，以考虑参数类型和算法属性，以减少可以应用于给定问题的等式的数量。目前的原型是集成在网格RPC中间件，以允许用户搜索服务的基础上的数学描述，而不是一个简单的名称。还将使用Grid-TLSE项目提供的元数据，以减少可应用于给定1 5 http：//monet.nag. 有限英国/cooon/monet/index.html16 http://helm.cs.unibo.it/178A. Hurault，M.Pantel/Electronic Notes in Theoretical Computer Science 151（2006）161term. 最后，我们计划将我们的原型集成在MatLab环境中，以帮助用户浏览可用的数学库。引用[1] F. Baader和W.斯奈德 统一理论。 以. Robinson和A. Voronkov，编辑，《自动推理手册》，第一卷，第八章，第445Elsevier Science，2001年。[2] L. Susan Blackford和James Demmel等，《基本线性代数子程序更新集》（An updated set ofBasic Linear Algebra Subprograms，BLAS）。ACM Trans. Math. Softw. ，28（2）：135[3] H.- J. Bürck