金融市场交易的正式验证

2022-6-24 09:55:04

交易员也使用计算机算法在市场上下订单。随着计算机辅助交易的到来，市场的交易量和流动性急剧增加，因此，市场变得更加复杂。支持整个交易过程的软件程序极其复杂，并且必须满足高效标准，因为它们需要实时处理大量数据。此外，为了提高市场交易者的信心，市场监管机构为这些软件制定了严格的安全和公平准则。传统上，为了满足这些标准，软件开发广泛依赖于在大数据集上测试程序。虽然测试有助于识别bug，但它不能保证bug的存在。即使是交易软件中的小错误也可能对整体经济产生灾难性影响。对手可能会利用一个bug来为自己谋利，也会为其他真正的交易者谋利。在健康的经济中，这些事件当然是不可取的。最近，证券交易所出现了各种违反交易规则的情况。例如，在[1]中，监管机构指出：“纽约证券交易所Arca未能在特定的市场条件下执行特定类型的限制指令，尽管有一条规则，这被称为算法交易。根据知识共享许可证获得许可，由莱布尼茨国际诉讼公司抄送，载于德国达布尼茨出版公司Dagstuhl–Leibniz Zentrum für Informatik，Dagstuhl Publishing，GermanyXX:2金融市场交易的正式验证声明纽约证券交易所Arca将执行此类订单”。这是一个不符合其规范的项目实例。

扫码加我拉你入群

请注明：姓名-公司-职位

以便审核进群资格，未注明则拒绝

2022-6-24 09:55:07

在这里，该计划是交易所使用的匹配算法，监管指南是该计划的广泛规范。请注意，在大多数情况下，监管机构规定的指南并不是该计划的完整规范。此外，没有正式保证这些准则是一致的。这些都是一些严重的问题，可能会危及市场的安全性和完整性。计算机科学中形式化方法的最新进展可以很好地用于确保安全和公平的金融市场。在过去几十年中，形式化方法工具在证明大型软件和硬件系统的正确性方面越来越成功【9、8、12、10】。虽然模型检查工具已用于硬件验证，但交互式定理证明器在大型软件验证中的使用相当成功。使用这些工具对金融算法进行正式验证，有助于对整个市场行为进行严格分析。交易所（场馆）使用的匹配算法是金融市场广泛使用的算法的核心。验证匹配算法的正式框架也可用于验证金融市场中的其他算法。1.1 exchangeAn交易所的交易概述是一个有组织的金融市场。有各种类型的交易所：股票交易所、商品交易所、外汇交易所等。交易所有助于买卖双方就在交易所注册的产品进行交易。潜在的贸易商（买方或卖方）在市场上为某种产品下订单。这些指令由证券交易所配合执行交易。

扫码加我拉你入群

请注明：姓名-公司-职位

以便审核进群资格，未注明则拒绝

2022-6-24 09:55:10

大多数证券交易所主要在两个交易时段进行交易：上市前（或拍卖时段）和连续市场（或常规交易时段）。上市前阶段通过发现产品的开盘价来减少市场的不确定性和波动性。在上市前阶段，交易所在固定的时间内收集所有买入请求（出价）和卖出请求（要求）。在此期间结束时，交易所使用匹配算法以单一价格匹配这些买卖请求。在连续的市场交易中，新来的买家和卖家不断地相互匹配。传入的出价（ask）（如果匹配）将立即与现有的出价（ask）匹配。否则，如果出价（ask）不匹配，则将其放置在按价格排序的优先级队列中。交易员可以在这两个交易日下多个数量的每种产品的订单进行交易。然而，为了进行市场分析，必须假设每个订单是单个产品的单个单元；多个quantityorder始终可以被视为一组订单，每个订单都有一个数量，单个产品的分析将分别适用于所有产品。因此，请注意，下多个单位订单的单个交易员被视为多个交易员分别订购一个单位，即使在连续市场中也是如此。因此，在两次交易中，多个买家和卖家同时匹配。一种用于匹配多个买家和卖家的机制称为双边拍卖[7]。在双边拍卖中，拍卖商（如交易所）在一段时间内收集买卖请求。每个潜在的交易者下的订单都有一个限价：纽约证券交易所和群岛交易所合并形成了纽约证券交易所Arca，这是一个股票和期权都可以交易的交易所。Suneel Sarswat和A.K。

