抽象状态机的有效模型：定义及状态转移系统，计算模型，图灵机

理论计算机科学电子笔记135（2006）15-23www.elsevier.com/locate/entcs抽象效率模型Udi Boker Udi Boker1，2特拉维夫大学特拉维夫，以色列Nachum Dershowitz3特拉维夫大学特拉维夫，以色列摘要我们修改古列维奇的抽象机器的概念，以便包括计算模型，即，共享同一域的机器集。我们还增加了效率要求。由此产生的“有效模型”类关键词：计算模型，图灵机，ASM，抽象状态机，有效性1顺序程序我们首先定义这些是抽象的状态转移系统，其状态是代数。定义1.1（国家）1这项工作是在部分实现博士学位的要求。第一作者的水平。2Email：udiboker@ta u. 梭IL3Email：nac hu md@ta u. 梭Il1571-0661 © 2006 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2005.09.01716联合Boker，N.Dershowitz/Electronic Notes in Theoretical Computer Science 135（2006）J• 一个状态是一个（有限元）词汇表F上的结构（代数）s，也就是说，一个域（元素的非空集合）D连同函数名f∈ F在D上的解释[[f]]s。• 词汇F在域D的位置是一对，表示为f（a），其中f是F中的k元函数名，a∈ Dk.• 状态s中的位置f（a）的值，记为[[f（a）]]s，是域元素[[f]]s（a）。• 我们有时使用术语f（t1，. ，tk）来表示位置f（[[t1]] s，. ，[[tk]] s）。• 定义域相同的词汇表F上的两个状态s和SJ在F - t项的集合T上重合，如果对所有项t ∈ T，[[t]]s=[[t]]SJ.• 域D上的位置l的更新是一对，表示为l：=v，其中v ∈ D.• 在相同的词汇表将一个状态s修改为另一个状态sJ且域为{1：=vJ}，| [[l]]s=[[l]]sJ=v}.• 状态s通过注入ρ：D→DJ在词汇F和域D上的映射ρ（s）是词汇F在DJ上的状态sj，使得对于s的每个l个元素f（a），ρ（[[f（a）]]s）=[[f（ρ（a））]]SJ。• 两个状态s和sJ在同一个词汇表上，分别具有域D和DJ，是同构的，如果存在一个双射π：DParticipateDJ，使得sJ=π（s）。“顺序过程”类似于古列维奇的“顺序算法”，有两个定义1.2（顺序程序）• 顺序过程A是一个元组F，In，Out，D，S，S0，τn，其中：F是一个有限的词汇表;In和Out是F中的空函数名;D是过程域，是一个域;S是它的状态，是词汇表F的结构的集合，在同构下闭合;S0是初始状态，是S在域D上的子集，包含直到In值变化的相等状态（通常称为单个状态s0）;τ：S → S，转换函数，使得：· 域不变性。对于每个状态s ∈ S，s和τ（s）的域是相同的。· 同构保存。转移函数保持同构。这 意味着，如果状态s和sJ通过双射π同构，则联合Boker，N.Dershowitz/Electronic Notes in Theoretical Computer Science 135（2006）17=y=y1=y=y=y2=yτττ（s）和τ（sJ）也通过π同构。 也就是说，τ（π（s））= π（τ（s））。·有限的探索。存在“临界”项的有限集合T，使得如果s和sj在T上重合，则满足π（s，τ（s））=π（sj，τ（sj））。过程A的元组元素被索引为F A、τA等。• 过程A的一次运行是一个有限或无限序列s0~τs1~τs2~τ·· ·，其中s0是初始状态，并且每个si+1= τA（si）。• 一个游程s0~τs1~τs2~τ···终止，如果它是有限的，或者如果从某个点开始si=si+1。• 一个终止游程s0~τs1~τs2~τ···的终止状态是它的最后一个状态，如果它是有限的，或者是它的稳定状态，如果它是有限的。如果有一个终止运行，从状态s开始，在状态sJ结束，我们写~！ sJ。• 序贯过程A在域D上的可拓性是部分函数f：D→D，使得f（x）=[Out]]SJ 无论何时跑步~！[11][12][13][14][15][16][17][18][19][19][1域不变性只是确保了过程的特定“运行”在一个特定的领域。同构保持反映了我们在一个固定的抽象级别上工作的事实。参见[3，第89页]。为了保证过程的行为是有效的，需要有界探索约束.这反映了一个非正式的假设，即一个算法的程序可以由一个有限的文本给出[3，p。90]。2可编程机器“可编程机器”的转换函数由一个有限的“可编程程序”给出：定义2.1（可编程机器）• 一个词汇表为F的搜索程序P具有以下语法：如果x11.11.12 12.1k1k则l1：=v1如果x21.21.22 22.2k2k则l2：=v2.如果x...n1= yn1anddxn2= yn2andd. . . xnkn=ynkn那么ln：=vn.其中每个=是“=”或“=”，n，k 1，... ，kn∈ N，且所有的xij，yij，li，和vi是F项。SS和x而且... X1和x而且... X218联合Boker，N.Dershowitz/Electronic Notes in Theoretical Computer Science 135（2006）• 程序的每一行都被称为一条规则。• 在F -结构s上的可编程程序P的激活，记为P（s），是一组更新{l：=v|ifpthenl：=v∈P，[[p]]s}（在=，/=和合取的标准解释下），或者空集如果上面的集合包含两个相同位置的值。• 可编程机器是一个元组F，In，Out，D，S，S0，P0，其中除了最后一个组件之外的所有组件都是顺序过程（定义1.2），并且P是F.• 可编程机器的运行及其可拓性被定义为顺序过程（定义1.2），其中转移函数τ由τ（s）=sJ∈ S给出，使得τ（s，sJ）=P（s）。为了使marticat程序更具可读性，我们结合了规则，如%注释（如果cond-1）stat-1stat-2其他stat-3类似于[3]的主要引理，可以证明每一个可编程机器都是一个顺序过程，每一个顺序过程都是一个可编程机器。与抽象顺序机（ASMs）相比，我们在过程的定义中没有内置等式，布尔或unfned：等式概念不在过程的初始状态中假设相反，转换函数必须被编程为执行任何需要的相等性检查。布尔常量和连接词可以像任何其他常量或函数一样定义可以显式地使用默认域值，而不是用于未定义值的特殊术语。3有效模型我们将“有效过程”定义这一假设指出，除了域表示（“基本结构”）之外，过程可能只有有限的初始数据因此，我们通过允许初始状态包含一个“几乎恒定的结构”来形式化初始数据的有限性由于我们正朝着有效性的特征化前进，程序实际操作的领域应该有无数的元素，这些元素必须是可命名的。联合Boker，N.Dershowitz/Electronic Notes in Theoretical Computer Science 135（2006）19因此，在不失一般性的情况下，可以假设命名是通过术语。定义3.1（几乎常数和基本结构）• 一个结构S几乎是常数，如果除了有限个位置之外，所有位置都具有相同的值。• 定义域D上的有限词汇表F的结构S是基结构，如果所有定义域元素都是唯一F-项的值。也就是说，对于每个元素e∈D，存在唯一的F-项t使得[[t]]S=e。• 定义域D上的词汇F的结构S是结构SJ和Sjj，表示为S=SJSJJ，JJ J J如果F=F，则对于S的每一个l，[[l]]S=[[l]]Sj，并且对于SJJ的每个位置l。一 个 基 结 构 同 构 于 它 的 词 汇 表 的 标 准 自 由 项 代 数 （ Herbranduniverse）。命题3.2设S是词汇G和领域D上的基结构。然后又道：• 词汇G至少有一个空值函数。• DomainD是可数的。• 每个域元素都是S的唯一位置的值。公理3.3（初始数据）过程的初始状态由无限基结构和几乎常数结构组成。也就是说，对于一些无限基本结构BS和几乎恒定结构AS，并且对于每个初始状态s0，对于一些In，我们有s0= BSAS{In}。定义3.4（有效程序和模型）• 有效过程A是满足初始数据假设的顺序过程 因此，有效过程是一个元组在定义1.2中定义的顺序过程元组中添加基本结构BS和几乎恒定结构AS。• 一个有效模型E是一组共享相同基本结构的有效过程。也就是说，对于所有有效过程A，B∈E，BSA= BSB。一个计算模型可能有一些预定义的复杂运算，比如一个内置整数乘法的RAM模型。将这样的模型视为顺序算法，允许初始状态将这些复杂函数作为预言机包含在内[3]。由于我们要求有效性，我们不能允许任意函数作为预言机，并强制初始状态只包含域表示之上的有限数据（公理3.3）。所以20联合Boker，N.Dershowitz/Electronic Notes in Theoretical Computer Science 135（2006）在所需的抽象级别上对模型的观察是通过“大步骤”来完成的，这可能会使用复杂的功能，而这些复杂的功能是通过幕后的有限序列的“小步骤”来实现的。也就是说，一个有效过程（的外延性）可以被包括在其他有效过程的初始状态中（作为一个（参见[ 2 ]的4有效性包括可计算图灵机和其他计算方法可以被证明是有效的。我们将在下面演示如何用有效模型来描述图灵机和计数器机。4.1图灵机我们考虑具有双向无限带的图灵机（TM）。磁带字母表为{0， 1}。磁带的两个边缘由一个特殊的$符号标记。通常，图灵机的状态（瞬时描述）是左，q，右，其中左是一个有限字符串，包含读取头左侧的磁带部分，q是机器的内部状态，右是一个有限字符串，磁带部分位于读取头右侧。读取头指向右字符串的第一个字符TM可以通过以下有效模型E来描述：网域： 以$符号结尾的有限字符串。这就是定义域D={0， 1}$。基础结构： 有限字符串的构造函数（name/arity）：$/0，缺点0/1和缺点1/1。几乎恒定结构：• 输入和输出（空值函数）：In，Out。In在初始状态下的值是磁带的内容，作为以$符号结尾的{0， 1}• 字母表字符和TM状态（空值）的常量：0，1，q0， q1，...，q k。它们的初始值是无关紧要的，只要它是每个常数的不同值。• 保持图灵机当前状态的变量（空值）：Left、Right和q。它们的初始值是：左= $，右= $，q=q 0。• 检查磁带的函数（一元函数）：Head和Tail。在所有位置，它们的初始值都是$。联合Boker，N.Dershowitz/Electronic Notes in Theoretical Computer Science 135（2006）21转换函数：对于每个图灵机m∈TM，通过一个类似于以下的可编程程序定义一个有效过程mJ∈E如果q=q_0%TM%write1，向右移动，切换到q_3左：= Cons_1（左）右：=尾（右）q：= q_3内部操作%尾部（Cons_1（左））：=左侧头部（Cons_1（左））：= 1如果头部（右）= 1%写0，向左移动，切换到q_1左：=尾（左）右：= Cons_0（右）q：= q_1内部操作%尾部（Cons_0（右））：=右头部（Cons_0（左））：= 0如果q =q_1% TM...如果q = q_k%，则停止状态Out：= RightHead和Tail的更新是簿记操作，实际上是“幕后”小步骤的一部分该过程还需要一些初始化，以便将内部函数Head和Tail的值填充到给定输入字符串的所有字符串它按顺序枚举所有字符串，为其分配Head和Tail值，直到遇到输入字符串。以下内部变量（空值函数）用于初始化（Name =初始值）：New=$，向后= 0，向前= 1;AddDigit= 0，方向=$。% 顺序构造左变量%，直到它等于输入In，用于填充%是Head和Tail的值。%枚举为$，0$，1$，00$，01$，.ifLeft= In%完成右：=左左：=$else%保持枚举ifDirection= New %defaultvalifHead（Left）=$ %$ -> 0$左侧：= Cons_0（左侧）头部（Cons_0（左侧））：= 0尾部（Cons_0（左侧））：=左侧如果头（左）=0%例如110$ ->111$左：= Cons_1（尾（左））头（Cons_1（尾（左））：= 1尾（Cons_1（尾（左））：=尾（左）如果头部（左）=1%01$->10$; 11$->000$方向：=向后左：=尾（左）右：= Cons_0（右）如果方向=向后如果头部（左）= $%，则添加最右边的数字方向：=向前AddDigit：= True如果头部（左）=0%，则更改为1左：= Cons_1（尾部（左））22联合Boker，N.Dershowitz/Electronic Notes in Theoretical Computer Science 135（2006）方向：=前进如果头部（左）=1%，则向左向后：=尾部（左）右：= Cons_0（右）ifDirection=Forward %Gather right 0ifHead（Right）=$ %完成收集方向：=新，如果 AddDigit= 1左：= Cons_0（左）头部（Cons_0（左））：= 0尾部（Cons_0（左））：=左AddDigit = 0其他左：= Cons_0（左）右：=尾（右）头（Cons_0（左））：=0尾部（Cons_0（左））：=左4.2计数器。计数器机（CM）可以用以下有效模型E来描述：定义域是自然数N。基本结构由一个空函数Zero和一个一元函数Succ组成，解释为N上的正则后继 。 几 乎 恒 定 的 结 构 具 有 词 汇 表 （ 名 称 /arity ） ： Out/0 ，CurrentLine/0 ， Pred/1 ， N ext/1 ， Reg 0 ， . ， Reg n/0 ， 以 及 行1，...，线k/0。它的初始数据是True= 1，Line i=i，所有其他位置都是0。相同的结构适用于所有机器，除了寄存器数量（Reg i）和行数（Line i）。对于每个计数器机m∈CM，定义一个有效过程mJ∈E，以下是一个程序：%s：填充% 前置函数直到值投入的百分比ifCurrentLine = ZeroifNext = Succ（In）CurrentLine：=Line_1 elsePred（Succ（Next））：= Next Next：= Succ（Next）% 模拟反机器程序。%a、b、c和d的值如%的CM程序行。如果CurrentLine = Line_1Reg_a：=成功（Reg_a）% 或Pred（Reg_a）Pred（Succ（Reg_a））：如果Reg_b =零，则CurrentLine：=c else如果CurrentLine= Line_2，则CurrentLine：= d...%始终：输出：=Reg_0联合Boker，N.Dershowitz/Electronic Notes in Theoretical Computer Science 135（2006）235讨论在[3]中，Gurevich证明了任何满足他的假设的算法都可以用抽象状态机来表示。但是ASM被设计为因此，它可以计算非有效函数。我们采用了古列维奇对于有效性：算法的初始状态除了域表示之外可能只包含有限数据。除了输入之外，同一过程的不同运行共享相同的初始数据;同一模型的不同过程共享一个基本结构。在这里，我们证明了图灵机和计数器机是有效的模型。在文[1]中，我们证明了图灵机可以模拟所有的有效模型.为了覆盖超计算模型，需要放松有效性公理或有界探索要求。引用[1] Udi Boker和Nachum Dershowitz，Church-Turing Thesis的形式化，准备中。[2] N. G. 弗鲁加和R。 F. Stéark. TurboAb数据流处理器的这一特殊配置。在大肠 Béorger，A.Gar gant in i和E. R iccobenee，edi tor s，AbstractStateMachineines-Advancesin Theory andApplications ， 10th International Workshop ， ASM 2003 ， Taormina ， Italy ， pages 244-262.Springer-Verlag，Lecture Notes in Computer Science 2589，2003。[3] 尤里·古列维奇顺序抽象状态机捕获顺序算法。ACM Transactions on Computational Logic，1：77