多语言等式逻辑和范畴语义理论研究

可在www.sciencedirect.com在线获取理论计算机科学电子笔记352（2020）79-103www.elsevier.com/locate/entcs多语言的等式逻辑和范畴语义Samuele Buroa和Roy Croleb和Isabella Mastroenia1，2，3a意大利维罗纳大学和b英国莱斯特大学摘要编程语言互操作性是两种编程语言作为单个系统的一部分进行交互的能力每种语言都可以针对特定任务进行优化，程序员可以利用这一点。HTML、CSS和JavaScript产生了一种互操作性，它们协同工作以呈现网页。一些面向对象的语言通过虚拟机主机具有互操作性（公共语言中的.NET CLI兼容语言，以及Java虚拟机中的JVM兼容语言高级语言可以与低级语言（Apple的Swift和Java-C）进行交互虽然已经有一些研究探索互操作性机制（第1节），但理论基础的发展很少。本文提出了一种基于等式逻辑和范畴语义理论的互操作性方法。我们给出了两种语言可以混合的方式，以及使用混合语言的方程的互操作性。形式上，多语言等式逻辑被定义为从一组公理开始推导有效的等式，这些公理假设了组合语言的属性。因此，我们有一个多语言理论的概念，本文的大部分内容都致力于探索这些理论的性质。这是通过范畴论来实现的，它给了我们一个非常通用和灵活的语义，因此是一个很好的模型集合。分类范畴被构造，因此等式理论为每个范畴模型提供了一种内部语言;由此我们也可以建立可靠性和完备性。一个集合论语义学作为一个例子，它本身是健全和完整的。 范畴语义学是基于一些预先存在的研究，但我们给出了一个介绍，我们觉得更容易和更简单的工作，改善和温和地扩展当前的研究，特别是非常适合计算机科学家。在整个文件中，我们证明了一些有趣的性质的新的语义机器。 我们提供了一个小的运行示例来说明我们的想法，一个更复杂的例子。关键词：分类逻辑，等式逻辑，互操作性，多语言，排序签名和理论，编程语言，子排序多态。1介绍方程代数的理论一直是一个引人注目的话题，因为早期的普遍代数[33，2]。关于等式逻辑的研究，解决了关于项相等的演绎推理问题，已经很丰富了（见[34，17]）。1电子邮件：samuele. univr.it2电子邮件：rlc3@le.ac.uk3电子邮件：isabella. univr.ithttps://doi.org/10.1016/j.entcs.2020.09.0051571-0661/© 2020作者。出版社：Elsevier B.V.这是一篇基于CC BY-NC-ND许可证的开放获取文章（http://creativecommons.org/licenses/by-nc-nd/4.0/）。80S. Buro等人/理论计算机科学电子笔记352（2020）79调查）。特别是出现了许多健全完备的演绎体系。例如，如果Sg是一个单排序、多排序或顺序排序的签名（排序和函数符号），则这些系统分别出现在[2]、[10]和[13]中。这些发展对操作语义学和自动定理证明产生了显著的影响。特别是，[8，18]的开创性工作使等式演绎可操作化，导致了项重写系统理论[15，35]，该理论具有广泛的应用。多语言是从现有语言的组合中产生的编程语言[27，1，32，9，14，26，24，21]。直观地说，多语言的术语是通过执行跨语言替换来获得的。例如，[21]中设计的多语言允许程序员用Scheme表达式替换ML潜在的好处是代码重用和软件互操作性。为了提供语义，[21]引入了新的构造来调节底层语言之间的值的流动，即所谓的边界函数。但是多语言的形式属性和语义是什么呢？事实上，我们能有多普遍在任何情况下，什么是一个好的正式定义的多语言摆在首位？Buro和Mastroeni[4]将[21]的方法扩展到更广泛的有序代数类，提供了一种系统和更一般的方法来定义多语言，但他们没有解决等式推理。我们在这里就是这样做的更详细地说，通过组合两个顺序排序的签名Sg1和Sg2来指定多语言。但是，这些签名究竟应该如何组合呢？什么是术语互操作性的形式方程理论？更确切地说，由于方程不仅定义在两个都在Sgi之一上的项之间，而且定义在包含Sg1和Sg2的符号的项之间，对于这样的多语言方程，什么是好的演绎系统？我们解决这些问题，指定多语言的方程逻辑，这是健全的和完整的。详细贡献：从概念上讲，我们将序排序方程逻辑的基本句法理论[13]和理论模型提升到[4]定义的代数多语言框架。[13]中的模型是从集合中构建的，但我们采用了[20]中的分类方法。 主要贡献是一个多语言的演绎系统，具有健全和完整的范畴语义。 我们还证明了一些有趣的语义属性。本文中有一个运行的示例应用程序，在第3.3节中有一个更详细的应用程序的概述，我们将命令式语言和lambda演算结合起来。我们对有序方程理论的解释建立在[20]的基础上并加以完善，我们所有的演绎系统都有统一而清晰的归纳规则。此外，我们在等式判断中包括显式类型信息，并包括可能是条件方程我们给出了一个简化的范畴语义以及范畴类型论对应和分类范畴，并给出了一个与自由集代数语义的显式联系备注和直觉：我们使用有序签名[13]。因此，我们的语言享受子排序多态性;没有参数化的规定。S. Buro等人/理论计算机科学电子笔记352（2020）7981多态这样的签名可以满足被称为单调性和规律性的标准。由于这些准则的直观性通常在技术论文中被省略，我们做了一些评论。语言术语t是通过将函数符号f应用于现有术语（以常量开始）而归纳建立的。这样的符号f可以被多态地排序。因此，如果f的一个输入排序是另一个输入排序的子排序，我们希望项t相对于输出排序是多态的。单调性将这一要求形式化。我们需要对这种多态性进行一些控制：一种方法是应用一个要求，即每个项t都有一个最小排序。[13]这是一个很好的例子。为了确保每个项tto都有一个最小排序，我们可能会天真地要求每个子排序多态函数符号f都有一个最小输入和最小输出排序，希望t能归纳地做到这一点。我们需要给所有常数一个最小排序来开始归纳;我们可以简单地规定每个常数只有一个排序。 在最初的构建术语中，如果有任何函数符号f的（多态）输入排序是常数排序的严格子排序，则f不能应用于该常数。我们被引导去完善我们天真的想法：固定任何f。只考虑这个f可以多态应用的那些常数。现在固定一个这样的排序为s的常数;这为f的输入排序施加了一个下界，即s。然后我们要求对于f的所有这样的多态实例，有一个实例具有最小输入排序s，当然s≤s，和最小输出排序。这种形式化的要求就是规则性。论文结构：在第2节中，我们提出了一个透明的规则为基础的演绎系统的顺序排序方程逻辑与条件公理，连同一个范畴语义，这是证明的声音和完整的。在第3节中，我们提出了一组类似的结果，多语言。在第4节中，我们给出了多语言的一些进一步的在3.3节中，我们给出了一个扩展示例的概要，其中传统的lambda演算和命令式while语言混合为一种多语言。2序分类方程逻辑我们回顾序排序方程理论（例如见[13，20]）。在这里，我们给出了一个改进的介绍，是语法上比在上述简单，我们进一步扩展理论，包括条件方程公理。我们还对[20]中的分类模型进行了详细但风格上改进的总结，以及分类类别的更简单构造（直到等价）。然后，我们证明了一个结果有关的分类范畴的自由序排序代数。2.1序排序代数一个集合S通常被认为是一个类的集合或一个地类型的集合。通常S被≤偏序，然后SnS×· · · ×S（n-次卡鲁奇积，n≥1）继承了点态序，典型的例子记为w≤WJ。如果w∈Sn，我们通常通过写ws1，...，s n，有时指排序的序列。82S. Buro等人/理论计算机科学电子笔记352（2020）791nJ我们写（A s|s∈S），其中每个A s有时是一个集合，但更一般地是范畴C中的一个对象。我们有时把这个族称为S-排序的集合（或S-排序的对象）.这样的指标族是简单的函子A在预层范畴SetS（CS）中。因此，一个S-排序的函数（S-排序态射）h：A→B只是SetS（CS）中的态射（即自然变换），其中S是一个集合或偏序集。在本文中，所有范畴都有有限积，函子保持它们直到同构。如果A、B和Ai（1≤i≤n）是范畴C中的对象，我们写A×B表示A和B的二进制积，A1×· ·· ×An或Ai表示Ai的有限积，1表示终结对象。二元积的中介态射记为，通常的f×fJ（对于适当的f和f以及通常的投影）。我们对有限积采用了明显的扩展表示法如果A是一个S-排序的对象，并且w是1，...，s n，我们用Aw表示乘积As1 ×···× Asn。同样，如果f是S-排序态射，则态射f w定义为fs1×···×fsn。A和B的余积对象记为A+B。我们写l1…ln或l1，...，l n为一个典型的有限列表，我们可以只L.在s1，.的特殊情况下，s n我们通常用w表示。 当我们定义顺序排序的签名Sg1，Sg2，Sg，Sgj等时，我们将隐式地假定它们的偏序集的排序记为（S1，≤1），（S2，≤2），（S1，≤），（SJ，≤J）等，分别序分类方程理论的关键要素是签名和代数的定义。前者定义了语言术语赖以建立的符号，后者为术语提供了意义。这个意义既可以是集合论的，也可以是范畴论的[13，20]。定义2.1（有序排序签名）有序排序签名Sg由下式指定：• 一类偏序集（S，≤）;• 函数符号的集合f：s1，.， s a→ s，每个a ≥ 1，（w，s）∈Sa×S是f的秩，其中ws1，...，sa;• 常数k：s的集合，每个常数具有唯一的秩s（仅单个排序）;以及• 一个单调性要求，即当f：w1→s和f：w2→r，w1≤w2，则s≤ r。我们所说的运算符是指一个函数符号或一个常数。与多态性相关的这种签名Sg的关键属性是规则性。我们将很快展示如何从Sg中构建一组项，正则性确保每个项都有唯一的最小排序[13，命题2.10]。(All本文中的签名被假定为规则的）。定义2.2（有序排序签名的正则性）有序排序签名Sg是正则的，如果对于每个f：w→s和对于每个下界w l≤w，集合{（wJ，sJ）|f：WJ→ sj<$wl≤ WJ}<$Sn× S有一个极小值，称为f关于wl的最小秩。S. Buro等人/理论计算机科学电子笔记352（2020）7983−r，x：s，rJ<$x：s−（k：s）Γk：s（Fn） （α 1≤i≤a）Γαti：si（f：s，.，S→s）r：s（s≤r）1ar ∈f（t1，.，t a）：s联系我们Fig. 1.由有序签名Sg生成的已证明项。签名Sg上的原始项由t：：= x定义|K|f（t1，.，t a），其中x ∈ Var（变量的可数无限集合），k是常数，f是元数为a的函数符号。上下文是由变量x和Sg中的排序s形成的有序对x：s的有限列表。我们通常通过写Γ [x1：s1，.，x n：s n]。我们将Γ和ΓJ的上下文级联表示为Γ， ΓJ。我们处理形式为Γt：s的排序判断。 由排序规则生成的在图1中，被称为证明项。注意，一个项t可以有不止一个类s，其中Γt：s是一个已证明项。然而，总是有一个唯一的最小排序。引理2.3（项具有最小排序）假设Γ是上下文，t是给定正则签名Th的原始项。 如果有任何类s，其中Γ t：s是一个被证明的项，那么有一个最小的这样的类，st。证据一种是使用规则归纳法。这个证明很容易，尽管在文献中，一个关键的步骤经常被省略。通过归纳，对于规则Fn，人们很容易使用正则性来获得一个排序，例如，使得Γf（t1， . ，ta）：s。 N_w_s_n是f（t1， . ，ta）。大多数作者说，这种类型的时间最少。这是真的，但证明这一点需要一个单独的（尽管微不足道的）规则归纳。Q我们用t[u/x]表示原始项u对t中变量x的替换，用t[u/x]表示原始项u u1，.，对于变量x x1，.， x n.定义2.4（包含结构和FPI范畴）范畴C中的包含结构I由C的子集（子范畴）I指定，使得• 对于C的任意两个对象A和B，如果存在I中的唯一态射A>B，则A> B是 C中的幺半群;• 对于C中的任何对象A，身份idA在I中（因此I是一个LU子类：它与C具有相同的对象）;• 如果ι1：A1>B1和ι2：A2>B2是I中的态射，那么To是ι1×ι2：A1×A2> B1×B2。一个对（C，I）称为FPI范畴。直觉上，产品模型是排序列表，而包含模型是子排序多态。因此，FPI范畴可以用作签名的代数定义的基础，即定义2.5（序排序代数）给定一个序排序签名Sg，一个FPI范畴（C，I）中的Sg-代数A被指定为：84S. Buro等人/理论计算机科学电子笔记352（2020）79（k）A（k）B分s≤s） idA分s）（）（）（）（）（2）（Ⅲ）（）（）（）（Ⅲ）（Ⅲ）• C中的对象sA对于每个排序s，以及对象wAs1A× ···×s nA对于每个ws1，.，Sn∈ Sn;• 态射f：w→sA： WA→ sA和kA：1 → 对于每个f：w→s，sA和k：s;和• 在I中的态射<$s≤r）A：<$s）A><$r）A，对于S中的每个s≤r，其中我们设置使得如果函数符号f在Sg中以多于一个秩f：w1→ s和f：w2→r出现，其中s1，.，saw1≤w2r1，.，ra，则下图为commutes：1）A × ··· ×<$sa）A<$f：w1→s）A（s）A<$s1≤r1）A×···×<$sa≤ra）A<$s≤r）A1）A × ··· ×<$ra）A<$f：w2→r）A（r）A从现在开始，只要上下文清楚，我们就删除语义括号定义2.6（序排序同态）设Sg是序排序符号，A和B是Sg-代数。 Sg-同态h：A → B是S-排序态射（hs：sA→sB|s∈S），使得给定f：s1，...，s a→s，k：s，且s≤r在Sg中，以下图可交换：1）A × ··· ×<$sa）Af）A（s）A1分s）Ahs1×···×hsahs hs（1）B ×···×<$sa）B（f）B（s）ASB（1）A （r）A（s）BHS（s）B<$s≤r）Bhr（r）B我们定义hwh s1 ×···×h sa 条件是ws1，...， ×s a.给定一个序排序的签名Sg，所有序排序的Sg-代数的类和所有序排序的Sg-同态的类构成一个范畴，记为OSAlg（C，I）Sg.若Γ [x1：s1，.，]是正则签名Sg中的一个已证项，xn：s n]，任何Sg-代数A从 ΓAs1A× · ··× s nA到sAin C，根据图2中的归纳定义。我们将这样的箭头表示为Γt：sA，并将其称为Γt：s的语义。由于在一个给定的上下文中，术语可以被赋予不同的类型，我们应该考虑图2中S. Buro等人/理论计算机科学电子笔记352（2020）7985的定义是否合理。因此，我们有以下引理，其中可以看到，给出了术语替换的语义86S. Buro等人/理论计算机科学电子笔记352（2020）79−（k：s）<$r =<$s≤r）<$m：<$r）→<$s）→<$r）（2）（）（）（）（））（）（α=1−<$r，x：s，<$j <$x：s）π：<$r）×<$s）× <$<$rJ）→<$s）（k：s）（k）<$r）→1 →<$s）（1≤i≤a）<$ti：si）m i：<$r）→ <$s i）（f：s，.，S1一1一1我→s）f（t，.，t）：s）（f）m，.，m：<$r）→（a<$s））→<$s）1a<$rt：s）=m：<$r）→<$s）（s≤r）图二、证明项的范畴语义像往常一样，通过态射合成：引理2.7（良定语义学）给定一个已证明的项Γt：s和一个代数A：• 语义态射Γt：s是唯一的;也就是说，这是一个完整的功能。• 代数在posetal范畴诱导函子（S，≤）→Is≤sJ<$s≤sJ）：<$s）><$sJ），因此语义可以是通过态射Γt：st分解，也就是说，Γt：s=st≤s 我的天• 令r [x1：s1，.，x n：s n]。如果我们已经证明了项Γ t：s和Γ ju i：s i，其中1≤i≤n，则Γ jt [u/x]：s和Γ jt [u/x]：s=Γt：sΓ ju1：s1，.，Γ J►u n：s n⟩.证明项之间的方程仅针对相干签名定义。为了定义相干性，首先让是≤的对称和传递闭包。由S上的S诱导的等价类是（S，≤）的连通分支;并且（S，≤）是局部过滤的，如果对于同一连通分支中的每两个排序SJ和SJJ，存在一个排序s使得SJ，SJJ≤s。然后，签名Sg被称为是一致的，当且仅当它是正则的和局部滤波的。直觉是，如果SJ和SJJ有一个“共同的超排序”s，它们就可能被判断为相等定义2.8（排序方程和满足）设Sg是相干签名。Sg中的等式（在上下文中）由T t =tJ：s表示，其中• 存在SJ，SJJ类使得Γt：SJ和ΓTJ：SJJ是Sg中的已证明项•SJ和SJJ落在（S，≤）的相同连通分量中;并且• s是SJ和SJJ的公共超类（它由相干条件存在Sg中的条件方程（在上下文中）是m+ 1个在上下文中的方程的列表。上下文（其中m≥1）可表示为mΓtα=tJα：sα=Γt=S. Buro等人/理论计算机科学电子笔记352（2020）7987（2）（）（）1设Γ[x1：s′1， . ，xn：s′n]是（AxSub）和（AxCSub）中的一个函数.Γt =tJ：s∈Ax（1≤i≤n）Γjui：sJi（AxSub）rjt [u/x] =tJ[u/x]：sM Γtα=tJα：sα= Γt=tJ：s∈Ax（1≤i≤n）Γjui：sJi（AxCSub）（α1≤α≤m）ΓJ<$tα[u/x]=tJα[u/x]：sαrjt [u/x] =tJ[u/x]：s（Ref）联系我们rt=t：s（Sym）t=tJ：sT=t：s（翻译）rt=tJ：srtJ=tJJ：srt =tJJ：s（子排序） t=tJ：s（s≤r）rt：s（1≤i≤Γn) Γ t=tJ：r► ui=uJi：si（丛）Γjt [u/x] =t[uS/x]：s（Γ[x1：s1，.，x n：s n]）图三. 由序分类理论Th（Sg，Ax）产生的定理。tJ：s.我们说一个代数A满足一个方程，如果r t：s = rtJ：s。我们说一个代数A满足一个条件方程，如果对所有态射u：U→ Γ，Γt α：s αu = ΓtJα：s αu蕴涵了Γt：su =ΓtJ：s u。我们定义一个序排序理论Th（Sg，Ax）为一对， 签名Sg和一组公理Ax。每个公理要么是一个方程，要么是一个条件方程。理论Th的定理是由图3中的等式逻辑规则生成的那些等式。引理2.9（广义代换）下面的规则是可接受的常规规则归纳（子）Γt=tJ：s（1≤i≤n）Γjui：si（Γ[x：s，...，X：s]）rjt [u/x] =tJ[u/x]：s1 1n n设Th（Sg，Ax）是一个有序理论.如果一个Sg-代数A满足Ax中的所有公理，我们称A为Th的模型。模型范畴OSMod（C，I）Th是由Th在（C，I）中的所有模型给出的OSAlg（C，I）Sg引理2.10（满意度是良好定义的）作为引理2.7的结果，满意度是良好定义的，直到子类多态相等，如下：假设我们在模型A中有一个定理t=tJ：ssatisfiedd。 如果rt=tJ：s也是一个定理，那么它也是满足的。是的。最小类st和st′的存在性意味着s和st是连通的，因此有一个超型SJ。因此，每一项都有这种类型的SJ，并且通过使用引理2.7的因式分解和左消去性质，拉吉88S. Buro等人/理论计算机科学电子笔记352（2020）79monomorphisms。Q范畴Pres×，>（（C，I），（D，J））是由两个保有限积的函子F：C → D定义的，且F限制于一个函子F|I：I→J（即monics也被保留）。 假设我们有一个模型A在OSMod（C，I）Th.然后在OSMod（D，J）Th中有一个模型FA，粗略地说，定义为并应用F同样，我们可以“将F应用于模型的同态”，这个过程（这在范畴类型论/逻辑中是绝对标准的;例如参见[6，16]）导致函子ApA：Pres×，>（（C，I），（D，J））→OSMod（D，J）Th。理论Th的分类范畴Cl（Th）是一个FPI范畴，使得存在范畴等价ApG：Pres×，>（Cl（Th），（D，J））OSMod（D，J）Th因此Th在（D，J）中的模型对应于具有源Cl（Th）的这种结构保持函子。定理2.11（分类范畴的存在性）存在一个由Th的句法构造的FPI-范畴Cl（Th），其中存在Th的一般模型，其性质是态射的相等性对应于项方程的可导性。在抽象层次上，这个概念是范畴类型理论/逻辑中的标准;例如参见[6，16]。我们觉得我们的具体结构比[20]中发现的更简单，并认为这是一个小小的贡献。这样的存在性证明是出了名的棘手得到完全正确的，并有显着的错误，在文献中。我们使用匹配上下文和置换不变性[7，29]来替换重命名变量的常见替换，我们认为这使得我们的证明更容易陈述和证明（因此更不容易出错）。证据设Var是一个（可数的）固定的变量集合{V1，V2，. . }中。我们称上下文为Γs[V1：s1，.，V n：s n]）任何排序s1，.的主上下文，s n.一般来说，下面的元变量x，y，z等，可能有下标，范围在Var。因此，r[x1：s1，...，x n：s n]是一个典型的上下文，我们说，任何这样的上下文匹配S1，...，s n.首先我们定义FOSAlg的对象T（Γ）。当然T（Γ）必须是一个S-序集，并且其组成部分是等价类的集合T（Γ）s项（Γ）s/n，其中项（Γ）s{ t}个|（T：s in Th）其中，我们定义等价关系ttJ，以防我们可以导出Γt =tJ：s在Th中，对于典型的等价类，写[t令Γ和ΓJ满足chs1， . ，Sn和SJ1， . ，sJmres pecti vel y.态射h：T（Γ）→T（ΓJ）必须是S-排序函数（ hs：T（Γ） s→T（Γ J） s|s∈S）。这些由列表h s{rJ}t1，.，t n}，其中t i∈Term（Γ J）si，其中hs（[t]∈T（r）s）[t[t1， . ，tm/x1， . ，xm] ]∈T（ΓJ）sS. Buro等人/理论计算机科学电子笔记352（2020）7989（Ⅲ）JJJ所以我们有（Γ |t）=（r |t），当r =t：s时，是一个定理Q很容易检查，这是很好的定义。注意如果h{r}=1， . .. ，tJm我们有这样的定义：}：T（rJ）→T（rJJ）{r j J}t1[tJ1， . ，tJm/x1， . ，xm]， . ，tn[tJ1， . ，tJm/x1， . ，xm]}这是繁琐的，但例行的验证，这产生了一个类别，关键是依赖于替代规则的方程推导。Q定理2.12（可靠性和完备性）设Th是序分类理论。Γ t = tJ：s是Th的一个定理当且仅当Th的每个模型都满足Γ t = tJ：s。证据合理性遵循图3的规则归纳。 为了完整性，假设在任何模型中都满足Γ t = tJ：s。然后，特别地，它在分类范畴Cl（Th）中的类属模型G因此，我们有<$rt：s）G=我们用一个新的结果来结束这一节，尽管它是由类似的定理[28]激发的。该证明还使用了匹配上下文和变量的排列。定理2.13（与自由代数的关系）在FPI范畴Cl（Th）和（FOSAlg op，J）之间存在等价性，其中FOSAlg是有限变量集上的自由序代数范畴，和序同态范畴。此外，还通过FPI函子Φ：Cl（Th）（FOSAlg op，J）给出了等价性.证据为了证明（FOSAlgop，J）是一个FPI范畴，我们将证明FOSAlgis有有限个余积，然后定义J。给定对象T（r）和T（rJ），则二元余积对象由T（Δ rs，rs）给出，其中排序分别匹配r和rJ。余积插入由{Δ vv1，...，v n}和{Δv n+1，.，vn+ m}。给定态射I， . ，tn}：T（r）→T（rJJ）and{jJjjtJ1， . ，tJm}：T（rJ）→T（rJJ）则中介态射是{ΓJ∈t1， . ，tn，tJ1， . ，tJm}。 注意T（k）是初始对象。假设对于每个1≤i≤n，si≤ri。 然后有一个史诗态射i{r sx1，.，xn}：T（Γ r）→T（Γ s）;很容易证明这是一个满态，因此在FOSAlg op中产生一个单态。Luc子范畴J的所有态射都是单态射iop{r sx1，.，xn}：T（Γ s）→T（Γ r）。 这当然是一个包容性的范畴。90S. Buro等人/理论计算机科学电子笔记352（2020）79现在我们证明等价性。我们定义一个函子Φ：Cl（Th）→（FOSAlgop，J）如下。 给定一个态射（Γ |t1）. （Γ |t m）：s → r，则Φ将此发送到{r sπt1，...，πt m}： T（r）→T（s）其中置换π由π：xi→Vi指定。我们检查这是很好的定义。假设（Γ|t1）. （Γ|t m）=（Γ J|tJ1）. （Γ|tJm）。我们得检查一下{r sπt1，...，πt m}Φ（Γ|t1）. （Γ|（t m））=Φ（（rJ|tJ1）. . . （Γ|tJm））{rsπJtJ1， . ，πJtJm}根据定义，我们有：Γt j= ρtJj：r j，其中ρ由ρ：xJi→x i指定。我们可以用方程的替换规则推导出，π Γ <$πt j= π（ρtJj）：r j，这正是所需要的，因为πJ= π <$ρ。我们认为，置换的使用，虽然等同于通过替换使用同时变量重命名，但通过使用置换不变的判断，提高了可读性，更重要的是简化了计算。（Φ本质上是满射）：对于Cl（Th）中的任何对象s，我们有Φ（s）=T（Γs）。但我们很容易证明，对于任意的T（Γ），其中Γmatchess，我们有一个T（Γ）n=T（Γs），其中逆同态（Φ是忠实的）：让Φ（Γ|t1）. （Γ|t m））= Φ（（r J|tJ1）. （Γ|tJm））。我们需要检查一下，Γ t j= ρtJj：r j。 假设我们有{rsπt1， . ，πtm}={rsπJtJ1， . ，πJtJm}因此，Γs<$πtj =πtJj：rj。因此，我们可以推导出：Γ<$tj =（π−1<$πJ）tJj：rj;由于π−1<$πJ=ρ，我们就完成了。（Φ是满的）：令{s}1，.，t m}：Φ（r）= T（r）→ Φ（s）= T（r s）则（r s|t1，...，t m）是适当的Cl（Th）态射。（Φ是P rs×的对象，>（Cl（Th），（FOSAlgop，J））：我们需要检查Φ，|I：I→J其中I是Cl（Th）的包含范畴。设s≤r。 注意，Φ（r|x1）. （Γ |xn）：s →r）是单态映射{Γ s<$x1，.， x n}：Γ r→ Γ sQ3多语言等式逻辑3.1多语言基础在这一节中，我们经常引用下面介绍并随后扩展的运行示例，以说明该理论如何在具体环境S. Buro等人/理论计算机科学电子笔记352（2020）7991在Char中跟随c（假设标准的字母顺序）。0：nat零常数s：nat→nat后继函数+：nat，nat→nat加法运算符(a) Sg1操作员。（c∈Char）c：chr特征常数下一个：chr→chr下一个字符函数+：str，str→str字符串连接(b) Sg2操作员。图四、 排序签名Sg 1和Sg 2的运算符。(see第3.3节介绍了一个更复杂的例子）。运行示例。我们的例子是使用以下顺序排序的签名定义的：• 签名Sg1定义了一种语言的符号，用于在皮亚诺符号中构造自然数的简单数学表达式设Sg1的排序偏序集（S1，≤1）是一个具有单一排序nat的偏序集，表示自然数的类型，其算子为图4a中的算子.• 设c∈Char{a，b，...，z}是在有限集合Char上的元变量人物。签名Sg2定义了一种在Char上构建字符串的语言。Sg 2的排序集合S2携带字符串的排序str和排序chr对于角色来说。 子排序关系≤2是S2+上的自反关系chr ≤2str（即字符是一个符号串），Sg 2中的运算符符号出现在图4b中。我们通过（Set，Incl）中的序排序代数A1和A2（见图5）对Sg1和Sg2进行建模，（S et，I ncl）是具有形成包含的包含函数的集合的FPI范畴结构在next的定义中，符号cJ表示（1）A2注3.1即将出现的定义和结果逐渐定义和说明了多语言，并给出了多语言和有序语言之间的关系。多语言签名3.2被指定为两个顺序排序的签名（如运行示例中所示）以及两个签名之间的互操作性关系这就决定了多语言的术语。请注意，这种关系不是底层签名的普适属性;还请注意，多语言签名显式地为用户提供了原始的两种语言规范。 我们在3.3节中展示了关于签名类别的一些很好的概念，包括顺序排序的和多语言的。我们还将看到，我们可以展示一个函子，它将一个多语言签名映射到一个顺序排序的签名（相关签名3.4），将两个原始签名混合成一个。在定义了多语言代数3.5和同态3.6之后，定理3.7将通过相关的签名提供多92S. Buro等人/理论计算机科学电子笔记352（2020）79CHR）CharA2（Ⅲ）（Ⅲ）（Ⅲ）（Ⅲ）我（1）A（1）A1 （n1，n2）›→n1+n2：N2→N2 （s1，s2）›→s1s2：（Char）2→Charsi对于元素ii（s）∈S1+S2，其中ii（s）（s，i）∈S1×{1}<$S2×{ 2}排序natA1N字符串A2Char操作员0A10：1 →N（s）A1n›→n+ 1：N→N（c∈Char）cA2›→c：1 →Char下一页）A2c<$→cJ：Char →Char亚类<$chr≤2str）A2c›→c：Char →Char图五、 Sg 1和Sg 2的范畴语义。和排序语言。特别是，它建议如何使用相关的签名给出（多语言）术语，方程和满意度的定义。然后，我们就可以用等式来推理这两种给定语言的互操作性这将我们带到3.2节，在那里我们详细研究了等式推理为了定义多语言签名，我们引入了一些关键的符号。我们用+表示两个集合的不相交并集：在集合范畴中形成余积的插入态射是单射函数，因此它们有左逆（并且有一个不相交并的模型）。在下文中，如果S1和S2是两个排序集，并且s∈Si，其中i1， 2，我们写因此，在关系sisjj中，我们有s∈Si和SJ∈Sj。这是一个非常有用的符号，但可能需要在第一次阅读时小心。此外，如果w为1，... s n∈Sn，则对于（s1）i，.， （s n）i.定义3.2（多语言签名）A多语言签名SG（Sg1，Sg2，）是• 一对序排序签名Sg1和Sg2具有排序偏序集（S1，≤1），（S2，≤2）;和• 在S1+S2上的一个（二元）关系连接，使得sisJj，i，j∈ {1， 2}，i ≤= j。其思想是，如果sisJj，并且Γt：s是一种语言中的已证明项，则t可以用来代替项tJ，使得在另一种语言中ΓjtJ：sJ：如[21]中所述，这是精确的，S. Buro等人/理论计算机科学电子笔记352（2020）79931适时定义3.3OSSg是有序排序签名的范畴，其形态为h：Sg1→Sg2，由下式给出：• 单调函数h：（S1，≤1）→（S2，≤2）（这里我们记为h（w））h（s1），.，h（s n）for ws1，...，s n∈Sn），且• 从Sg 1中的算子到Sg 2中的算子的保持秩的映射h：给定Sg 1中的k：s，则Sg 1中的h（k）：h（s）;给定Sg 1中的f：w→s，则Sg 2中的h（f）：h（w）→h（s）。此外，我们用MLSg表示多语言签名的范畴其中一个态射H（h1，h2）：（Sg1，Sg2，）→（SgJ1，SgJ2，J）由OSSg中的两个态射h1：Sg 1 → Sg J1和h2：Sg 2→ Sg J2定义，使得它们保持连接关系，即（Sg1，Sg 2，）中的s i s j在（Sg j 1，Sg j 2，j）中蕴涵（hi（s）iJ（hj（sJ））j.定义3.4（关联签名）设SG（Sg1，Sg2，）为多语言签名. SG的关联签名SG是如下定义的顺序排序的签名：• 类的偏序集由（S1+S2，≤）给出，其中si≤rj，如果i=j且s≤ir;• 若f：w→s是SGi中的算子，对i1， 2，则fi：wi→si是SG中的函数符号;• 如果k：s是Sg i中的常数，对于某些i1， 2，则ki：si是SG中的常数;并且• 转换操作符<$→si，s′j：si→SJj，对于每个const r aintsisjj。关联的签名函子（−）：MLSg→ OSSg将每个多语言签名SG（Sg1，Sg2，）映射到其关联的签名SG，并且将每个多语言签名态射H：SG→SGJ映射到由H（si）（hi（s））i对于每个s∈Si（因此si∈S1+S2）和H（fi）（hi（f））i对于每个f∈Sgi（因此fi在SG中）给出的顺序排序的签名态射H：SG→SGJ运行示例。（ -）将多语言签名SG嵌入到OSSg中，提供多语言的顺序排序版本SG。SG生成Sgi项（参见第3.2节）以及涉及转换运算符的混合多语言项，如chas[c：chr2， n：nat1]n+1（<$→chr2，nat1 （c），n） ：nat1。从现在开始，我们在示例中使用颜色来消除左包含和右包含的代替下标1和2。此外，只要操作符适合这样做，我们就使用一个整数表示法。也就是说，前一项由[c：chr，n：nat]表示。这样的函子概述了将多语言签名嵌入到有序签名中，使我们能够将多语言视为普通语言。94S. Buro等人/理论计算机科学电子笔记352（2020）79（）（）（）J）jJstr）（n）chr（n）;andd2A（1）（Ⅲ）（）（）（）¢事实上，很容易看出（−）既是对象上的内射，也是忠实的函子。定义3.5（多语言代数）令SG（Sg1，Sg2，）是多语言签名。FPI范畴（C，I）中的SG -代数A由下式给出：• Sg1和Sg2上（C，I）中的一对序排序代数A1和A2;• 边界态射sJjA：sAi→ sJAjinCfor each constraintsisJj。一个代数阐述了多语言的含义：底层语言的含义，以及排序s∈Si的项如何被解释为排序sJ∈Sj的项。换句话说，定义3.6（多语言同态）设SG（Sg1，Sg2，）是多语言签名，设A和B是两个SG-代数。一个SG-同态h：A→B由一对序排序的同态h1：A1→ B1和h2：A2→ B2给出，使得它们与边界函数可交换，即，如果sisjj，则下面的对偶可交换：我阿SAi（sj）Aj（hi）s（s）Bisis′B（hj）s′（s）Bj给定一个多语言签名SG，所有SG-代数和SG-同态构成一个范畴，记为MLAlg（C，I）SG。我们在这个范畴和OSAlg（C，I）SG之间有一个简单的联系，在定理3.7中概述，在更多的运行示例之后。运行示例。 假设我们对多语言SG感兴趣（Sg1，Sg2，）根据以下规格：• 表示自然数的术语可以根据函数chr：N → Char来代替字符，该函数将自然数n映射到第n个字符符号模|Char|;以及• 表示字符串的术语可以根据函数len：Char→N来代替自然数，即字符串的长度为了得到这样一种多语言，我们提供（1）S1+S2上的连接关系和（2）对于每个约束s i s j j，由下式引入的边界态射sisJjA：sAi→sJAj：• nat1chr2和nat1带边界的字符串2nat1chr2A（n）nat1• CHR2nat1和str2nat1有边界 CHR2nat1A（c）Len（c）= 12nat1A（s）len（s）.和（str）¢S. Buro等人/理论计算机科学电子笔记352（2020）7995<$hi（k））Ai;annd（2）<$hi（f）：hi（w）→hi（s））Ai;（2）∗∗（Ⅲ）.Σ（2）（Ⅲ）（2）下一个定理给出了多语言和顺序排序语言之间的形式对应：我们可以通过应用函子（−）使多语言签名SG成为顺序排序的签名，从而混合底层语言。然而，如果我们考虑SG和SG上的代数范畴，我们不会丢失任何语义信息。定理3.7SG上的多语言代数范畴关联签名SG上的序排序代数范畴之间存在自然同构η：MLAlg（C，I）<$OSAlg（C，I）<$（−）诱