扫码加我拉你入群

请注明：姓名-公司-职位

以便审核进群资格，未注明则拒绝

2022-6-24 09:55:13

辛格XX：3卖方不会出售，超过该标准买方不会购买。该时间段结束时的交易所根据这些订单的限价匹配这些订单。整个过程是使用双边拍卖匹配算法完成的。双边拍卖的设计算法已经得到了很好的研究[13、17、14]。这些研究的一个主要重点是最大化匹配的数量或最大化拍卖商的利益。在拍卖理论文献中，拍卖师的利益被定义为匹配买卖对的限价之间的差异。然而，如今大多数交易所通过向交易员收取交易成本来赚取利润。因此，最大化匹配数量可以提高交易所的收益以及市场的流动性。除了在评估匹配算法的有效性时考虑的匹配数量外，还有其他重要属性，如公平性、一致性和个人合理性。然而，众所周知，没有任何一种算法可以同时拥有所有这些属性【17，13】。1.2相关工作我们之前没有已知的正式确定交易所使用的财务算法的工作。Passmore和Ignatovich在[15]中强调了金融市场正规化的重要性、机遇和挑战。他们的工作详细描述了为确保市场安全和公平而需要验证的金融算法的整体情况。交易所使用的匹配算法是整个频谱的核心。另一方面，有相当多的作品将拍卖理论中的各种概念形式化[6、11、16]。这些作品大多集中于Vickrey拍卖机制。在Vickreyauction中，有一个卖方拥有不同的项目，多个买方拥有每个项目子集的估值。

扫码加我拉你入群

请注明：姓名-公司-职位

以便审核进群资格，未注明则拒绝

点击查看更多内容…

2022-6-24 09:55:15

每个买家对每一个项目组合进行投标。在投标结束时，卖方的目标是通过适当地将项目分配给买方，使项目的总价值最大化。1.3我们的贡献在这项工作中，我们正式定义了拍卖理论中与金融市场交易分析相关的各种概念。我们在Coqproof assistant中定义了出价、请求和匹配等概念。Coq的相关类型对于这些概念的简洁表达非常有用，这也反映了它们的自然定义。在准备好基本框架后，我们定义了双边拍卖中匹配的重要属性：公平性、一致性、最大化和个人理性。这些物业反映了各种交易监管准则。此外，我们正式证明了这些性质的各种组合的存在性的一些结果。例如，公平和最大化总是可以同时实现的。这些结果也可以解释为监管指南各子集的一致性证明。我们在Coq证明助手的构造性设置中证明了所有这些结果，而没有添加任何额外的公理。这些证明是使用可计算的函数完成的，这些函数计算的是实际情况（Certificate）。我们还使用可计算函数在列表上表示各种谓词。最后，我们使用此设置来验证两类重要匹配算法的属性：动态价格算法和统一价格算法。在第2节中，我们正式定义了双边拍卖的理论。在第3节中，我们定义并证明了双边拍卖中匹配算法的一些重要性质。特别地，我们提出了一种动态价格匹配算法，该算法可以产生最大匹配和公平匹配。

扫码加我拉你入群

请注明：姓名-公司-职位

以便审核进群资格，未注明则拒绝

2022-6-24 09:55:18

在第3.3节中，我们描述了一种统一的价格匹配算法，该算法使用DXX:4金融市场交易的正式验证来发现金融市场中的价格。此外，我们证明了它产生的匹配在所有可能的一致匹配中是最大的。我们在第4节总结了这项工作，并对未来可能的工作进行了概述。本文中概念和证明的Coq形式化可参见[4]。2建模双边拍卖拍卖是一项竞争性活动，将商品和服务出售给最具竞争力的参与者。参与交易的交易者的优先级取决于出价和要价的各种属性（例如价格、时间等）。这种优先级最终可以通过按顺序对其排序来表示。序列最好使用Coqstandard库中的列表数据结构来表示。2.1出价、要价和限价在任何双边拍卖中，多个买家和卖家下单购买或出售标的产品。拍卖商根据他们的限价匹配这些买卖请求。虽然采购订单（即bid）的限价是买方不想购买的价格，但销售订单（即ask）的限价是卖方不想出售的价格。如果交易者希望买卖多个单位，他可以创建多个具有不同ID的出价或询问。我们可以使用包含两个字段的记录来表达出价和请求。记录Bid：类型：=Mk\\u Bid{bp：>nat；idb:nat}。记录Ask：类型：=Mk\\u Ask{sp：>nat；ida:nat}。对于标书b，（bp b）是限价，（idb b）是其唯一标识符。同样，对于ANAK a，（sp a）是限额价格，（ida a）是a的唯一标识符。请注意，当以最低面值的货币单位（如美国的美分）表示时，限额价格是自然数。

