行动代数

编辑
本词条由“匿名用户” 建档。
在代数逻辑中,行动代数是一种代数结构,它既是一个残差半格子,又是一个Kleene代数。它在前者中加入了后者的星形或反相闭合操作,而在后者中加入了前者的左、右残差或暗示操作。与动态逻辑和其他程序模态逻辑不同的是,程序和命题形成了两个不同的种类,而行动代数则将这两者结合成一个单一的种类。它可以被认为是直觉逻辑的一个变种,带有星形和非交换联结,其身份不需要是顶层元素。与Kleene代数不同,行动代数形成...

行动代数

编辑

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

行动代数的定义

编辑

它是两类代数的联合理论的任何模型。现在Kleene代数是用准方程来公理化的,也就是两个或多个方程之间的蕴涵,因此,行动代数在直接用这种方式公理化时也是如此。然而,行动代数的优点是它们也有一个纯等价的公理化。动作代数的语言以一种自然的方式延伸到动作网格的语言,即通过包含一个满足操作。下面我们把不等式a≤b写成方程a∨b=b的缩写。第二条公理断言,星是单调的。第三条公理可以等价写成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的反身元素,并且是传递性的,也是大于或等于代数的每个元素。

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

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

轻触这里

关闭目录

目录