基于导数的Mealy机器综合及其数学描述

理论计算机科学电子笔记164（2006）27-45www.elsevier.com/locate/entcs基于导数的Mealy机器综合Helle Hvid Hansen1阿姆斯特丹自由大学（VUA）和Centrum voorWiskunde en Informatica（CWI）De Boelelaan 1081a，NL大卫·科斯塔2Centrum voor Wiskunde en Informatica（CWI）P.O. Box 94079，NLJan Rutten3Centrum voor Wiskunde en Informatica（CWI）和阿姆斯特丹自由大学（VUA）P.O. Box 94079，NL摘要在Rutten [13]中，给出了从2-adic算术中的指定合成二进制Mealy机的理论基础这种结构是基于符号计算的coalgebraic概念的流函数衍生物，一般化的Brzozowski衍生物的正则表达式。在本文中，我们完成了Mealy机的建设，从规范在2-adic和模2算术描述我们如何决定等价的表达式通过减少到规范形式，我们提出了一个Haskell实现这种Mealy综合算法，和理论结果，其特点是（数Mealy机器中的状态，由有理2-adic specifications构造关键词：Mealy机，综合，导数，流，余代数。1引言Mealy机是有限状态转换器，用于对执行同步、持续计算的系统进行建模和规范，例如顺序数字电路（参见[9]），更一般地，反应系统（参见例如[14]）。合成1 电子邮件地址：hhhansen@few.vu.nl2 电子邮件：costa@cwi.nl。 由葡萄牙联邦现金信托基金13762 - 2003号赠款支助3电子邮件：janr@cwi.nl1571-0661 © 2006 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2006.06.00328H.H. Hansen等人/理论计算机科学电子笔记164（2006）27Mealy机的自动化是指从一个正式的规范构造一个Mealy机的自动化过程，该Mealy机的行为满足或实现该规范。在Rutten [13]中，我们证明了Mealy机自然地适合于余代数的框架;它们的行为可以形式化为将输入流映射到输出流的函数;并且概述了一种综合方法，用于从2-adic算术的代数语言中的有理比特流规范构建该方法基于流函数导数的共代数概念，它与Brzozowski[ 2 ]从正则表达式构造有限确定自动机的方法密切相关我们目前的贡献是：（i）描述了如何计算2-adic和模2算术代数中的标准形，以确定两个表达式是否指定相同的行为;这对于终止合成算法至关重要，并且在[13]中没有完全解决;（ii）在函数编程语言Haskell [8]中实现了从2-adic和模2算术的规范中进行Mealy合成;（iii）从有理2-adic规范中构造的最小Mealy机中的状态的特征（定理3.3）。这个结果为我们提供了另一个证明，证明有理2-adic比特流函数有有限多个导数，并且可以用指定来表示它们的数量的上限（推论3.4）。我们指出，有理2-adic函数的这些结果是基于我们的Haskell程序生成的数据证明的。在第2节中，我们介绍了基本概念，以及对Mealy机的coalgebraic观点（参见。[12，13]），在第3节中，我们介绍了我们用作规范语言的比特流代数。这些初步章节的部分内容已经包含在[13]中，但在当前的演示文稿中，我们的动机是实现问题，因此更仔细地区分语法和语义。关于有理2-adic函数的新结果在3.2小节中找到。在第4节中，我们描述了如何符号化地计算流函数导数，以及如何通过规范形式确定等价性在第5节中的实际建设的Mealy机使用这些符号的衍生物进行了说明。我们的Haskell程序的一个简短的，面向用户的描述在第6节，最后，我们在第7节讨论相关的工作。2预赛自然数用N表示，整数用Z表示，有理数用Q表示。有理数x的绝对值写为|X|有理数的符号由函数sgn：Q→ {− 1，0，1}给出，具有通常的定义。我们用Set表示集合和函数的范畴，而一个Set-函子F则是一个从Set到Set的函子。给定一个集函子F，一个F-余代数（X，γ）由一个集X和一个函数γ组成：X→F（X）.函数f：X→Y是F-余代数（X，γ）与（Y，δ）之间的F-余代数同态，若δ<$f=F（f）<$γ.一个F-余代数（Z，φ）是最终的，如果对任何F-余代数（X，γ）存在唯一的F-余代数H.H. Hansen等人/理论计算机科学电子笔记164（2006）2729同态h：（X，γ）→（Z，φ），也称为最终映射。2.1河流和河流扩散方程设A是一个任意集合，则Aω是A上的（有限）字集合，Aω是空字，Aω={α|α：N→A}是A上的流的集合。对于α∈Aω，我们也将α =（α（0），α（1），α（2），. . . ），并且对于a∈A和α∈Aω，我们将使用符号a：α来表示流（a，α（0），α（1），. . ）. α ∈ Aω的初始值定义为α（0），α的流导数为流αJ=（α（1），α（2），α（3），. . . ）.定义映射γ：Aω→A×Aω由α→α（0），αJ∈ α，众所周知，（Aω，γ）是集函子S的最终余代数，定义为S（X）=A×X。我们将把S-余代数称为流自动机.由于（Aω，γ）的有限性，我们可以通过用初值和流导数来定义流和流操作的行为来对于前-例如，我们可以定义具有奇数的有理数的比特流表示。 LetQ={n/（2m+1）|n，m∈Z}表示具有奇数分母的n个比特流的集合，并且令2 ω是比特流的集合（即，2={0，1}上的流），则新的网络不能将Q映射到一个比特流，该比特流包括以下内容：q（0）=odd（q）和qJ=q-odd（q），（1）2其中奇数（n/（2m+1））=nm od2。在B：Q_n→2ω_n_w中定义一个（bitstream）m将比特流与每个q∈Q：如果您不想让我们知道您的姓名，一个自然数n∈N，B（n）是n的二进制展开（后面跟着一个零的尾部）。我们将在3.1节中回到这个例子。方程，如在（1）中使用的那些被称为流微分方程（cf.[12]），并且在一定的良构条件下，它们具有由最终映射给出的唯一流解。在第3节中，我们将使用流微分方程定义比特流上的操作。2.2Mealy机与余代数假设给定集合A和B。输入在A，输出在B的Mealy余代数是集函子M的余代数，定义为M（X）=（B×X）A。 如果Q是 一个状态集，（Q，φ）是Mealy余代数，则转移结构φ：Q→（B×Q）A将每个状态q∈Q关联到一个输出函数oq：A→B和一个下一个状态函数dq：A→Q，定义为φ（q）（a）=（oq（a），dq（a）），对所有a∈A.对于φ（q）（a）=（b，r），我们也将使用符号：Qa|布拉 河如果（Q，φ）和（T，φ）是Mealy余代数，则函数g：Q→T是Mealy同态，如果g尊重转移结构：对所有q∈Q，和所有a∈A，30H.H. Hansen等人/理论计算机科学电子笔记164（2006）27oq（a）=og（q）（a）和dg（q）（a）=g（dq（a））：Qa|bbr|bg（r）。初始Mealy余代数是一个三元组（Q，φ，q），其中（Q，φ）是Mealy余代数，q∈Q是初始状态. Mealy机是一个初始化的Mealy余代数（Q，φ，q0），其中状态集Q和输入/输出集A和B是有限的。Mealy机器也被称为顺序机器（参见。[4]），Mealy机不是语言识别设备，而是所谓的确定性转换器，即，它以确定性方式将输入流转换为输出流。这种输入-输出行为与行为的共代数概念相一致。给定Mealy余代数（Q，φ），状态q0∈Q的Mealy行为是流函数Beh（q0）：Aω→Bω，它将α∈Aω映射到流（b0，b1，b2，. . ）∈Bω，从q0开始在输入α上观察到的输出：q0α（0）|b0q1α（1）|b1...α（k−1）|bkqkα（k）|bk qk+1.更准确地说，对于所有k≥0，Beh（q0）（α）（k）归纳定义为：Beh（q0）（α）（k）= oqk（α（k）），其中qk+1= dqk（α（k））.（二）众所周知（也很容易检验），Mealy行为f：Aω→Bω具有因果性质，这意味着f（α）的第n个元素只依赖于输入α的前n个元素。形式上，f：Aω→Bω是因果的，如果对所有α，β∈Aω和对所有n∈N，如果k≤n.α（k）= β（k）则f（α）（n）= f（β）（n）。因此，对于Mealy余代数中的每个状态，我们可以通过行为映射Beh关联因果流函数。此外，通过初始输出和流函数导数的概念，因果流函数的集合本身可以被视为Mealy余代数。定义2.1设f：Aω→Bω是因果流函数，a∈A.f的初始输出（在输入a上）被定义为（对于任意α∈Aω）f（a：α）的初始值：f[a]：= f（a：α）（0）.f（在输入a上）的流函数导数是函数fa：Aω→Bω它将流α∈Aω映射到f（a：α）的流导数f a（α）：= f（a：α）J.我们以预期的方式将上述概念从字母扩展到A设w∈A<$，a∈A，f<$=f，则f[wa]：=（f w）[a]，且f wa：=（fw）a。H.H. Hansen等人/理论计算机科学电子笔记164（2006）2731注意，在定义2.1中，f[a]定义得很好，因为f是因果的，并且很容易证明因果流函数的导数也是因果的。当我们说到流函数f的导数：Aω→Bω，则我们通常指的是集合{f w|w∈ A <$}。现在设Γ ={f：Aω→Bω|f是因果的}，定义π：Γ →（B× Γ）A为π（f）（a）=（f [a]，fa）. （ 1）是一个有穷的Mealy余代数（cf. [13]）：对于每个Mealy余代数（Q，φ），如（2）中定义的行为映射Beh：Q→Γ是从（Q，φ）到（Γ，π）的唯一Mealy同态。最后的Mealy余代数（Γ，π）通过行为映射Beh刻画了Mealy煤族的所有行为，如果Beh（q）=Beh（r），则称Mealy余代数（Q，φ）中的两个状态q，r∈Q是（行为上）等价的我们将需要以下概念。一个初始Mealy余代数（Q，φ，q）如果Beh（q）=f，则实现了因果流函数f，或者是因果流函数f的（抽象）实现，并且f被称为可实现（或有限状态）行为，如果f可以由Mealy余代数（Q，φ，q）实现，则f可以被称为可实现（或有限状态）行为。机 给定Mealy余代数（Q，φ）中的一个状态q，我们记（Q，φ）中由q生成的Mealy子余代数为<$q <$。 也就是说，q是（Q，φ）对Q的最小子集，它包含q并且在转移映射φ下是闭的。应该清楚的是，如果（Q，φ，q）实现f：A ω → B ω，那么<$q <$也实现f：A ω→ B ω。正如[13]中所示，最终Mealy余代数的存在现在保证了任何f ∈ Γ都有一个（抽象）实现，即f，并且f是实现f的最小Mealy余代数，在这个意义上，任何其他实现至少会有和f一样多的状态。一般来说，我们可以有无限多个状态，但为了综合的目的，我们主要对可实现的行为感兴趣。3比特流代数我们现在将描述我们在指定因果位流函数中使用的两个代数结构。两个代数的语义域是比特流2ω的集合，即，2 ={ 0， 1}上的流，并且使用流微分方程和比特上的布尔运算来定义运算。在2上的布尔运算是：对a，b∈2，ab= max{a，b}，ab =min{a，b}，<$a = 1−a和ab=（a<$ b）<$（<$ab）。在下文中，我们将使用符号2来表示集合{0， 1}以及整数2。上下文应该清楚地说明所要读的是什么要表示的第一个比特流代数基于2-adic数的算术运算[5]。研究这种结构的动机是它与顺序二进制算术和数字电路的相关性。除了Vuillemin的工作外，关于这个问题的文献似乎不多，见例如[16]。 另一个比特流代数是基于模2加法的，它也是由它与数字电路和开关理论[9]的联系所激发的，特别是线性电路的理论和设计在第4节中，我们将更详细地描述语法，并解释如何确定表达式的等价性。在我们描述这两个比特流代数之前，我们首先介绍一些符号和约定。从句法上看，32H.H. Hansen等人/理论计算机科学电子笔记164（2006）27``yyi=0时每个比特流代数的每个比特流代数是通过算术签名在单个比特流变量σ上生成的，该算术签名包含用于加、乘和除的二元函数符号，用于减的一元函数符号，以及常数[0]，[1]，Xn（n∈N）。在这两种情况下，常量都被解释为以下位流：[0]=（0，0，0，.. . ），[1] =（1，0，0，.. . ），Xn=（0，.，0，1，0，0，... . ）的。“我的天，n次因此，作为标准，X0和[1]表示相同的对象。为了节省符号，我们没有显式地将常数Xn，n∈N包含在签名中，但默认它们是签名的一部分。我们注意到，在存在乘法×（2-adic）和π（mod-2）两个定义的情况下，符号Xn后通 过 下 面 的 小 节 中 对 × 和 的 定 义 ， 读 者 可 以 很 容 易 地 证 明 对 所 有α∈2ω ，X×α=X<$α=0：α。因此X×。. . × X= Xn次- 是的- 是的-是的X x = Xn。n次我们将在元表示法中使用一些标准的算术约定 为了说明起见，假设{+，-，·，/，[0]，[1]}是算术签名。我们 会写X而不是X1，有时写x-y而不是x+（-y），x而不是x/y。 x表示法将用于2-adic和mod-2表达式，但仅作为元表示法，并且它将始终与其他操作相明确。该表达式是2进分数还是模2分数。由于分数，而不是逆，是我们算法操作的基本表达式形式，我们选择将/视为原始构造函数，而不是将x/y定义为x·（1/y）的简写（如[13]），其中1/y被定义为y的（乘法）逆。逆1/y可以定义为分数[1]/y，当我们考虑两个比特流代数的代数属性时，我们隐式地使用逆的这个定义。最后，括号用于消除文本中表达式的歧义，但它们不是语法的一部分，为了尽量减少使用它们，我们假设运算符的绑定强度按降序排列为−，·，/，+，+和·关联到右边。 我们还指出，我们严格使用σ来表示比特流变量，即，语法对象，而α和β将被用作比特流或表达式的元符号。3.12-adic运算2-adic比特流代数是结构A2adic=（2ω， +，−，×，/，[0]，[1]）其中这些操作被解释为被视为2-adic整数的比特流的加、减、乘和除。 Brie Berryy描述了，对于任何素数，p，p-adic整数被获得为形式为<$∞aipi的幂级数，其中H.H. Hansen等人/理论计算机科学电子笔记164（2006）2733ai∈ {0，.，p−1}对于所有i∈N，这样一个级数的极限是关于p-adic范数定义的。p进整数Zp形成p进数域Qp的子环[5]，其中幂级数的指数可以从某个负整数而不是从0开始。 通常的整数Z是（严格地！） 包括在Zp中，通过在其有限基p展开式中写入正整数;负整数通过取其正整数的p的补数的无穷形式来表示对应物。 比特流a =（a0，a1，a2，.. . ）因此表示2-adic整数∞i=0时ai2i，特别是正整数，由比特流表示，仅包含有限个1包含无限多个02-adic整数的加法是二进制加法的无限版本，也就是说，进位位可以无限传播例如，（1，1，1，.. . ）+（1，0，0，. . ）=的（0，0，0，.. . ），这表明−[1] =（1，1，1，. . ）. 2-adic乘法是2-adic加法的柯西积，即， 对于比特流α和β，（α×β）（n）=ni=0 α（i）<$β（n−i），其中<$表示2-adic求和，可以计算以加法和移位的方式，类似于如何乘以通常的整数。2-adic整数形成交换环和整环，因为没有零因子，即，α×β= [0]意味着α= [0]或β=[0]。这意味着算术运算具有结合性、交换性和分配性等熟悉的性质，我们将在下文中自由地使用这些性质。然而，Z2不是一个域，因为初始值为a0= 0的 2-adic整数没有a（乘法）逆。这是很清楚的，因为α×β=[1]意味着α（0）=β（0）= 1，事实上，它表明a0在底层结构中有一个逆，这在2-adic的情况下意味着a0= 1/a0 = 1。2-adic操作由图1中的流微分方程在位流上定义。衍生物初始值条件（α+β）J=αJ+βJ+[α（0）<$β（0）]（−α）J= −（αJ+ [α（0）]）（α×β）J=αJ×β+ [α（0）]×βJ（α/β）J=（αJ−[α（0）]×βJ）/β（α+β）（0）=α（0）<$β（0）（−α）（0）=α（0）（α×β）（0）=α（0）<$β（0）（α/β）（0）=α（0）β（0）= 1Fig. 1. 2进运算从上面对2-adic整数的描述中，+和×的流微分方程应该很容易理解。−的定义方程是简单地从+的定义方程和α+（−α）=[0]的要求推导出来的，通过在两边取初值和导数。对于初始值，我们得到α（0）<$（−α）（0）= 0，因此（−α）（0）=α（0）。 通过求导，我们得到αJ+（−α）J+ [α（0）] =[0]，因此（−α）J= −（[α（0）] +αJ）。 α/β的流微分方程可以类似的衍生第二部分。1我们已经看到，具有奇数分母的算法的数据流Q的子块可以被视为比ΣΣ34H.H. Hansen等人/理论计算机科学电子笔记164（2006）27特流，并且实际上，最终流映射H.H. Hansen等人/理论计算机科学电子笔记164（2006）273522B：Q_n→A2_dic是整数和有理数的一种算术运算，因此应用于表示具有奇数分母的整数和有理数的位流的2_dicoperaticor atic on特别地，由于恒定流X=（0，1，0，0，.. . ）表示基数2，我们有比特流的α+α=X×α。3.2有理2-adic流函数在这一节中，我们将使用同态B导出的对应：Q→A2adictoprovideanum erinterprationoftakingderivivofrational2-adic流函数（稍后定义），这反过来又导致了关于它们的最小实现自动机的大小的结果（推论3.4），以及有理2-adic流函数具有有限实现这一事实的另一[13]）。由于我们对比特流和2-adic运算符的数值语义感兴趣在此基础上，我们将利用B（q）对q∈ Q_n进行定义，并在我们的元符号中简单地使用了所有的元素和符号。定义3.1比特流函数f：2ω→ 2ω是有理2-adic流函数，如果f具有以下形式：Mf（σ）=×σn其中m和n是整数，n是奇数，σ是流变量。从2-adic运算的定义中，应该清楚有理2- adic流函数是因果的。作为一个例子，有理2进流函数f（σ）=6×σ可用2-adic表示法表示为f（σ）=X+X2×σ。此外，委员会认为，−9 −[1]−X3我们注意到f（σ）与−2×σ等价，但与−12×σ不等价，因为只有分数3 18有奇数分母的都是定义明确的。引理3.2（数值2-adic导数）设f：2ω→ 2ω是以下形式的2-adicf（σ）=d+m×σ n对于整数d，m和n（奇数）。对于a∈ 2，流函数导数f a由下式给出：f（σ）=da+m×σ一其中（在数值解释中）⎧如果% d为偶数，则为% dn⎧如果d（0）=m（0），则为1（d+m）d0=2如果d为奇数，则为1d1=21（d+ m-n） 如果d（0）/=m（0）证据 应用第7页图1中的电感定义来确定f（0：36H.H. Hansen等人/理论计算机科学电子笔记164（2006）27nnnnnσ）J和f（1：σ）J，我们得到d0=dJ−[d（0）]×nJ，d1= dJ+ mJ+ [d（0）<$m（0）] − [d（0）<$m（0）] ×nJ。剩下的证明现在使用（1）很简单，我们只给出一些情况的细节。在d是奇数的情况下，我们得到d0：JJ 11 1d0=d−n=（d− 1）− （n− 1）= （d− n）。2 2 2当d和m都是奇数时，即d（0）=m（0）= 1，我们有JJ 11 1d1=d + m +1 =（d− 1）+（m− 1）+ 1 =（d + m）。2 2 2Q使用导数的数值解释，我们可以证明有理2-adic函数有有限个导数。定理3.3（有理函数的导数）设f（σ）=m×σ是一个有理2-adic流函数，其中m=0，n > 0是奇数，则对f的所有流函数导数fw，w ∈ 2 π，fw有如下形式f（σ）=dw+m×σwn（三）其中dw是整数，使得1）−n+1≤dw≤m− 1ifm>0，2） −n+ m +1 ≤ 如果m 0，则dw≤ 0<。证据引理3.2的一个直接结果是f的导数具有形式（3），因为f本身具有引理3.2中要求的形式（取d≠ 0），因此f的所有导数也是如此。值dw在给定范围内的证明可以通过对w∈2<$的长度的归纳来进行，使用引理3.2中给出的流函数导数的数值解释。我们离开细节给读者。Q因此，有理2-adic函数f（σ）= m×σ的导数可由dw的不同值表征，这意味着由上述定理，我们可以导出有理2-adic函数f的态数的上界.推论3.4（自动机大小）设m×σ<$是实现有理2-adic函数f（σ）=m×σ的最小Mealy 余 代 数 ， 其 中 m 和 n 是 整 数 ， 使 得 m= 0 ， n 是 奇 数 ， 并 设 NumStates（m×σ<$）表示H.H. Hansen等人/理论计算机科学电子笔记164（2006）2737nnnnnnnnn状态为m× σ。然后M⎧⎨|M|+|n|如果m> 0，则为− 1NumStates（状态数）n×σ）≤gcd（m，n）⎩|M|+|n|gcd（m，n）n如果m0<我的律师。让我和我的朋友们：=sgn（m）·|M|/gcd（m，n）andn：=|/gcd（m，n），则称y m ∈ = m，且d m ∈ × σ ∈ h ∈ m × σ ∈ h是同构的。|/gcd(m,n),thennumericall y m˜=m,and⟨m˜×σ⟩isisomorphicwit h ⟨m×σ⟩.nnnHenceNumStates（中文）×σ）=Num Stat es（m×σ）。As m an d a tisfy the第三部分的内容。3itfollowsttNum Stat es（数字签名）×σ）等于不同的dw值发生在流函数的衍生物的f。 因此如果m≥0，即，sgn（m）=1，thenmNumStates（状态数）n×σ）≤（m<$−1）−（−（n<$−1））+1=m<$+n<$−1=|+的|n|n|gcd（m，n）-1，并且difm= <0，即，，sgn（m）=−1，thenmNumStates（状态数）n×σ<$）≤−（−n<$+m<$+1） + 1=n<$−m<$=|n|+的|m|为|+的|n|n|.gcd（m，n）Q实验结果有力地表明，推论3.4中的不等式实际上是一个等式。也就是说，上式精确地给出了Σm×σm中的状态数然而，目前我们还没有正式的证据。3.3模2运算mod-2比特流代数Amod2=（2ω，ω，g，ω，ω，[0]，[1]）基于模2加法，换句话说，采用比特流的逐元素异或。在本文中，我们将使用符号来表示位流和位上从上下文来看，打字应该是清楚的mod-2比特流操作没有数值解释;相反，它们对应于在Mod2环（和整数域）上被视为形式幂级数的比特流上的操作（2，k，k，id， 0， 1）。注意，模2加法是幂零的，即，对于任何a∈2，a∈a= 0，因此−a=a=id（a）。比特流α=（a0，a1，a2. . ）现在被解释为形式幂级数的系数38H.H. Hansen等人/理论计算机科学电子笔记164（2006）27a0+a1x+a2x2+根据形式幂级数理论，可以得出Amod2也是交换环和整环，其中f是幂零的，g是单位元。特别地，乘法是关于以下的柯西乘积：除法定义为与除法相反，我们再次要求对于分数α<$β，β（0）= 1。模2运算由图2中的流微分方程定义。H.H. Hansen等人/理论计算机科学电子笔记164（2006）2739衍生物初始值条件（α<$β）J=αJ<$βJ（α<$β）（0）=α（0）<$β（0）β（0）= 1（gα）J=g（αJ）（gα）（0）=α（0）（α<$β）J=（αJ<$β）<$[α（0）]<$βJ（α<$β）（0）=α（0）<$β（0）（α<$β）J=（αJ<$[α（0）]<$βJ）<$β（α<$β）（0）=α（0）图二. mod-2操作我们提到有理mod-2函数可以类似于有理2-adic函数定义，并且可以证明有理mod-2函数是因果的和可实现的。但是，我们没有篇幅提供细节。4语法4.1表达式的导数在第3节中，我们介绍了我们用来指定因果比特流函数的两个比特流代数的语义。我们现在转向它们的语法，并详细描述如何使用相应签名生成的表达式象征性地计算初始值和流函数导数。其思想是提供具有Mealy结构的项代数;表达式θ的Mealy行为然后通过到最终Mealy余代数的行为映射获得，我们将说θ是因果函数Beh（θ）的一个特例这种构造适用于第3节的两个比特流代数，因此我们将使用通用积分域签名n={+，·，-，/}来说明。令Term（σ）为在变量σ上生成的表达式。回想因果函数f（σ）关于比特a∈2的初始输出和流函数导数的定义2.1f[a]=f（a：σ）（0）和fa=f（a：σ）J我们希望在语法中模仿这种语义定义，这意味着给定一个指定因果函数fθ的表达式θ，并且位a∈ 2，我们正在寻找一个系统的过程来获得位θ [a]和表达式θa，使得θ[a] =fθ[a]anddBeh（θa） =（fθ）a。 我们认为，初始值和导数的定义由两部分组成。第一个是比特流变量σ与位a的实例化，它将σ转换为a：σ。 二是f（a：σ）的初值和流导数的选取。实例化比特流变量σ i的语法等价物基于以下观察：对于任何比特流α∈2ω：0：α=X×α=X<$α1：α=[1]+X×α=[1]<$X<$α因此，如果θ∈项θ（σ），则我们用θ（0：σ）表示从θ得到的表达式40H.H. Hansen等人/理论计算机科学电子笔记164（2006）27[1]+X用X·σ代替所有出现的σ;类似地，用[1]+X·σ代替θ中的σ，得到θ（1：σ）∈ 项（σ）。表达式θ（0：σ）和θ（1：σ）称为实例化表达式。它仍然需要定义初始值和实例化表达式的流导数。初始值应该是位，导数应该是项（σ）中的表达式我们归纳地定义实例化表达式的流对于常数，这显然是：初始值衍生物Xn（0）= （Xn）J=Xn−1，n≥1X0（0）= [1]（0）= 1[1]联系我们[0]（0）= 0[0]联系我们对于变量σ，我们不能确定σ（0）和σJ，因为σ本身是不确定的。但这不是问题，因为我们只需要考虑实例化的表达式，并且我们观察到在任何实例化的表达式中，σ总是出现为表达式X·σ的一部分，表示流0：σ。 因此，我们定义（X·σ）（0）= 0和（X·σ）J= σ。不同于X·σ的非原子实例化表达式的流行为通过将图1和图2中的流微分方程分别作为2-adic和mod-2表达式的归纳定义来获得。然而，这意味着形式为α/β的（实例化的）表达式，其中β（0）= 0，没有流行为，因此不是所有的表达式都有Mealy行为。这是，对于例如，2进表达式θ=[1]的情况，因为θ（1：σ）=[1][1]+σ[1]+（[1]+X×σ）它有一个初始值为0的分母，因此θ[1]和θ1是unfined。综上所述，如果定义良好，则在输入a∈2上的项θ（σ）中的表达式θ的初始输出和导数由下式给出θ [a]：= θ（a：σ）（0） 和θa（σ）：= θ（a：σ）J。（四）注意，如果σ不出现在θ中，则θ（a：σ）=θ，其中a∈2。因此，像往常一样，常数表达式可以解释为0元函数，因此它们可以同时具有流行为和Mealy行为，而包含σ的表达式只能具有Mealy行为。定义（4）可以从位扩展到位字w∈2 <$，与定义2.1中的方式相同，当我们谈到导表达式时，我们通常指的是对于某个给定的规范θ的所有表达式θw，w∈2<$。例4.1考虑2进表达式θ=X2×σ. θ的实例化对于比特1，θ（1：σ）=X2×（[1] +X×σ） .[1]+XH.H. Hansen等人/理论计算机科学电子笔记164（2006）2741[1]+XR2[1]+X×σ输入1的初始输出为θ[1] =X2（0）<$（[1] +X×σ）（0）= 0<$1 = 0，导数θ1为.2j 2jJθ（1：σ）J=X×（[1]+X×σ）[1]+X（X×（[1]+X×σ））−[0]×（[1]+X）[1]+X（（X2）J×（[1]+X×σ）+[0]×（[1]+X×σ）J）−[0]×（[1]+X）J[1]+X（X×（[1]+X×σ）+[0]×（[0]+σ+[0]））−[0]×（[0]+[1]+[0]）[1]+X很明显，这个表达式可以使用2-adic比特流代数的恒等式来简化，以产生等价的表达式X+X×σ。下一节将解释从项（σ）计算任意表达式的这种简化形式除了当表达式没有Mealy行为时可能出现的“失败”之外，表达式可以引起无限Mealy行为，即，因果比特流函数，没有有限状态实现。这样的例子是由2-adic表达式σ×σ给出的。通过对n∈N的归纳很容易证明，（σ×σ）0n等价于Xn×（σ×σ）。 对于不同的n，这些表达式显然不是故有诸法，故有诸法。同样，可以证明，[1]第一章只有有限的Mealy实现。 然而，这很容易表明，p+q·σ的形式的描述，对于p、q和r为非线性的p、q和r，具有有限状态的Mealy行为，并且上述观察表明这是可实现的规范的最一般形式。4.2判定表达式这两个比特流代数的一个重要性质是，我们可以有效地决定两个导数表达式是否等价。该判定方法依赖于两个比特流代数是整数域的事实。给定两个任意表达式θ和η，我们首先计算我们称之为它们的标准形。 正常一个表达式θ的形式是两个多项式表达式的分数Nθ/Dθ，贡献范式，即，Nθ和Dθ是形式为Cn·σn的单项式的和，其中Cn是常数（多项式）系数。我们用PNF（p）表示多项式p的分配正规形式如果θ已经是多项式表达式的分数θ=ρ/δ ， 则 θ 的 标 准 形 是 PNF （ ρ ） /PNF （ δ ） 。 如 果 PNF （ Nθ·Dη ） <$PNF（Nη·Dθ），则两个表达式θ和η等价，其中表示语法相等。规范形Nθ/Dθ本质上是关于两个比特流代数的 这些恒等式的一部分是所有整数域所共有的，但常数多项式表达式的约简（即多项式范式中的系数Cn）是每个比特流代数所特有的：约简2-adic系数：由于2-adic常数和运算的数值解释，我们可以将常数多项式2-adic表达式z（即z是在没有变量或除数/的情况下构建的）解释为整数Val（z）。例如，Val（−X2+（[1]+ X）×X2）= −4 +（1 + 2）4 = 8。N中的任何x都可以写成===42H.H. Hansen等人/理论计算机科学电子笔记164（2006）27[1]+X[1]+X[1]+X[1]+X作为其符号二进制展开BinExp（x），其中常数X表示基数2。例如，在一个示例中，BinExp（5）是表达式[1]+X2。如果Val（z）≥0，则常数多项式2-adic表达式z的范式定义为BinExp（Val（z）），并且否则为−BinExp（−Val（z））。例如，[1]−X3的范式是−（[1]+X+X2）。减少模2系数：任何常数多项式模2表达式都可以重写为变量X的有符号幂和（通过应用分布性和其他环定律）。由于α的幂零性，我们可以很容易地看到，这样的和可以通过应用恒等式αα=[0]和gα=α来简化为标准形式。这个标准形由Xn的唯一幂在n上按升序排列的和组成。例如，和X2<$X1<$X0<$gX3<$X2，有标准形式[1]<$X1<$X3。例4.2考虑表达式θ =[1]+ σ +[1]。 利用积分定理，θ=0（[1]+[1]+X）+（[1]+X）·σ. 在完成这些成本核算之后，获得：22-adic代数的标准形X+（[1]+X）×σ模-2代数的标准形：X<$（[1]<$X）<$σ对于表达式θ，我们定义θ的大小（或长度），用len（θ）表示，θ中符号出现的次数。计算多项式p的PNF（p）的时间复杂度在最坏情况下是len（p）中的指数，这是由于应用分配律时子表达式的重复（例如a·（b+c）=a·b+a·c）。也就是说，T（PNF（p））= 2 O（len（θ））。 因此，计算任意表达式θ的标准形的时间复杂度也是2 O（len（θ）），并且检查两个标准化表达式的等价性也具有指数代价：检查θ = Nθ/Dθ和η = Nη/Dη的等价性的最坏情况时间复杂度为2 O（len（θ）+len（η））。虽然效率不是我们实现中的主要关注点，但我们注意到，当初始规范θ具有分母Dθ为常数的规范形式时，等价性检查可以得到优化这尤其适用于有理函数。回想一下两个比特流代数中分数导数的定义：2-adic：（α/β）J=（αJ−[α（0）]×βJ）/βmod-2： （α<$β）J=（αJ<$[α（0）]<$βJ）<$β从这些定义以及对于常数Dθ，对于任意a∈2，我们有Dθ（a：σ）=Dθ，我们看到θ=Nθ/Dθ的所有导数也将有分母Dθ。因此，为了判定θ的两个导数，如δ和η是否等价，需要检查它们的标准形式分子的句法相等性：Nδ<$Nη。这可以在线性时间内完成：O（len（δ）+len（η））。H.H. Hansen等人/理论计算机科学电子笔记164（2006）2743[1]+X[1]+X[1]+X[1]+X5建设我们从给定的比特流规范θ构造Mealy机的方法可以看作是Brzozowski[ 2 ]从正则表达式构造确定有限自动机的方法的推广从指定θ开始，我们为每个比特a∈2计算与输入a对应的转换，并将其用于θ的导数，直到没有新的转换被发现，即，已经达到了一个我们将一个（部分构造的）Mealy机表示为一个标记转移的列表，定点计算从包含从初始指定θ到其直接导数θ0和θ1的转移的列表开始。我们还跟踪列表S中的当前状态/导数，该列表被初始化为包含θ（的标准形式）。通过一个例子最好地说明了这种结构。例5.1考虑2进规范σ/（X2−[1]）。该规范的数值解释为σ/3，因此其规范形式为θ=σ/（[1] +X）。现在我们计算θ的归一化导数：θ=（X×σ）J=σ−[0]×（[1]+X）J为σ= θ0[1]+X[1]+X[1] +Xθ=（[1]+X×σ）J=σ−[1]×（[1]+X）J=−[1]+σ1[1]+X[1] +X[1] +Xθ的初始输出很容易计算：θ[0] = 0和θ[1]= 1。 所以，计算开始于状态列表S1= [σ]，以及转换列表L1：L1 = [σ，0 |0、σ⟩; ⟨σ，1 |1，−[1]+σ][1] +X[1]+X[1] +X[1] +XL1包含θ的Mealy实现中长度为1的路（的表示）。在第一次迭代中，通过计算新状态的导数来计算长度为2的路径。我们发现θ1是唯一的新状态。θ1的初始输出是θ1[0]= 1和θ1[1] = 0，并且导数：−[1]+X×σJ（（−[1]）J+σ+[0]）−[1]×（[1]+X）J−X+σ10=（[1]+X）=[1]+X=[1] +Xθ=（−[1]+（[1]+X×σ））J =（（−[1]）J+σ+[1]）−[0]×（[1]+X）J为σ= θ。11[1]+X[1] +X [1]+X现在我们将θ1加到S1上，得到S2=[σ，−[1]+σ]，并添加新的跃迁L1：L2 = L 1 ++ [−[1]+σ，0 |1，−X+σ;−[1]+σ，1 |0，σ][1] +X[1]+X[1] +X[1] +X在下一次迭代中，我们计算从新状态θ10= −X+σ的跃迁。初始输出为θ10[0] = 0和θ10[1] = 1，导数为：θ=（−X+X×σ）J=（（−X）J+σ+[0]）−[0]×（[1]+X）J=−[1]+σ=θ100[1] +X−X+（[1]+X×σ）J[1]+X（（−X）J+σ +[0]）−[1]×（[1]+X）J[1]+X1−