扫码加我拉你入群

请注明：姓名-公司-职位

以便审核进群资格，未注明则拒绝

2022-6-24 09:55:22

另请注意，在第一个投标字段中使用了强制符号：>。它将bp声明为一个隐式函数，该函数应用于在预期自然数的上下文中出现的Bid类型的任何术语。因此，从现在起，我们可以简单地使用binstead of（bp b）来表示b的限价。同样，我们可以使用a来表示ask a的限价。由于Bid和ask两个领域的相等性都是可判定的（即nat:eqType），因此也可以证明Bid和ask的相等性是可判定的。这是通过取消两个规范实例bid\\u eqType和ask\\u eqType来实现的，这两个实例将bid和ask连接到eqType。2.2双边拍卖中的匹配所有买卖请求可假设分别存在于列表B和列表A中。在拍卖时，拍卖师将B中的出价与A中的要求进行匹配。如果B≥ a（即bp b≥ sp a）。此外，拍卖师为每个匹配的买卖对指定一个交易价格。这个过程产生一个匹配的M，它由所有匹配的买卖对及其交易价格组成。我们将匹配定义为一个列表，其条目类型为fill\\u类型。记录fill\\u type:type：=Mk\\u fill{bid\\u of:bid；ask\\u of:ask；tp:nat}Suneel Sarswat和A.K.Singh XX:5在匹配的M中，bid或ask最多出现一次。请注意，B中可能有一些出价与M中的任何请求都不匹配。类似地，可能有一些任务inA与M中的任何投标不匹配。M中的投标列表由BM表示，M中的任务列表由AM表示。例如，图1显示了投标清单B和询价清单a之间的匹配M。请注意，BM中不存在限价37的投标，因为它与M中的任何询价都不匹配。][][][][][][][][][][][][][][][][][][][][][][][][][BAM图1 B中的投标和a中的询价分别用右括号和左括号与其限价一起表示。

扫码加我拉你入群

请注明：姓名-公司-职位

以便审核进群资格，未注明则拒绝

mingdashike22

2022-6-24 09:55:24

M中每个匹配的买卖对都使用相同颜色的括号显示。限价37、83和120的投标与匹配M中的任何ask都不匹配。更准确地说，对于给定的bid B列表和ask a列表，M是匹配的i F，（1）M中的所有bid-ask对都是匹配的，（2）BMis无重复，（3）AMis无重复，（4）BM B、和（5）上午 A、我的定义1。matching\\u in B A M：=所有\\u可匹配的M∧ NoDup BM公司∧ NoDup AM∧ BM公司 B∧ 调幅 A、上述定义中的“NoDup BMI”一词表示，每次投标都是对一个单位项目的交易请求，项目是不可分割的。我们使用表达式BM B表示术语（子集BMB）。它表达了这样一个事实，即列表中的每个元素bmi也存在于列表B中。虽然谓词NoDup和Subset能够有效地表达匹配的概念，但我们需要更多的定义来描述双边摩擦中匹配的属性。在图2中，我们描述了列表上的三个二元关系，即sublist、included和perm，它们有助于说明导致重要匹配结果的一些中间引理。例如，考虑以下引理，该引理指出匹配的性质在置换下是不变的。I引理2。匹配库存：perm M M->perm B B->perm A A->在BA M中匹配\\u->在B“A”M中匹配\\u。请注意，列表的置换概念类似于多重集中的相等。更准确地说，我们有以下指定perm关系的引理。引理3。perm\\u简介：( a、 count a l=count a s）->perm l s.I引理4。perm\\u elim：perm l s->( a、计数a l=计数a s）。引理3中的术语（计数a l）表示列表l中元素a的出现次数。在证明匹配M的各种属性时，我们经常以BM、AMAN和PM中的信息为基础进行论证。

扫码加我拉你入群

请注明：姓名-公司-职位

以便审核进群资格，未注明则拒绝

2022-6-24 09:55:28

因此，让引理建立BM、AMAN和PMM之间的相互作用以及列表上的上述关系是有用的。二十： 6金融市场交易的正式验证ABFB（a）子列表（b）包括（c）Perml1l1l2l1l2abcdfabcdefgabbcdcaebcdaeabccbabedbffigure 2列表条目之间的虚线证实了这些条目在两个列表中的存在。（a）如果Lis子列表中的每个Lis条目也出现在土地上，则它们会以相同的顺序出现。（b）包含在Lif中的列表Lis，Lis中的每个条目也存在于L。（c）如果两个条目在两个L.I引理5中的发生次数相同，则两个列表彼此的Lare排列。included\\u M\\u imp\\u included\\u投标：included M M->included BMBM。I引理6。included\\M\\u imp\\u included\\u asks:included M M->included amam上述引理中包含的概念类似于多集上的子集关系。我们有以下引理来说明包含关系的确切行为。I引理7。included\\u简介：( a、计数a l≤ 计数a，s）->包括l，s，I引理8。included\\u elim：包含l s->( a、计数a l≤ 计数a s）。在这项工作中，我们遇到了输入和输出都是列表的各种流程。我们需要类似于子序列关系的子列表关系来正确地指定这些过程的行为。I引理9。sublist\\u intro1（a:T）：sublist l s->sublist l（a：：s）。I引理10。sublist\\u elim3a（a e:T）：sublist（a：：l）（e：：s）->sublist l s。请注意，如引理10所示，sublist的递归性质。它使得在先行词中包含子列表的语句更容易归纳。但是，对于其他关系（即included和perm），情况并非如此。3双边拍卖分析在这项工作中，我们不考虑对拍卖商的利益进行分析。因此，匹配的买卖双方的买方支付的金额与卖方收到的金额相同。

扫码加我拉你入群

请注明：姓名-公司-职位

以便审核进群资格，未注明则拒绝

2022-6-24 09:55:31

匹配的买卖对的价格称为该对的交易价格。由于abuyer的限价是她不想购买的价格，因此该买家的交易价格预计将低于其限价。同样，卖方的交易价格预计将高于其限价。因此，在任何匹配中，阿比德ask对的交易价格都应介于其限制价格之间。具有此属性的匹配称为单独有理（IR）匹配。请注意，任何匹配都可以转换为IRmatching，而无需更改其bid-ask对（见图3）。在双边拍卖机制的设计中，匹配算法产生的匹配买卖对的数量至关重要。增加匹配竞价邀请的数量增加了市场的流动性。因此产生最大匹配的是anSuneel Sarswat和a.K.Singh XX:7][][][][][][][][][][]]][[[[[M1M2图3彩色点表示相应匹配的bid ask对交易的交易价格。而匹配的Mis不是IR，因为一些点位于对应的匹配的bid ask对之外。匹配的Mis IR是因为区间内每个匹配的bid ask对的交易价格。请注意，匹配的Mand M包含完全相同的bid ask对。重要方面双边拍卖机制设计。对于给定的出价列表B和请求列表a，如果没有其他匹配的同一B和a包含比M更多的匹配出价-请求对，则匹配M是最大匹配。I定义11。Is\\u MM M B A：=（匹配B A M中的\\u）∧ ( M\'，匹配B AM中的\\u\'→ |M’|≤ |M |）。在某些情况下，为了产生最大匹配，不同的买卖对必须指定不同的交易价格（图4）。然而，同一市场上同一产品的不同价格同时导致一些贸易商的不满。

扫码加我拉你入群

请注明：姓名-公司-职位

以便审核进群资格，未注明则拒绝

2022-6-24 09:55:34

以相同的交易价格清除所有匹配的买卖对的机制称为统一匹配。这也被称为感知公平。（a） UM（b）MMBABAFigure 4在这种情况下，尺寸2的唯一合理匹配是不均匀的。3.1公平性与限价较低的投标相比，限价较高的投标更有竞争力。同样，与限价较高的询价相比，限价较低的询价更具竞争力。在竞争激烈的市场中，更具竞争力的交易者优先匹配。优先考虑更具竞争力的交易者的匹配称为公平匹配。我的定义12。fair\\u on\\u bids M B：= b b’，在b b中∧ 在b’b->b>b’->Inb’BM->在b BM中。我的定义13。fair\\u on\\u问M A：= s s’，在s A中∧ 在s\'A->s<s\'->Ins\'AM->s AM中。我的定义14。Is\\U fair M B A：=fair\\U on\\U asks M A∧ fair\\u on\\u bids M B。这里，谓词fair\\u on\\u bids M B表示匹配的M对买家B列表是公平的。同样，谓词fair\\u on\\u ask M A表示匹配的M对卖家A列表是公平的。出价和ask公平的匹配使用谓词fair M B A来表示。XX:8金融市场交易的正式验证与统一匹配一样，在不影响匹配大小的情况下，始终可以实现公平匹配。我们可以通过将任何匹配转换为公平匹配而不改变其大小来实现这一点。例如，考虑以下函数make\\u FOB。固定点Make\\u FOB（M：列表填充类型）（B：列表出价）：=匹配（M，B）与|（nil，_）=>nil |（M：：M，nil）=>nil |（M：：M，B：：B\'）=>（Mk\\u fill B（ask\\u of M）（tp M））：：（Make\\u FOB M“B”）结束。函数make\\u FOB根据给定的匹配和投标B列表生成一个公平的\\u on\\u投标匹配，两者都按投标价格的降序排序（见图5）。

扫码加我拉你入群

请注明：姓名-公司-职位

以便审核进群资格，未注明则拒绝

2022-6-24 09:55:38

请注意，make\\u FOB不会更改M中的任何ask，并且由于make\\u FOB onB的递归性质，在替换过程中不会重复投标。因此，新的BMis无重复。一旦我们在出价上获得了公平匹配，我们就使用类似的函数make\\u FOA来生成公平匹配。BABABAMake FOBMake Foam1m2m3图5中的虚线表示匹配M、M和M中的匹配买卖对。在第一步函数中，make\\u FOB在MRecursive上运行。在每一步中，它都会选择顶级的bid-ask对，比如Mand中的（b，a），并用b中最具竞争力的出价替换bid b。这个过程的结果是一个公平的\\u-on\\u出价匹配M。以类似的方式，函数make\\u-foache会更改Mintro a-on-ask匹配M的公平。更准确地说，对于函数make\\u-FOB和make\\u-FOA，我们有以下引理分别证明其公平的bids和fair-on-ask。I引理15。mfob\\U fair\\U on\\U bid M B：（排序M）->（排序B）->子列表PBMPB->fair\\U on\\U bids（Make\\u FOB M B）B。I引理16。mfob\\U fair\\U on\\U ask M A：（排序M）->（排序A）->子列表PAMPA->fair\\U on\\U ask（Make\\u FOA M A）A。I定理17。exists\\u fair\\u matching（Nb：节点B）（Na：节点A）：matching\\u inB A M->（） M\'，匹配B A M中的\\u\'∧ M’B A公平吗∧ |M |=| M’|）。定理17的证明依赖于引理16和引理15。此外，引理16和引理15可以通过归纳M.3.2最大匹配的大小来证明。任何市场中的流动性都是衡量一个人在没有太多成本的情况下在市场中交易的速度。增加流动性的一种方法是最大限度地增加匹配的投标askpairs的数量。在上一节中，我们已经看到，任何匹配都可以更改为fairSuneel Sarswat和a.K.Singh XX:9匹配，而不改变其大小。因此，我们可以在不影响匹配公平性的情况下进行最大匹配。在本节中，我们将描述一个公平且最大的匹配。

扫码加我拉你入群

请注明：姓名-公司-职位

以便审核进群资格，未注明则拒绝

2022-6-24 09:55:41

对于给定的bid B列表和ask a列表，可以通过两个步骤实现最大和公平的匹配。在第一步中，我们应用函数product\\u mms，该函数生成一个匹配，该匹配在投标时是最大且公平的。在下一步中，我们将make\\u FOA应用于此最大匹配，以生成公平匹配（见图6）。Bababaproduct-MMMake-foam1m2图6在第一步中，函数product\\u-MM递归操作投标列表B和任务列表A。在每次迭代中，product\\u-MM选择最具竞争力的可用投标，然后与最大的可匹配任务配对。此函数的输出是公平的，因为它不会从顶部留下任何出价。在第二步中，函数make\\u FOA将mint转换为公平匹配M。Fixpoint product\\u MM（B：列表出价）（A：列表询问）：（列表填充类型）：=将（B，A）与|（nil，\\u）=>nil |（B：：B\'，nil）=>nil |（B：：B，A：：）=>将（A<=B）与| true=>（{Bid\\u of：=B；Ask\\u of：=A；tp=（bp）|：：（product\\u MM B“A”）| false=>生成\\u MM B A“end。在每次迭代中，PRODUCT\\U MM生成一个可匹配的bid ask对（见图6）。由于函数PRODUCT\\u MM在B和A上都具有递归性质，因此它从不将任何bid与多个ASK配对。这确保匹配中的投标列表（即BM）无重复。请注意，PRODUCT\\u MM会尝试匹配出价，直到找到匹配的ask。当所有出价都匹配或遇到没有匹配ask可用的出价时，函数终止。因此，函数product\\u MM从给定的bidsB列表和ask a列表中生成匹配，这两个列表都是按限制价格降序排序的。以下定理表明，当两个波段a按限价降序排序时，函数PRODUCT\\u MM产生最大匹配。定理18。

扫码加我拉你入群

请注明：姓名-公司-职位

以便审核进群资格，未注明则拒绝

2022-6-24 09:55:44

product\\u MM\\u is\\u MM（Nb：NoDup B）（Na：NoDup A）：排序的B->排序的A->is\\u MM（product\\u MM B A）B A。证明：我们使用列表A大小的归纳来证明这个结果。归纳假设（IH）： A’，| A’|<| A |-> B、排序B->排序A“->为\\u MM（生产\\u MM B A’’B A’。设M是出价列表B和请求列表A上的任意匹配项。此外，假设B和A分别是B和A中最顶层的出价和请求（即A=（A：：A）和B=（B：：B））。我们证明| M |≤ |在以下两种情况下产生| MM B A |。二十： 10金融市场交易的正式验证case-1（b<a）：在这种情况下，a的限价严格高于b的限价。在这种情况下，函数product\\u MM计算B和a的匹配。注意，由于归纳假设（即IH），这是B和a的最大匹配。由于ask a的限价高于B中最具竞争力的投标B，因此它不能出现在B和a的任何匹配中。因此，B和a的最大匹配也是B和a的最大匹配。因此，我们有| M |≤ | 制作| MM B A |。案例2（a≤ b）：在这种情况下，PRODUCT\\u MM生成大小为m+1的匹配，其中m是匹配PRODUCT\\u MM BA的大小。我们需要证明| M |≤ m+1。请注意，由于归纳假设（即IH），匹配产生的结果是a带上的最大匹配。因此，a带上的任何匹配都不会大于m。在不丧失一般性的情况下，我们可以假设m也按照比价的降序排序。现在，我们进一步将该案例分为以下五个子案例（见图7）。（a）（b）（c）（d）（e）B0A0MMMM1MM1MM1B0A0B0A0B0A0B0B0B0B0A0A0A0A0A0BABBAABBAABB0A0A0A0A0A0A0A0B0B0==>==>==>图7显示了案例2的所有五个子案例（即当b≥ a）。虚线显示匹配M中存在连接对。出价列表B和请求列表A均按其限制价格的降序排序。

扫码加我拉你入群

请注明：姓名-公司-职位

以便审核进群资格，未注明则拒绝

2022-6-24 09:55:49

此外，我们假设B=B：：波段A=A：：A.Case-2A（M=（B，A）：：M）：在这种情况下，匹配M中的bid B与ask A匹配（见图7（A））。请注意，Mis a在频带a上匹配。自| M |≤ m wehave | m |=| m |+1≤ m+1。案例2B（b/∈ BM公司∧ a/∈ AM）：在这种情况下，匹配M中既没有bid b也没有ask a（见图7（b））。因此，M是频带a上的匹配项。因此，我们有| M |≤ m<m+1。案例2C（b、a）∈ M∧ （b、a）∈ M：在这种情况下，我们有（b，a）∈ M和（b，a）∈ M此处a∈ A和b∈ B、我们可以获得另一个与M相同大小的匹配Mof（见图7（c）），其中（B，a）∈ 曼德（b，a）∈ M、请注意，Mis的所有其他条目与M相同。因此，我们有M=（b，a）：：M在a带上有误匹配。自| M |≤ m我们有| m |=| m |≤ m+1。案例2D：（b、a）∈ M∧ a/∈ AM：在这种情况下，我们有（b，a）∈ M和a/∈ Amwhere公司∈ A、我们可以获得与M相同大小的另一个匹配Mof（见图7（d）），其中（b，A）∈ M、因此，我们有M=（b，a）：：M在BandA上没有匹配。自| M |≤ m我们有| m |=| m |≤ m+1。案例2E：（b，a）∈ M∧ b类/∈ BM：在这种情况下，我们有（b，a）∈ M和b/∈ BMwhereb公司∈ B、我们可以获得另一个与M尺寸相同的匹配Mof（见图7（e）），其中Suneel Sarswat和A.K.Singh XX:11（B，A）∈ M、因此，我们有M=（b，a）：：M在BandA上没有匹配。自| M |≤ m我们有| m |=| m |≤ m+1。请注意，上述证明中的所有情况都对应于谓词，这些谓词只能使用列表上的成员谓词来表示。因为我们在列表的元素上有可判定的等式，所以所有这些谓词也是可判定的。因此，我们可以对它们进行案例分析，而无需假设任何公理。既然我们证明了product\\u MM的极大性，我们就可以通过将Make\\u FOA和Make\\u FOB函数应用于product\\u MM的输出来产生公平的和最大的匹配。

扫码加我拉你入群

请注明：姓名-公司-职位

以便审核进群资格，未注明则拒绝

2022-6-24 09:55:52

更准确地说，对于给定的投标清单B和要求清单a，我们有以下结果表明存在一个最大且公平的匹配。I定理19。exists\\u fair\\u最大值（B：列表出价）（A：列表询问）： M、（Is\\u fairM B A∧ Is\\u MM M B A）。3.3金融市场匹配上市前会议的一个重要方面是发现一个单一的价格（均衡价格），在这个价格下，最大的需求和供应可以匹配。大多数交易所在这一交易日以均衡价格进行交易。考虑函数UM，它产生了一个在所有一致匹配中公平且最大的个体理性匹配。不动点生成（B：列表出价）（A：列表询问）：=将（B，A）与|（nil，u）=>nil |（|，nil）=>nil |（B：：B，A：：A））=>将（A<=B）与| false=>nil | true=>（{Bid\\u of：=B；Ask\\u of：=A；tp：=（bp B）|}）：：生成| B“A”End。定义统一价格B A：=bp（bid\\U of（last（PRODUCT\\U UM B A）））。定义UM B A：=替换\\u列（生产\\u UM B A）（统一价格B A）。函数product\\u UM生成买卖对，uniform\\u price计算uniformprice，最终UM生成统一匹配。函数product\\u UM是递归的，它在每次操作中都会将B中最大的可用bid与A中最小的可用ask进行匹配（见图8）。当B中可用的最具竞争力的投标与A中的任何可用ask都不匹配时，此函数终止。以下定理表明，当投标列表B按限价降序排序，而ask列表A按限价升序排序时，函数PRODUCT\\u UM在所有一致匹配中产生最大匹配。定理20。

扫码加我拉你入群

请注明：姓名-公司-职位

以便审核进群资格，未注明则拒绝

2022-6-24 09:55:55

UM\\u is\\u Maximum\\u Uniform（B：列表出价）（A：列表询问）：排序B->排序A-> M：列表填充类型，Is\\u uniform M->| M |≤ | （UM B A）|证明：设M是出价B和询问A列表上的任意IR和一致匹配，其中每个匹配的出价-询问对以价格t进行交易。我们需要证明M≤|（UM B A）|其中m是匹配m中匹配的买卖对的数量。观察到在任何单独的理性和统一匹配中，高于交易价格的出价数量与低于交易价格的出价数量相同（见图9）。因此，在B和A中，t上方至少有m个投标，t下方至少有m个要求。二十： 12金融市场交易的正式验证ABA（a）U M（b）M M图8（a）虚线表示函数PRODUCT\\U M生成的所有买卖对。在每个迭代函数中，PRODUCT\\U UM将B中的最大可用出价与A中的最小可用ask进行匹配。（B）此处的虚线表示出价列表和ask列表A的最大匹配。请注意，在这种情况下，UM生成的匹配不是最大匹配。]]][[[[M]]]]]]][[[[[[[【B/a图9中匹配M的交易价格p用一个点表示，该点位于带限价90的询价和带限价91的报价之间。请注意，由于M是单独合理的，因此低于交易价格p的匹配询价数量与高于交易价格p的匹配报价数量相同。因为在每一步中，函数produce\\UM都会将B中可用的最大报价与最小的询价可用数量配对ble在A中必须至少生成m个bid ask对。因此，对于B的列表和ask的列表，函数UM生成一个大小至少为m的统一匹配。4结论当今金融市场的交易活动主要是通过计算机算法实现的。这些算法非常庞大和复杂。

扫码加我拉你入群

请注明：姓名-公司-职位

以便审核进群资格，未注明则拒绝

mingdashike22

2022-6-24 09:55:58

交易所（场馆）使用的匹配算法是这一广泛金融算法的核心【15】。为了确保市场的安全性和完整性，市场监管机构引入了指南，规定了这些算法的不同特征。传统的以测试为中心的软件开发方法不能保证这些软件符合指导原则。在这项工作中，我们开发了一个正式的框架来验证Exchange使用的匹配算法的一些重要属性。这些算法使用双边拍卖，在不同的交易时段将多个买家与多个卖家进行匹配。我们使用独立类型的Coq证明助手来简明地表示拍卖理论中与这些算法验证相关的各种概念。在此框架下，我们正式验证了双边拍卖的两个重要类别（统一价格和动态价格）。在这项工作中，我们将每个出价或要求定义为交易单个产品单元的请求，并且产品是不可分割的。未来，通过引入适当的函数，从多个单位的买卖请求中生成单个单位的买卖请求，这项工作可以扩展到适应涉及一个项目多个单位的交易。另一个有趣的工作方向是将此工作扩展到连续市场中不同类型的订单（如限价订单、市场订单、止损订单、冰山订单等）。这需要根据这些订单的各种属性维护优先级队列。Sarswat和A.K.Singh XX:13对交易所交易的验证将提供一个正式的基础，可用于其他金融算法的严格分析（例如。

扫码加我拉你入群

请注明：姓名-公司-职位

以便审核进群资格，未注明则拒绝

2022-6-24 09:56:01

订单发送、清算和结算TC）。References1 SEC因纽约证券交易所屡次未能按照交易所规则运作而向其收取费用。2纽约证券交易所因多次违规支付1400万美元罚款。NSE共定位问题为3级。4 Coq拍卖形式化。https://github.com/suneel-sarswat/auction.5Coq标准库。https://coq.inria.fr/library/.6Marco B.Caminati、Manfred Kerber、Christoph Lange 0002和Colin Rowat。声音拍卖规范和实施。《第十六届ACM经济与计算会议论文集》，编辑Tim Rawgarden、Michal Feldman和Michael Schwarz，EC’15，波特兰，或美国，2015年6月15-19日，第547-564页。ACM，2015.7丹尼尔·弗里德曼。双重拍卖市场制度：一项调查。《双重拍卖市场：制度、理论和证据》，14:3–251993.8托马斯·亨辛格、兰吉特·贾拉、鲁帕克·马朱姆达尔和格雷戈伊尔·萨特尔。使用blast进行软件验证。在软件模型检查国际SPIN研讨会上，第235–239页。Springer，2003.9 J.R.Burch、E.M.Clarke和K.L.McMillan。使用符号模型检查进行时序电路验证。在第27届设计自动化会议上，第46–51页，1990.10格温·克莱因、凯文·埃尔芬斯通、格诺特·海泽、琼·安德罗尼克、大卫·科克、菲利普·德林、达米卡·埃尔卡杜威、凯·恩格尔哈特、拉法·科兰斯基、迈克尔·诺里斯等。sel4：操作系统内核的正式验证。ACM SIGOPS第22届操作系统原理研讨会论文集，第207-220页。ACM，2009.11 Christoph Lange、Marco B Caminati、Manfred Kerber、Till Mossakowski、Colin Rowat、Makarius Wenzel和Wolfgang Windsteiger。四个定理证明器对基本拍卖理论适用性的定性比较。智能计算机数学国际会议，第200–215页。斯普林格，2013.12泽维尔·勒罗伊。正式验证的编译器后端。

扫码加我拉你入群

请注明：姓名-公司-职位

以便审核进群资格，未注明则拒绝