(0) 阅读 (1040)

行动代数 编辑

词条创建者 匿名用户

行动代数

编辑

在代数逻辑中,行动代数是一种代数结构,它既是一个残差半格子,又是一个Kleene代数。它在前者中加入了后者的星形或反相闭合操作,而在后者中加入了前者的左、右残差或暗示操作。与动态逻辑和其他程序模态逻辑不同的是,程序和命题形成了两个不同的种类,而行动代数则将这两者结合成一个单一的种类。它可以被认为是直觉逻辑的一个变种,带有星形和非交换联结,其身份不需要是顶层元素。与Kleene代数不同,行动代数形成了一个品种,而且是可有限公理化的,关键的公理是a-(a→a)*≤a。与Kleene代数的方程理论模型(正则表达式方程)不同,行动代数的星运算在每个方程模型中都是反身传递性封闭。

行动代数的定义

编辑

行动代数(A,∨,0,-,1,←,→,*)是一个代数结构,使得(A,∨,-,1,←,→)形成一个残差半网格,而(A,∨,0,-,1,*)形成一个Kleene代数学。也就是说,它是两类代数的联合理论的任何模型。现在Kleene代数是用准方程来公理化的,也就是两个或多个方程之间的蕴涵,因此,行动代数在直接用这种方式公理化时也是如此。然而,行动代数的优点是它们也有一个纯等价的公理化。动作代数的语言以一种自然的方式延伸到动作网格的语言,即通过包含一个满足操作。下面我们把不等式a≤b写成方程a∨b=b的缩写。这使我们可以用不等式对理论进行公理化,但当不等式扩展为等式时,仍然有一个纯粹的等式公理化。行动代数的公理化方程是残差半格的方程,以及下列星形的方程。1∨a*-a*∨a≤a*a*≤(a∨b)*(a→a)*≤a→axxx个方程可以分解为三个方程,1≤a*,a*-a*≤a*,和a≤a*。这三个等式分别迫使a*是反身的、转身的、大于或等于a的。第二条公理断言,星是单调的。第三条公理可以等价写成a-(a→a)*≤a,这种形式使其归纳作用更加明显。这两条公理与残余半格的公理一起,迫使a*成为半格中大于或等于a的最小反身转折元素。把这作为a的反身转折闭合的定义,我们就会发现,对于任何行动代数的每个元素a,a*是a的反身转折闭合。行动代数的无隐含片段的等式理论,即那些不包含→或←的等式,可以被证明与Kleene代数的等式理论重合,也被称为正则表达式等式。

行动代数

在这个意义上,上述公理构成了正则表达式的有限公理化。Redko在1967年表明这些方程没有有限公理化,对此JohnHortonConway在1971年给出了一个较短的证明。Salomaa给出了一个公理化这一理论的方程模式,Kozen随后将其重新表述为一个使用准方程的有限公理化,即方程之间的影响,关键的准方程是那些归纳法:如果x-a≤x,则x-a*≤x,如果a-x≤x,则a*-x≤x。Kozen定义Kleene代数是这一有限公理化的任何模型。Conway通过给出一个四元素模型0≤1≤a≤a*,其中a-a=a,表明正则表达式的等价理论承认a*不是a的反身转折闭合的模型。在Conway的模型中,a是反身转折的,因此其反身转折闭合应该是a。

行动代数的例子

编辑

任何Heyting代数(以及任何布尔代数)都可以通过取-为∧和a*=1而成为一个行动代数。这是必要的,也是充分的,因为Heyting代数的顶层元素1是其xxx的反身元素,并且是传递性的,也是大于或等于代数的每个元素。字母表Σ上的所有形式语言(有限字符串集)的集合2Σ*形成了一个行动代数,0为空集,1={ε},∨为并集,-为联集,L←M为所有字符串x的集合,使得xM⊆L(同时M→L),L*为L中所有字符串的集合(Kleene封闭)。集合X上的所有二元关系的集合2X²形成一个作用代数,0为空关系,1为身份关系或平等关系,∨为联合,-为关系组合,R←S为由所有对(x,y)组成的关系,使得对于X中的所有z,ySz意味着


内容由匿名用户提供,本内容不代表vibaike.com立场,内容投诉举报请联系vibaike.com客服。如若转载,请注明出处:https://vibaike.com/163753/

发表评论

登录后才能评论

词条目录
  1. 行动代数
  2. 行动代数的定义
  3. 行动代数的例子

轻触这里

关闭目录

目录