全文 - FORMALISING THE DOUBLE-PUSHOUT APPROACH TOGRAPH TRANSFORMATION

图变换的双推重写方法的形式化

​

罗伯特·索尔德纳 和 德特勒夫·普拉姆普
英国约克大学
电子邮件地址：rs2040@york.ac.uk, detlef.plump@york.ac.uk

计算机科学中的逻辑方法
第20卷，第4期，2024年，第3:1–3:37页
https://lmcs.episciences.org/
提交日期：2023年12月27日
出版日期：2024年10月4日
​

摘要

本文利用Isabelle/HOL开发了一个用于双推重写图变换基本理论的形式化框架。我们的工作包括定义基本概念，如图、态射、推出和拉回，并证明它们的性质。我们借鉴Rosen 1975年的研究，确立了推导的唯一性，并使用Ehrig和Kreowski 1976年的证明验证了Church-Rosser定理，从而展示了我们形式化方法的有效性。本文详细介绍了我们在使用Isabelle/HOL时的方法论，包括塑造当前版本的关键设计决策。我们探讨了应用高阶逻辑所涉及的技术复杂性，旨在让读者深入了解使用交互式定理证明器的有趣方面。这项工作强调了形式化验证工具在阐明复杂数学概念方面日益增长的重要性。

引言

形式化方法通过严格验证软件正确性是否符合其规范，在最小化软件缺陷方面发挥着重要作用。这些方法运用数学技术来确保软件实现与预定义的规范和需求一致，包括模型检查、定理证明和符号解释[HR04]。

交互式定理证明器已经验证了重要的数学定理，如四色定理[Gon07]、素数定理[ADGR07]和开普勒猜想[HAB+15]。它们在验证特定算法和软件组件方面也发挥了重要作用，例如seL4微内核[KEH+09]和CompCert编译器[Ler09]。这些实例展示了交互式定理证明器在处理复杂理论和系统方面的有效性。

我们的研究致力于严格证明图变换的双推重写方法[EEPT06]中的基本结果，为我们使用Isabelle证明助手[NK14]验证GP 2图编程语言[Plu16, CCP22]中特定程序的总体目标做出贡献。

本文不仅综合了先前已发表的材料[SP23]，还介绍了新的必要技术细节，包括：

关键词：双推重写图变换，Isabelle/HOL，推导的唯一性，Church-Rosser定理。

3:2 R. Söldner 和 D. Plump 第20卷第4期

• 图、态射和规则的形式化，包括对我们设计决策的讨论。

• 关于我们粘合构造的额外细节。

• 我们增加了额外的证明，例如推出保持满射性的事实。

• 我们采用了定理4.3来涵盖顺序独立直接推导的交换性。

虽然像Strecker [Str18]这样的早期工作已将交互式定理证明器应用于图变换，但他们尚未充分探索双推重写方法可用的广泛理论成果。据我们所知，我们的工作是首次将双推重写图变换中的基础结果形式化。关于相关工作的更多细节见第5节。

在双推重写方法中，我们的目标是抽象掉特定的节点和边标识符。为实现这一点，我们引入了独立的类型变量，代表每个图的节点和边的类型。这种区分使得在开发过程中能够使用Isabelle的类型检查器来防止图之间节点或边标识符的意外混淆。然而，我们遇到了一个挑战：Isabelle无法在区域定义内对新的类型变量进行量化，这使得形式化推出和拉回的泛性质变得复杂。

为缓解此问题，我们在区域中采取了一种策略，将节点和边标识符定义为自然数。这一决定，以及其他一些决定（例如可能为节点和边标识符使用统一类型），需要替代构造并考虑约束条件，例如确保有足够大的标识符宇宙来执行不相交并集。我们将在技术性第2节中讨论这些关键的设计选择。

为了确立直接推导的唯一性，我们的证明策略分为两个不同的阶段。首先，我们专注于证明推出补的唯一性。接着，在假设推出补同构的情况下，我们证明推出对象本身的唯一性。在第一阶段，我们的方法受到Lack和Sobocinski的方法论[LS04]的启发。然而，我们调整了他们的方法，结合了推出特征刻画和简化链条件[EK79]，并利用了推出的组合与分解引理以及拉回。

对于Church-Rosser定理的证明，我们基于Ehrig和Kreowski的原始工作[EK76]。这里，推出特征刻画和简化链条件同样至关重要。我们进一步采用了推出和拉回的合成与分解引理。此外，我们引入了一个有助于在拉回和推出之间转换的引理。

虽然我们认识到有可能将我们的证明从图构造推广到黏附范畴，但这并非我们的主要目标。我们的决定基于两点考虑：首先，为了避免处理抽象范畴类（如范坎彭方）所涉及的复杂性；其次，因为我们的研究既涉及像推出和拉回这样的抽象概念，也涉及这些概念的集合论构造。为所有黏附范畴提供相应的构造是不切实际的。

我们的长期目标是为验证GP 2中的图程序奠定基础，GP 2是一种从根本上基于双推重写图变换方法的语言。我们期望为图变换语言中的形式推理提供交互式和自动化的工具支持。一个有效的GP 2证明助手将需要图、属性、规则、推导等的具体定义，这引导我们将重点放在图变换概念上。

本文的其余部分组织如下：

• 第1节简要介绍Isabelle证明助手，重点介绍我们研究中使用的构造。

• 在第2节中，我们深入探讨DPO图变换的基础知识以及在Isabelle中相应的形式化。本节涵盖了关键概念的形式化，如图、态射和规则。

• 第3节讨论直接推导的唯一性，包括推出补唯一性的详细证明。

• 第4节探讨Church-Rosser定理，该定理断言并行独立的直接推导可以重新排列，最终到达一个共同的图。

• 第5节简要回顾了该领域的相关工作，为我们的研究提供背景和来龙去脉。

• 最后，第6节总结了我们的主要发现，并概述了未来研究的潜在方向。

所有的形式化工件，包括完整的Isabelle理论，都可以在GitHub上获取：https://github.com/UoYCS-plasma/DPO-Formalisation。

1. Isabelle/HOL

Isabelle是一个多用途的交互式定理证明器，它基于LCF方法的原则运行。其设计的核心是一个紧凑的元逻辑证明内核，负责证明检查，这一特性显著增强了对证明器可靠性的信心。当提到Isabelle/HOL时，我们讨论的是Isabelle内的高阶逻辑实例化，被广泛认为是其套件中最成熟的演算[PNW19]。该实例化的特点是一个支持多态高阶函数的强类型系统[BH18]。

在Isabelle/HOL中，类型变量通过前导撇号明确标记。例如，类型为'a的项f表示为f :: 'a。我们的形式化利用了区域，这是一种用于编写和构造参数化规范的复杂机制。一个区域封装了一组参数（x1…xn）、假设（A1…Am）以及由此产生的定理，表示为∧x1…xn.(A1; …; Am) =⇒ C。这种方法有助于有效地组合和增强上下文，产生清晰且可维护的表示。更多细节，Ballarin [Bal21]提供了广泛的介绍。

此外，我们采用了易读的半自动推理（Isar），这是Isabelle用于编写结构化证明的框架[Wen99]。与线性执行演绎规则的"应用脚本"不同，Isar采用结构化的、有组织的方法。这种方法显著提高了证明的可读性和可维护性[NK14]。关于Isabelle/HOL的全面介绍可在[NK14]中找到。

2. Isabelle中的DPO图变换

我们在Isabelle/HOL证明助手内对基于DPO的图变换的形式化，主要围绕（有限）有向带标签图展开。

3:4 R. Söldner 和 D. Plump 第20卷第4期

图2. 反映我们形式化的区域层级结构

2.1. 图

这些图是在一个抽象的标签字母表上定义的，该字母表包含不同的节点和边标签集。我们有意将标签保持抽象，因为这确保了我们所讨论的属性普遍适用于特定的标签字母表。我们的定义是包容性的，我们允许平行边和环。

定义 2.1 (图)。字母表L上的一个图G = (V, E, s, t, l, m)是一个系统，其中V是节点的有限集，E是边的有限集，s, t: E → V是为每条边分配源和目标的函数，l: V → LV和m: E → LE是为每个节点和每条边分配标签的函数。

在证明助手内的形式化过程要求遵循特定的形式体系；在我们的上下文中，这是经典的高阶逻辑。这项工作涉及一系列设计选择。首先，我们采用Noschinski [Nos15]的方法，利用记录类型来实现组件的简洁表示，并利用区域来系统地强制这些组件的属性。图2从区域层级的角度描绘了我们开发的形式化。在此图中，箭头表示"被…使用"。例如，Graph区域作为Morphism区域的基础。类似地，Rule依赖于Morphism，而DirectDerivation依赖于Rule。

虽然我们工作的部分内容已在之前的工作[SP22]中描述过，但本文将改进和更新我们的方法。

正如在引言部分最初提到的，Isabelle/HOL只处理全函数。这意味着这些函数在底层类型的整个宇宙上都有定义。内置的option数据类型是表示可选值（即数据存在与否）的标准方式。这个和类型可以保存两种类型的值，由其构造子表示：

• None用于表示值不存在，以及

• Some a捕获值的存在，其中a是实际持有的值。

通过使用option数据类型，我们可以将偏函数模拟为'a ⇒ 'b option类型的函数，这通常被称为内置同义词map，带有中缀符号⇀。标准库中的另一个扩展是有限集和有限映射，分别称为fset和fmap。这些数据类型是在标准的（可能无限的）集合和映射之上，通过使用typedef关键字构建的，该关键字指示Isabelle/HOL提供一个具有有限元素和额外有限性质的新数据类型。

我们考虑以下不同的设计选项来进行形式化： (1) 使用有限映射和有限集（fmap和fset），以及 (2) 依赖全函数连同finite谓词。

虽然从工程角度来看，第一个选项在类型系统中编码属性似乎很有吸引力，但它并非没有挑战。在这里，我们可以通过使用内置的fmap和fset来表示图，如下所示定义一个pre_graph记录：

第20卷第4期 图变换的双推重写方法的形式化 3:5

record ('v,'e,'l,'m) pre_graph =
nodes :: "'v fset"
edges :: "'e fset"
source :: "('e,'v) fmap"
target :: "('e,'v) fmap"
node_label :: "('v,'l) fmap"
edge_label :: "('e,'m) fmap"

强制执行底层对象相应属性的区域的实现，可以在fmap和fset的上下文中使用更高层次的抽象来表达。在这种情况下，我们利用内置的原生fmdom和fmran函数来产生值域和定义域的fset，镜像出已定义的区域。这是可行的，因为有限映射依赖于option数据类型。源函数的完整性表达为fmdom sG = EG ∧ fmran sG |⊆| VG。相反，在全函数场景（2）中，需要显式量化节点和边的集合以表达等效的陈述。我们写∀ v ∈ EG. sG e ∈ VG来表达相同的性质。

根据我们的经验和评估，我们选择继续采用（2）方法以加强我们的自动化尝试。这个决定主要源于fset、map和fmap理论发展的不足。我们发现我们处于需要为fmap和fset建立许多以前未被证明的基本性质的境地。尽管Isabelle发行版的lifting和transfer包[HK13]提供了应用来自底层理论（如set和map理论）的已证明性质的基础设施，但整个过程仍然需要大量的努力。Díaz向形式化证明存档提交的工作[Dí20]进一步强调了这一点，该工作通过新的构造和已证明的性质增强了fmap理论。

相应的pre_graph记录由后续的Isabelle代码定义。

record ('v,'e,'l,'m) pre_graph =
nodes :: "'v set"
edges :: "'e set"
source :: "'e ⇒ 'v"
target :: "'e ⇒ 'v"
node_label :: "'v ⇒ 'l"
edge_label :: "'e ⇒ 'm"

我们在下面的代码块中呈现了强制执行图性质的最终区域。值得注意的是，由于全函数是为整个宇宙定义的，因此无需关于节点和边标签性质的显式陈述。

locale graph =
fixes G :: "('v::countable,'e::countable,'l,'m) pre_graph"
assumes
finite_nodes: "finite VG" and
finite_edges: "finite EG" and
source_integrity: "e ∈ EG =⇒ sG e ∈ VG" and
target_integrity: "e ∈ EG =⇒ tG e ∈ VG"

在我们的工作中使用内置的countable类型类用于节点和边标识符，解决了Isabelle/HOL禁止在区域定义中引入新类型变量的约束。这是HOL家族使用的简单类型理论的结果[HUW14]。这种方法类似于[SW09]中发现的方法，其中使用Isabelle的statespace命令来创建一个环境，其中包含将具体类型转换为自然数的公理。我们的方法的不同之处在于，利用countable类型类提供的单射to_nat函数，从而实现高效的类型转换。这个特定的限制在[SP22]中有更详细的说明。单射性也意味着逆函数from_nat的存在。我们使用这种技术将节点和边的任意标识符转换为基于自然数的通用表示。

定义 2.2 (基于自然数的图)。节点和边标识符为自然数的图称为自然图。

在Isabelle/HOL中，我们建立一个类型同义词ngraph，它将现有的pre_graph结构特化为nat（Isabelle中表示自然数的原生类型）用于两个标识符。

type_synonym ('l,'m) ngraph = "(nat,nat,'l,'m) pre_graph"

使用Isabelle/HOL的内置函数to_nat和from_nat允许我们在两种表示之间进行转换。我们定义转换函数to_ngraph，从参数化的pre_graph结构转换到ngraph，如下所示：

definition to_ngraph
:: "('v::countable,'e :: countable,'l,'m) pre_graph
⇒ ('l,'m) ngraph" where
‹to_ngraph G ≡ (|nodes = to_nat ‘ VG
,edges = to_nat ‘ EG
,source = λe. to_nat (sG (from_nat e))
,target = λe. to_nat (tG (from_nat e))
,node_label = λv. lG (from_nat v)
,edge_label = λe. mG (from_nat e)|)›

我们通过将countable类型类提供的to_nat函数应用于节点和边标识符集合中的每个元素，来转换这些集合，这通过映像函数（用""表示）完成。源函数和目标函数首先从nat映射到原始标识符，然后应用源函数和目标函数，随后再映射回nat空间。对于两个标签函数，我们简单地在应用相应的标签函数之前将nat`标识符转换回去。

反向过程，即将基于自然数的图转换为参数化图，操作类似。需要注意的是，from_nat (to_nat x) = x成立，但反之则不成立。需要记住的关键事实是，to_nat的定义依赖于希尔伯特选择算子SOME，它选择一个固定但任意的值。这种依赖是需要考虑的关键方面，因为它从根本上影响了to_nat函数的行为和限制。通过使用SOME，to_nat本质上包含了一定程度的任意性，使得其结果及其与逆过程的关系在我们的上下文中变得非平凡且重要。因此，我们经常需要包含类型注解，以避免推断出不同的类型，否则会导致选择不同的值。这在涉及嵌套函数应用的场景中变得尤为重要。在这些情况下，虽然最终类型正确匹配，但中间类型可能不匹配，导致潜在的差异。通过主动管理这些类型注解，我们确保了函数应用的一致性和准确性，特别是在处理复杂的嵌套结构时，类型对齐对于预期的结果至关重要。

2.2. 态射

接下来，我们将定义图之间保持结构的映射，称为图态射。

定义 2.3 (图态射)。图态射f: G → H是一对映射f = (fV: VG → VH, fE: EG → EH)，使得对于所有e ∈ EG和v ∈ VG： (1) fV (sG(e)) = sH(fE(e)) （源保持） (2) fV (tG(e)) = tH(fE(e)) （目标保持） (3) lG(v) = lH(fV(v)) （节点标签保持） (4) mG(e) = mH(fE(e)) （边标签保持）

我们为图态射采用与图为相同的设计模式：首先，定义一个记录类型来捆绑相关组件，这里包括节点和边映射。然后，建立一个区域来强制态射的性质。态射记录定义如下。

record ('v1,'v2,'e1,'e2) pre_morph =
node_map :: "'v1 ⇒ 'v2"
edge_map :: "'e1 ⇒ 'e2"

需要强调的是，一个态射可以在两个不同的类型之间映射每个节点和边标识符。这个方面对于我们后续关于推出和拉回构造的工作至关重要，我们将在本节后面讨论。

morphism区域利用区域的层次继承特性，使我们能够依赖graph区域来定义源图和目标图。我们通过使用fixes关键字固定pre_morph记录来增强其功能。接着陈述区域公理，断言这些图代表了一个保持结构的映射。这种设计选择不仅简化了区域的结构，而且确保了图属性在态射上下文中的逻辑集成。

locale morphism =
G: graph G +
H: graph H for
G :: "('v1::countable,'e1::countable,'l,'m) pre_graph" and
H :: "('v2::countable,'e2::countable,'l,'m) pre_graph" +
fixes
f :: "('v1,'v2,'e1,'e2) pre_morph"
assumes
morph_edge_range: "e ∈ EG =⇒ fE e ∈ EH" and
morph_node_range: "v ∈ VG =⇒ fV v ∈ VH" and
source_preserve : "e ∈ EG =⇒ fV (sG e) = sH (fE e)" and
target_preserve : "e ∈ EG =⇒ fV (tG e) = tH (fE e)" and
label_preserve : "v ∈ VG =⇒ lG v = lH (fV v)" and
mark_preserve : "e ∈ EG =⇒ mG e = mH (fE e)"

在此上下文中，图G作为源，而H代表目标图。封装G和H之间节点和边映射的记录被命名为f。两个假设，即morph_edge_range和morph_node_range，确保对于源图中的每条边e，fE映射到目标图中的一条对应边，节点亦然。假设source_preserve和target_preserve对于保持图的结构完整性至关重要；它们保证源和目标结构在映射过程中得到一致维护。最后，假设label_preserve和mark_preserve有助于确保节点和边标签在映射期间得以保留，从而保持图的完整信息内容。

定义 2.4 (特殊态射与同构图)。如果fV和fE是单射的（满射的，双射的），则态射f是单射的（满射的，双射的）。如果对于所有v ∈ VG和e ∈ EG，有fV(v) = v且fE(e) = e，则态射f是一个包含。一个双射的态射是一个同构。在这种情况下，G和H是同构的，记为G ≅ H。

我们的特征刻画也利用了区域继承机制。一个单射态射继承了morphism区域的所有属性，并额外断言节点和边映射在源图的节点和边集合上都是单射的。我们通过使用内置的inj_on谓词来实现这一点。这个谓词在确保源图中每个元素到目标图的映射的唯一性方面起着关键作用，从而在变换过程中保持图元素的独特性。

locale injective_morphism = morphism +
assumes
inj_nodes: "inj_on fV VG" and
inj_edges: "inj_on fE EG"

需要注意的是，fV（fE）映射以及图G及其对应组件（VG和EG）也在injective_morphism区域的主体中使用，这些同样由morphism区域提供。

满射态射也遵循此模式。在这种情况下，我们声明对于目标图H中的每个节点（或边），在源图G中存在一个对应的节点（或边），通过相应的态射函数（fV和fE）映射到它。这个条件确保了目标图中的每个元素在源图中都有一个原像，表明映射覆盖了整个目标图。

locale surjective_morphism = morphism +
assumes
surj_nodes: ‹v ∈ VH =⇒ ∃ v' ∈ VG. fV v' = v› and
surj_edges: ‹e ∈ EH =⇒ ∃ e' ∈ EG. fE e' = e›

双射态射结合了单射和满射态射的原则。在这个框架中，我们断言对于源图G中的每个节点（或边），在目标图H中存在一个唯一的对应节点（或边）。我们选择不从injective_morphism和surjective_morphism区域同时继承。相反，我们利用内置谓词bij_betw。做出这个决定的一个关键原因是为了利用自动化：在我们的实验中，使用现有的一套已证明的引理显著促进了定理的证明。虽然如果我们继承这些区域，也可以证明所有这些性质，但我们选择利用现有的基础设施。

locale bijective_morphism = morphism +
assumes
bij_nodes: "bij_betw fV VG VH" and
bij_edges: "bij_betw fE EG EH"

接下来，我们介绍组合两个态射以形成一个单一的联合态射的概念。

定义 2.5 (态射组合)。设f: F → G和g: G → H为图态射。态射组合g ◦ f: F → H定义为g ◦ f = (gV ◦ fV, gE ◦ fE)。

在Isabelle/HOL中，我们用通常隐藏底层细节的定义来定义这个组合，并且通常需要显式展开或一组已建立的已证明性质。选择全函数使我们能够对节点和边映射都使用标准函数组合技术。

definition morph_comp
:: "('v2,'v3,'e2,'e3) pre_morph
⇒ ('v1,'v2,'e1,'e2) pre_morph
⇒('v1,'v3,'e1,'e3) pre_morph" (infixl "∘→" 55) where
"g ∘→ f = (|node_map = gV ∘ fV, edge_map = gE ∘ fE|)"

请注意，每个态射都可以改变节点和边标识符的类型。因此，在我们的定义中，我们引入了三个类型参数。此外，我们引入了中缀语法∘→作为图态射组合的一种语法糖。

引理 2.6 (态射组合的良定义性)。给定两个态射f: G → H和g: H → K，组合g ◦ f: G → K也是一个态射。

如果我们有两个有效的态射，比如f: G → H和g: H → K，那么它们的组合g ◦ f: G → K也是一个有效的态射。在Isabelle中，我们使用lemma关键字以及一个特定的名称（wf_morph_comp）以备将来参考来捕获这个性质。

lemma wf_morph_comp:
assumes
f: ‹morphism G H f› and
g: ‹morphism H K g›
shows ‹morphism G K (g ∘→ f)›

我们首先在assumes块中假设存在两个有效的态射，我们将其命名为f和g。然后，通过使用shows关键字，我们在Isabelle中设定证明目标。在此设定之后，Isabelle要求用户交互地工作以实现所述目标，本质上证明态射组合的有效性。

我们使用intro_locales策略开始证明，这将应用相应的引入规则，产生如下的证明状态。

proof (state)
goal (3 subgoals):
1. graph G
2. graph K
3. morphism_axioms G K (g ∘→ f)

输出显示我们必须完成三个子目标。前两个，即断言G和K是有效图，由于态射性质是平凡的。由于morphism区域为源图和目标图都继承了图性质，这些子目标可以直接得出。

使用Isabelle的Isar语言，我们简化了证明编写过程，专注于论证的逻辑结构和进展。Isar强调"什么"而非"如何"，允许我们将复杂的证明结构化为可理解的片段。我们通过使用show关键字指定目标来开始每个证明，清晰地设定我们的目标。这种方法不仅简化了我们陈述的证明（在本例中，它遵循f和g的态射公理），而且保持了证明的可读性，并与传统的数学推理保持一致，增强了其清晰性和可验证性。

为了处理第三个子目标，我们关注morphism_axioms谓词，这是区域基础设施根据我们陈述的性质产生的一个产物。要完成这个子目标，我们使用标准策略开始证明，该策略将根据最顶层的逻辑连接词执行单个消去或引入规则[Wen]。

因此，我们的任务包括完成前面陈述的六个态射公理，我们将在下面简要概述。最初的两个目标处理这样的事实：对于G中的每条边（和节点），由态射组合创建的映像落在K的边（节点）子集内。

show ‹morphism_axioms G K (g ∘→ f)›
proof standard
show ‹g ∘→ fE e ∈ EK› if ‹e ∈ EG› for e
by (simp add: morph_comp_def
morphism.morph_edge_range[OF g]
morphism.morph_edge_range[OF f]
that)

Isabelle的简化器能够成功地完成所有目标，只要它配备了必要的引理。具体来说，对于我们的情况，我们需要展开morph_comp定义，并且为了完成第一个目标，我们需要为每个图G和K使用morph_edge_range事实。

类似地，断言组合态射在源函数下保持结构的性质也被完成。这个性质在morphism区域（source_preserve）中定义。我们使用类似于先前方法的方式处理它，采用相关的策略和引理（以正向风格使用OF关键字）。

show ‹g ∘→ fV (sG e) = sK (g ∘→ fE e)› if ‹e ∈ EG› for e
by (simp add: morph_comp_def
morphism.morph_edge_range[OF f]
morphism.morph_edge_range[OF g]
morphism.source_preserve[OF f]
morphism.source_preserve[OF g] that)

最后，态射对节点和边标签的保持遵循类似的模式，随后为完整性而展示。

show ‹lG v = lK (g ∘→ fV v)› if ‹v ∈ VG› for v
by (simp add: morph_comp_def
morphism.label_preserve[OF f]
morphism.label_preserve[OF g]
morphism.morph_node_range[OF f] that)

前面讨论的目的是为了让读者直观地理解性质是如何表达的，并让读者初步了解Isabelle中的整体设置。接下来，重点将转向描述我们形式化的基本结构，突出对理解所采用框架和方法至关重要的选定内容。

请注意，如果一个态射由其源和目标唯一标识，我们有时会省略名称并写F → G → H来表示组合g ◦ f。在我们的形式化中，我们用符号∘→表示态射组合，以防止与Isabelle的内置函数组合发生命名冲突。

2.3. 规则

在基于DPO的图变换中，图态射被用来定义规则，作为计算的基本单元。

定义 2.7 (规则)。一个规则(L ← K → R)由字母表L上的图L、K和R以及单射态射K → L和K → R组成。

遵循与之前相同的模式，我们使用一个pre_rule记录并建立一个rule区域来强制执行所需的属性。

record ('v1,'e1,'v2,'e2,'v3,'e3,'l,'m) pre_rule =
lhs :: "('v1,'e1,'l,'m) pre_graph"
interf :: "('v2,'e2,'l,'m) pre_graph"
rhs :: "('v3,'e3,'l,'m) pre_graph"

多态的pre_rule记录已经包含了八个类型参数，允许规则的每个图（左侧、右侧和界面）使用不同的节点和边标识符，同时保持标签类型一致。这种设置通过允许不同节点和边表示之间的态射，提供了显著的灵活性，这在粘合和删除构造中特别有用。然而，这种方法有一个技术缺点：需要在代码库中传播类型注解。在某些情况下，这可能导致代码不直观且难以阅读。为了解决这个问题并在灵活性和可读性之间取得平衡，我们在当前设计中通过为规则、图、态射和其他组件引入记录类型，减少了直接传递到区域中的参数数量。与我们形式化的早期版本相比，这显著减少了直接传入区域的参数数量。

尽管存在挑战，我们相信我们当前的设置在简洁性和保持必要的形式精确性之间提供了一个"甜蜜点"。我们将在本文后面更详细地探讨这种灵活性和可读性之间的权衡，特别是在粘合和删除构造的上下文中。

该区域本身两次继承了单射态射的性质，分别是从界面到左侧和从界面到右侧。

locale rule =
k: injective_morphism "interf r" "lhs r" b +
r: injective_morphism "interf r" "rhs r" b'
for r :: "('v1::countable,'e1::countable
,'v2::countable,'e2::countable
,'v3::countable,'e3::countable
,'l,'m) pre_rule" and b b'

我们需要填充countable类型类约束，以允许将图转换为基于自然数的图。主要原因在于区域机制的一个限制，

图2. 粘合图解

阻止在其定义中引入新的类型变量。一旦我们涵盖了推出（和拉回），我们将简要继续这个讨论。

沿着公共子图添加图组件称为粘合。

2.4. 粘合

下面的粘合构造使用了集合A和B的不相交并集，通常定义为

A + B = (A × {1}) ∪ (B × {2})。

它包含单射函数iA: A → A + B和iB: B → A + B，确保iA(A) ∪ iB(B) = A + B且iA ∩ iB = ∅。

这并不能直接转化为基于高阶逻辑的证明助手，因为该形式体系不足以表达表示的改变。在这里，我们会试图混合'a set（其中'a是元素的类型变量）和('a, nat)类型的元素。

为了简化引理2.8，我们假设D和R – b(K)的集合是不相交的。这个假设阻止了iA和iB在引理中的使用，同时尊重了不要求不相交性的更一般陈述。

引理 2.8 (粘合 [Ehr79])。设b: K → R和d: K → D为单射图态射。则以下定义了一个图H（见图2），即根据d将D和R粘合的结果： (1) VH = VD + (VR – bV(VK)) (2) EH = ED + (ER – bE(EK)) (3) sH(e) = ⎧ sD(e) 如果 e ∈ ED ⎨ dV(bV^{-1}(sR(e))) 如果 e ∈ ER – bE(EK) 且 sR(e) ∈ bV(VK) ⎩ sR(e) 否则 (4) tH 类似于 sH (5) lH(v) = ( lD(v) 如果 v ∈ VD；否则 lR(v) ) (6) mH 类似于 lH 此外，态射D → H是一个包含，而单射态射h定义为对于R中的所有项x：h(x) = 如果 x ∈ R – b(K) 则 x 否则 d(b^{-1}(x))。

我们对粘合概念的形式化始于定义相应的区域，该区域继承了两个单射态射b: K → R和d: K → D，如下所示。

locale gluing =
d: injective_morphism K D d +
r: injective_morphism K R b
for K D R d b

注意，K → R和K → D的单射区域的性质分别绑定到d和r。这些名称是任意选择的，用于引用相应态射的事实，而区域的参数对应于态射对象。

在区域上下文中，我们展示了引理2.8中描述的构造。首先，我们建立缩写，与定义不同，它们不引入必须展开的新概念；相反，它们仅仅允许我们通过缩写名称引用其内容。此构造依赖于和类型，具有两个构造子：Inl和Inr。我们利用内置函数Plus（用中缀符号<+>表示）来计算集合的不相交和。该定义依赖于将Inl构造子应用于第一个集合的每个元素，并将Inr构造子应用于第二个集合的每个元素。需要注意的是，这种设置改变了类型；我们从第一个集合的宇宙（比如'a）和第二个集合的宇宙（'b）移动到和类型'a + 'b。这种转变有助于简单构造不相交和，但会导致我们形式化中的一些复杂情况。我们曾考虑过施加节点（边）必须不相交的约束，作为区域的替代方法。然而，为了与我们构建具体粘合的长期目标保持一致，我们选择不限制我们的形式化，并直接进行构造。

遵循粘合构造（参见引理2.8），我们使用V（和E）来表示粘合图的元素。

abbreviation V where ‹V ≡ VD <+> (VR – bV ' VK)›
abbreviation E where ‹E ≡ ED <+> (ER – bE ' EK)›

符号'指的是内置的映像定义，它将提供的函数应用于集合的每个元素。源函数现在利用两个构造子，通过标准模式匹配来识别边的来源图。在第一种情况，对于s (Inl e)，考虑到V和E的构造，很明显这条边保留在图D中。因此，我们使用来自D的源，通过应用Inl将其重新定位到新类型中。这种重新定位反映了先前提到的单射函数iA的应用，见上文。在第二种情况，当边的源来自R但不来自界面时，需要确定边的源是否投影到界面中。如果是，我们必须应用b的逆，然后通过d进行遍历。我们通过使用内置函数inv_into（它使用希尔伯特epsilon算子SOME）来获取元素。如果不是，节点保持在右侧，只需要应用Inr构造子。

fun s where
"s (Inl e) = Inl (sD e)"
| "s (Inr e) = (if e ∈ (ER – bE ' EK) ∧ (sR e ∈ bV ' VK)
then Inl (dV ((inv_into VK bV) (sR e))) else Inr (sR e))"

目标映射类似。然而，两个标签映射都很直接，只需要与各自的标签函数进行模式匹配。

fun l where
"l (Inl v) = lD v"
| "l (Inr v) = lR v"

最后，我们已经完成了定义图H的pre_graph结构所需的所有组件。我们使用definition关键字来定义最终的pre_graph结构H。

definition H where
‹H ≡ (|nodes=V, edges=E
,source=s, target=t
,node_label=l, edge_label=m |)›

为了确立这个记录代表一个有效图，我们使用sublocale命令，这需要我们完成所需的图性质。

sublocale h: graph H

我们接着定义图态射h: R → H，这对于节点（或边）经由b存在于R中而不在K中是必要的。在第一种情况下，很明显节点（或边）通过Plus使用Inr构造子进行映射。在其他情况下，我们利用b的逆并沿着d前进。在所有情况下，节点（或边）必定存在于Plus的左侧部分，由Inl构造子指示。

definition h where
‹h ≡ (|node_map = λv. if v ∈ VR – bV ' VK
then Inr v
else Inl (dV ((inv_into VK bV) v)),
edge_map = λe. if e ∈ ER – bE ' EK
then Inr e
else Inl (dE ((inv_into EK bE) e))|)›

态射c: D → H是一个单射态射，它使用Inl构造子将图D注入H。

definition c :: "('e, 'e + 'g, 'f, 'f + 'h) pre_morph" where
‹c ≡ (|node_map = Inl, edge_map = Inl |)›

在某些情况下，需要添加额外的类型注解。如果跳过这些，Isabelle会尝试推断相应的类型，这可能导致意想不到的结果。删除构造的形式化在[SP22]中有描述。

2.5. 推出

有了这些组件，我们展示它们如何定义推出的抽象概念。

定义 2.9 (推出)。给定图态射b: A → B和c: A → C，一个图D连同图态射f: B → D和g: C → D是A → B和A → C的推出，如果满足以下条件（见图3）： (1) 交换性：f ◦ b = g ◦ c，且 (2) 泛性质：对于所有满足p ◦ b = t ◦ c的图态射p: B → D'和t: C → D'，存在唯一的态射u: D → D'使得u ◦ f = p且u ◦ g = t。 我们称D为推出对象，C为推出补。

我们无法直接表达泛性质中使用的唯一存在性。用于表达此性质的内置绑定器带来了挑战。由于全函数在整个宇宙上定义，而我们的图可能只覆盖节点（边）标识符的一个子集，内置绑定器会过于强大。因此，我们的量化需要只关注与所需对象相关的节点（边）。因此，我们引入缩写Ex1M，它将只量化相应图中使用的节点和边的所需子集。

abbreviation Ex1M
:: "((’v1,’v2,’e1,’e2) pre_morph ⇒ bool)
⇒ (’v1,’e1,’l,’m) pre_graph
⇒ bool" where
"Ex1M P E ≡ ∃ x. P x ∧ (∀ y. P y
−→ ( (∀ e ∈ EE. yE e = xE e)
∧ (∀ v ∈ VE. yV v = xV v)))"

我们现在准备使用一个区域来形式化推出，处理满足交换性和泛性质的态射A → B、A → C、B → D和C → D。形式化如下：

locale pushout_diagram =
b: morphism A B b +
c: morphism A C c +
f: morphism B D f +
g: morphism C D g for A B C D b c f g +
assumes
node_commutativity: ‹v ∈ VA =⇒ f ∘→ bV v = g ∘→ cV v› and
edge_commutativity: ‹e ∈ EA =⇒ f ∘→ bE e = g ∘→ cE e› and
universal_property: ‹[[
graph (D' :: (’c,’d) ngraph);
morphism (to_ngraph B) D' x;
morphism (to_ngraph C) D' y;
∀ v ∈ Vto_ngraph A. x ∘→ (to_nmorph b)V v = y ∘→ (to_nmorph c)V v;
∀ e ∈ Eto_ngraph A. x ∘→ (to_nmorph b)E e = y ∘→ (to_nmorph c)E e]]
=⇒ Ex1M (λu. morphism (to_ngraph D) D' u ∧
(∀ v ∈ Vto_ngraph B. u ∘→ (to_nmorph f)V v = xV v) ∧
(∀ e ∈ Eto_ngraph B. u ∘→ (to_nmorph f)E e = xE e) ∧
(∀ v ∈ Vto_ngraph C. u ∘→ (to_nmorph g)V v = yV v) ∧
(∀ e ∈ Eto_ngraph C. u ∘→ (to_nmorph g)E e = yE e))
(to_ngraph D)›

该区域包含了图3中描绘的四个态射。我们通过node_commutativity和edge_commutativity分别表达节点和边的交换性。实现泛性质比使用偏函数更复杂。使用偏函数时，我们在两个组合之间使用相等，而不使用偏函数时，我们必须显式量化定义域。我们处理Isabelle区域机制的限制，该限制限制了对用于图D'的新类型的量化。

我们的解决方案涉及利用to_ngraph和from_ngraph基础设施将我们的态射转换为自然数，这是之前讨论过的设置。需要这种变通方法的原因在于简单类型理论的限制，它限制了高阶逻辑系统允许对多态类型变量进行显式量化[HUW14]。因此，某些概念无法直接表达，导致细节可能难以阅读，并与标准数学教科书中的呈现方式不同。

此外，我们对全函数的依赖意味着我们无法直接验证态射的相等性。相反，我们必须量化它们被定义的特定区域。

为了响应区域的限制，我们在区域上下文中引入了一个附加引理。该引理通过省略ngraph主题来推广泛性质。因此，我们可以依赖这个引理来完成大部分工作，无需考虑标识符在图和ngraph之间的转换。

lemma universal_property_exist_gen:
fixes D'
assumes ‹graph D'› ‹morphism B D' x› ‹morphism C D' y›
‹∀ v ∈ VA. x ∘→ bV v = y ∘→ cV v›
‹∀ e ∈ EA. x ∘→ bE e = y ∘→ cE e›
shows ‹Ex1M (λu. morphism D D' u ∧
(∀ v ∈ VB. u ∘→ fV v = xV v) ∧
(∀ e ∈ EB. u ∘→ fE e = xE e) ∧
(∀ v ∈ VC. u ∘→ gV v = yV v) ∧
(∀ e ∈ EC. u ∘→ gE e = yE e)) D›

证明依赖于转换函数的正确性性质。

引理 2.10 (to_ngraph的正确性)。设G是一个图，则to_ngraph G是一个自然图。

正确性性质在Isabelle/HOL中表达为一个当且仅当。

lemma graph_ngraph_corres_iff:
‹graph (to_ngraph G) ←→ graph G ›

我们对态射以及在自然图上提升的态射表达了类似的性质。

引理 2.11 (to_nmorph的正确性)。设m: G → H是一个图态射，则to_nmorph m是一个从to_ngraph G到to_ngraph H的态射。

相应的形式化如下：

lemma morph_eq_nmorph_iff:
‹morphism G H m ←→ morphism (to_ngraph G) (to_ngraph H) (to_nmorph m)›

通过展开to_ngraph和to_nmorph的定义，利用相应函数的单射性和Isabelle强大的自动化能力，我们很容易完成这两个引理。

一个重要性质是推出在同构意义下是唯一的，我们最初在[SP22]中形式化了这一点，并在本文中使用了前述技术进行了增强。

定理 2.12 (推出的唯一性 [EEPT06])。设b: A → B和c: A → C连同D诱导了一个推出，如图3所示。一个图D'连同态射p: B → D'和t: C → H是b和c的推出当且仅当存在一个同构u: D → D'使得u ◦ f = p且u ◦ g = t。

我们在进入pushout_diagram区域上下文时形式化了这个性质，该上下文包含了所有相关的区域假设，并使用其指定的名称。因此，我们只能假设额外的图D'以及B → D'和C → D'。

theorem uniqueness_po:
fixes D'
assumes
D': ‹graph D'› and
f': ‹morphism B D' f'› and
g': ‹morphism C D' g'›
shows ‹pushout_diagram A B C D' b c f' g'
←→ (∃ u. bijective_morphism D D' u
∧ (∀ v ∈ VB. u ∘→ fV v = f'V v) ∧ (∀ e ∈ EB. u ∘→ fE e = f'E e)
∧ (∀ v ∈ VC. u ∘→ gV v = g'V v) ∧ (∀ e ∈ EC. u ∘→ gE e = g'E e))›

在我们的特定情况下，我们有单射推出（和规则），我们也可以陈述推出补的唯一性。

定理 2.13 (推出补的唯一性)。设b: A → B和c: A → C是单射态射，且图D诱导了一个推出，如图3所示。设A → B → D ← C' ← A是另一个具有单射A → C'的推出。则C和C'是同构的。

我们在pushout_diagram区域的上下文中形式化这个定理。由于区域通常依赖于态射，我们需要假设A → B和A → C是单射的。根据我们的假设，即C' → D是一个有效态射，我们可以得出结论C'是一个有效图。这里，为了清晰起见，我们明确添加了假设。

theorem uniqueness_pc:
fixes C' c' g'
assumes
b: ‹injective_morphism A B b › and
c: ‹injective_morphism A C c › and
C': ‹graph C'› and
c': ‹injective_morphism A C' c'› and
g': ‹morphism C' D g'›
shows ‹pushout_diagram A B C' D b c' f g'
−→ (∃ u. bijective_morphism C C' u)›

我们在第3节讨论证明。

2.6. 直接推导

通过规则对图的变换产生了直接推导。所谓的悬空条件是一个关键要求，它确保应用规则后得到的图仍然是良构的。它防止了悬空边的产生，即那些在删除节点后指向不存在节点的边。本质上，悬空条件保证了当一个节点被删除时，所有与其相连的边要么被规则显式删除，要么通过界面图被保留。我们在[SP22]中描述了形式化。

定义 2.14 (直接推导)。设G和H是图，r = ⟨L ← K → R⟩是一个规则，且g: L → G是一个满足悬空条件的单射态射。则G通过r和g直接推导出H，记为G ⇒_{r,g} H，如图4中的双推图所示。

注意，匹配态射g: L → G的单射性导致了一种比任意匹配情况下更具表现力的DPO方法[HMP01]。在我们早期的工作[SP22]中，我们使用direct_derivation区域来表示使用粘合和删除的操作视图。相反，这里我们使用依赖于推出的范畴论定义。

我们的形式化接近定义2.14。我们继承了rule区域，以及一个单射态射g和两个推出(1)和(2)。由于我们引入了pre_rule记录，我们使用访问器函数lhs、rhs和interf来提取相应的对象。

locale direct_derivation =
r: rule r b b' +
gi: injective_morphism "lhs r" G g +
po1: pushout_diagram "interf r" "lhs r" D G b d g c +
po2: pushout_diagram "interf r" "rhs r" D H b' d f c'
for r b b' G g D d c H f c'

操作定义在direct_derivation_construction区域内可用。

locale direct_derivation_construction =
r: rule r b b' +
d: deletion "interf r" G "lhs r" g b +
g: gluing "interf r" d.D "rhs r" d.d b' for G r b b' g H +
assumes a: ‹H = g.H›

在这里，我们遵循相同的模式，但不再依赖pushout_diagram区域，而是依赖deletion和gluing。在for语句内部，我们引入一个新的pre_graph记录，命名为H，它代表最终的图，如图4所示。通过使用assumes语句，我们要求(2)中的推出对象等于H（H = g.H）。这允许在证明内部使用绑定的名称H，而不是g.H。

2.7. 拉回

拉回与推出的概念对偶，拉回通常表示对象在公共对象上的交集。

定义 2.15 (拉回)。给定图态射f: B → D和g: C → D，一个图A连同图态射b: A → B和c: A → C是C → D ← B的拉回，如果满足以下条件（见图5）： (1) 交换性：f ◦ b = g ◦ c，且 (2) 泛性质：对于所有满足f ◦ p = g ◦ t的图态射p: A' → B和t: A' → C，存在唯一的态射u: H → A使得b ◦ u = p且c ◦ u = t。

形式化密切遵循pushout_diagram区域，所有设计考虑也适用于此。

locale pullback_diagram =
b: morphism A B b +
c: morphism A C c +
f: morphism B D f +
g: morphism C D g for A B C D b c f g +
assumes
node_commutativity: ‹⋀v. v ∈ VA =⇒ f ∘→ bV v = g ∘→ cV v› and
edge_commutativity: ‹⋀e. e ∈ EA =⇒ f ∘→ bE e = g ∘→ cE e› and
universal_property: ‹[[
graph (A' :: (’c,’d) ngraph);
morphism A' C c';
morphism A' B b';
⋀v. v ∈ VA' =⇒ f ∘→ b'V v = g ∘→ c'V v;
⋀e. e ∈ EA' =⇒ f ∘→ b'E e = g ∘→ c'E e]]
=⇒ Ex1M (λu. morphism A' A u ∧
(∀ v ∈ VA'. b ∘→ uV v = b'V v) ∧
(∀ e ∈ EA'. b ∘→ uE e = b'E e) ∧
(∀ v ∈ VA'. c ∘→ uV v = c'V v) ∧
(∀ e ∈ EA'. c ∘→ uE e = c'E e))
A'›

我们的许多证明使用基于集合的拉回构造，由以下定义给出。

定义 2.16 (拉回构造 [EEPT06])。设f: B → D和g: C → D是图态射。则以下定义了一个图A（见图5），即f和g的拉回对象： (1) 对于节点和边分别有：A = {⟨x, y⟩ ∈ B × C | f(x) = g(y)} (2) 对于⟨x, y⟩ ∈ EB × EC：sA(⟨x, y⟩) = ⟨sB(x), sC(y)⟩ (3) 对于⟨x, y⟩ ∈ EB × EC：tA(⟨x, y⟩) = ⟨tB(x), tC(y)⟩ (4) 对于⟨x, y⟩ ∈ VB × VC：lA(⟨x, y⟩) = lB(x) (5) 对于⟨x, y⟩ ∈ EB × EC：mA(⟨x, y⟩) = mB(x) (6) b: A → B和c: A → C定义为b(⟨x, y⟩) = x且c(⟨x, y⟩) = y

我们使用pullback_construction区域形式化拉回构造，假设图态射f: B → D和g: C → D。

locale pullback_construction =
f: morphism B D f +
g: morphism C D g
for B D C f g

为了构造拉回对象C，我们首先分别定义所有所需的pre_graph组件，节点和边集如下：

abbreviation V where
‹V ≡ {(x,y). x ∈ VB ∧ y ∈ VC ∧ fV x = gV y}›
abbreviation E where
‹E ≡ {(x,y). x ∈ EB ∧ y ∈ EC ∧ fE x = gE y}›

相应的集合包含对(x, y)，其中x ∈ B且y ∈ C，使得它们通过f和g投影到D中的同一元素。源函数和目标函数（s和t）分别对每个元素使用相应的函数。对于标签函数，选择哪个不重要，我们选择使用来自B的那个。

fun s where ‹s (x,y) = (sB x, sC y)›
fun t where ‹t (x,y) = (tB x, tC y)›
fun l where ‹l (x,_) = lB x›
fun m where ‹m (x,_) = mB x›

有了所有组件，我们现在可以定义最终的pre_graph对象：

definition A where
‹A ≡ (|nodes = V, edges = E, source = s, target = t
,node_label = l, edge_label = m |)›

在随后的代码中，我们使用sublocale关键字来证明我们对拉回对象A的定义是一个有效图。我们接着定义展示拉回图解所需的两个缺失态射。首先，态射A → B通过使用元组的第一个元素来定义。我们通过使用内置函数fst来实现这一点。注意，我们显式地向两个pre_morph对象添加了类型注解，以防止类型被推断为严格类型时出现问题。

definition b :: "(’a × ’g, ’a, ’b × ’h, ’b) pre_morph" where
‹b ≡ (|node_map = fst, edge_map = fst |)›

对于A → C，我们使用另一个投影snd来提取元组的第二个元素。

definition c :: "(’a × ’g, ’g, ’b × ’h, ’h) pre_morph"
where ‹c ≡ (|node_map = snd, edge_map = snd |)›

最后，我们通过使用sublocale机制证明b和c的定义都是有效的态射。证明b: A → B通过展开A和b的定义进行，而c: A → D还需要考虑f和g的标签保持性。

下一个引理表明这个构造产生了一个有效的拉回图解。

引理 2.17 (拉回构造的正确性)。设f: B → D和g: C → D是图态射，设图A和图态射b和c如定义2.16中所定义。则图5中的方形是一个拉回图解。

我们使用sublocale命令，而不是interpretation，来通过标识符pb使这些事实在当前上下文中持久化。

sublocale pb: pullback_diagram A B C D b c f g

证明基本上遵循我们的构造。类似于推出，拉回在同构意义下是唯一的。

定理 2.18 (拉回的唯一性)。设f: B → D和g: C → D连同A诱导了一个拉回，如图5所示。一个图A'连同态射p: A' → B和t: A' → C是f和g的拉回当且仅当存在一个同构u: A' → A使得b ◦ u = p且c ◦ u = t。

该定理在Isabelle/HOL中陈述如下：

theorem uniqueness_pb:
fixes A' b' c'
assumes
A': ‹graph A'› and
b': ‹morphism A' B b'› and
c': ‹morphism A' C c'›
shows ‹pullback_diagram A' B C D b' c' f g
←→ (∃ u. bijective_morphism A' A u
∧ (∀ v ∈ VA'. b ∘→ uV v = b'V v)
∧ (∀ e ∈ EA'. b ∘→ uE e = b'E e)
∧ (∀ v ∈ VA'. c ∘→ uV v = c'V v)
∧ (∀ e ∈ EA'. c ∘→ uE e = c'E e))›

证明与推出的唯一性对偶（参见定理2.12），可以在[EEPT06]中找到。

2.8. 拉回和推出的组合与分解

第3节和第4节即将进行的证明所必需的性质是推出和拉回的组合与分解。

引理 2.19 (推出/拉回组合与分解)。给定图6中的交换图解，则以下陈述成立： (a) 如果(1)和(2)是推出，则(1)+(2)也是推出。 (b) 如果(1)和(1)+(2)是推出，则(2)也是推出。 (c) 如果(1)和(2)是拉回，则(1)+(2)也是拉回。 (d) 如果(2)和(1)+(2)是拉回，则(1)也是拉回。

证明。以下证明基于[EEPT06]： (a) 假设(1)和(2)是推出。通过引理2.6，组合A → B → E和C → D → F是态射。首先证明交换性： A → B → E → F = A → B → D → F (由(2)的交换性) = A → C → D → F (由(1)的交换性) 最后证明泛性质：设X是一个图，且E → X和C → X是态射，使得A → B → E → X = A → C → X。由(1)的泛性质，使用B → E → X和C → X，我们得到唯一的态射D → X。由(2)的泛性质，使用D → X和E → X，我们得到唯一的态射F → X。现在我们首先证明E → F → X = E → X和C → D → F → X = C → X。第一个等式由F → X的构造成立。第二个等式如下： C → D → F → X = C → D → X (由F → X的构造) = C → X (由D → X的构造) 由(2)的泛性质，我们知道F → X是唯一的，使得E → F → X = E → X且D → F → X = D → X。我们将第二个等式两边与态射C → D复合，得到C → D → F → X = C → D → X = C → X，这是由D → X的构造得到的。因此，F → X是唯一的，使得E → F → X = E → X且C → D → F → X = C → X。 (b) 假设(1)和(1)+(2)是推出，并设X是一个图，连同态射D → X和E → X，使得B → E → X = B → D → X。设F → X是由(1)+(2)的泛性质得到的唯一态射，使得E → F → X = E → X且C → D → F → X = C → X。 但我们从(1)的泛性质也知道，D → X是唯一的，使得C → D → X = C → X。 因此，由D → X的唯一性，有D → F → X = D → X。 (c) 证明通过对偶性类似可得。 (d) 证明通过对偶性类似可得。

我们的Isabelle形式化是对给定证明的改编，在保持原始论证精髓的同时，融入了必要的技术修改。推出组合是一个独立的引理，在理论Pushout中定义，参见图1，遵循引理2.19的(a)。

lemma pushout_composition:
assumes
1: ‹pushout_diagram A B C D f g g' f'› and
2: ‹pushout_diagram B E D F e g' e'' e'›
shows ‹pushout_diagram A E C F (e ∘→ f) g e'' (e' ∘→ f')›

这里，f: A → B，g: A → C，g': B → D，f': C → D连同e: B → E，e': D → F，和e'': E → F构成了组合的推出图解。

对于推出分解，我们额外假设(2)是交换的，即e'' ◦ e = e' ◦ g'。在Isabelle中，我们针对B的节点和边独立地表达这一点。

lemma pushout_decomposition:
assumes
e : ‹morphism B E e› and
e': ‹morphism D F e'› and
1 : ‹pushout_diagram A B C D f g g' f'› and
"1+2": ‹pushout_diagram A E C F (e ∘→ f) g e'' (e' ∘→ f')› and
"2cv": ‹⋀v. v ∈ VB =⇒ e'' ∘→ eV v = e' ∘→ g'V v› and
"2ce": ‹⋀ea. ea ∈ EB =⇒ e'' ∘→ eE ea = e' ∘→ g'E ea›
shows ‹pushout_diagram B E D F e g' e'' e'›

在我们的形式化中，拉回的(c)和(d)部分类似于推出的部分。

lemma pullback_composition:
assumes
1: ‹pullback_diagram A B C D f g g' f'› and
2: ‹pullback_diagram B E D F e g' e'' e'›
shows ‹pullback_diagram A E C F (e ∘→ f) g e'' (e' ∘→ f')›

lemma pullback_decomposition:
assumes
f: ‹morphism A B f› and
f': ‹morphism C D f'› and
2: ‹pullback_diagram B E D F e g' e'' e'› and
"1+2": ‹pullback_diagram A E C F (e ∘→ f) g e'' (e' ∘→ f')› and
"1cv": ‹⋀v. v ∈ VA =⇒ g' ∘→ fV v = f' ∘→ gV v› and
"1ce": ‹⋀ea. ea ∈ EA =⇒ g' ∘→ fE ea = f' ∘→ gE ea›
shows ‹pullback_diagram A B C D f g g' f'›

证明类似于[EEPT06，事实2.27]。在下一节中，我们将通过利用目前所使用的基础设施，展示直接推导的结果在同构意义下是唯一的。

3. 直接推导的唯一性

在推理规则应用时，直接推导的唯一性是一个重要性质。本节不依赖于图范畴的黏附性，相反，我们的证明基于[EK79]中图推出的特征刻画。在陈述定理之前，我们介绍一些额外的事实，主要是关于推出和拉回的，这些将在定理3.9的证明中使用。

一般来说，沿着单射态射的推出也是拉回。

引理 3.1 (单射推出是拉回 [EEPT06])。如图3所示的推出图解，如果A → B和A → C是单射的，则它也是拉回。

证明依赖于拉回构造（参见定义2.16）以及拉回是唯一的事实（参见定理2.18）。我们在形式化中的Gluing理论中展示了这个性质（参见图1）。

lemma pushout_pullback_inj_b:
assumes
b: ‹injective_morphism A B b › and
c: ‹injective_morphism A C c ›
shows ‹pullback_diagram A B C D b c f g ›

此外，推出和拉回在某种意义上保持单射性（满射性），即相应图解（见图3和图5）中的对偶态射也是单射的（满射的）。

引理 3.2 (单射和满射态射的保持性 [EEPT06])。给定图3中的推出图解，如果A → B是单射的（满射的），则C → D也是单射的（满射的）。给定图5中的拉回图解，如果C → D是单射的（满射的），则A → B也是单射的（满射的）。

我们使用我们的基础设施，独立于推出、拉回以及单射性或满射性来形式化这些性质。在pushout区域上下文中，如果b: A → B是单射的，则如图3所示的g: C → D也是单射的。

lemma b_inj_imp_g_inj:
assumes ‹injective_morphism A B b ›
shows ‹injective_morphism C D g ›

如果b: A → B是满射的，则g: C → D也是满射的。

lemma b_surj_imp_g_surj:
assumes ‹surjective_morphism A B b ›
shows ‹surjective_morphism C D g ›

因此，如果A → B是双射的，则C → D也是双射的。

lemma b_bij_imp_g_bij:
assumes ‹bijective_morphism A B b ›
shows ‹bijective_morphism C D g ›

拉回的陈述在相应的区域上下文中类似地完成。

某些形式的交换图解可以产生拉回。这个性质在证明推出补的唯一性时使用（参见定理3.9）。

引理 3.3 (特殊拉回 [EEPT06])。如果m是单射的，则图9中的交换图解是一个拉回。

在Isabelle中，我们如下描述这个引理。

lemma fun_algrtr_4_7_2:
fixes C A m
assumes ‹injective_morphism C A m ›
shows ‹pullback_diagram C C C A idM idM m m ›

Isabelle能够使用自动提供的事实完成这个目标。

定义 3.4 (简化链条件 [EK79])。图8中的交换图解满足简化链条件，如果对于所有b' ∈ B和c' ∈ C，满足f(b') = g(c')，则存在a ∈ A使得b(a) = b'且c(a) = c'。

我们证明拉回满足简化链条件。

引理 3.5 (拉回满足简化链条件)。如图5所示的每个拉回图解都满足简化链条件。

我们首先分别针对节点和边证明这个引理，在Isabelle中陈述如下：

lemma reduced_chain_condition_nodes:
fixes x y
assumes ‹x ∈ VB› ‹y ∈ VC› ‹fV x = gV y›
shows ‹∃ a ∈ VA. (bV a = x ∧ cV a = y)›

如果提供相应的事实，Isabelle的简化器能够完成所有目标。特别是，构造也是一个拉回（交换性）以及图A的定义，连同两个态射。随后，我们可以在pullback_diagram区域内陈述一个更一般化的引理：

lemma (in pullback_diagram) reduced_chain_condition_nodes:
fixes x y
assumes ‹x ∈ VB› ‹y ∈ VC› ‹fV x = gV y›
shows ‹∃ a ∈ VA. (bV a = x ∧ cV a = y)›

我们的证明依赖于拉回构造（参见定义2.16）以及拉回是唯一的事实（参见定理2.18）。

定义 3.6 (联合满射性)。给定单射图态射f: B → D和g: C → D。f和g是联合满射的，如果D中的每个项在B或C中都有一个原像。

引理 3.7 (推出是联合满射的)。给定图3中的推出图解，对(f, g)是联合满射的。

我们在Isabelle中为边表达这个性质如下：

lemma joint_surjectivity_edges:
fixes x
assumes ‹x ∈ ED›
shows ‹(∃ e ∈ EC. gE e = x) ∨ (∃ e ∈ EB. fE e = x)›

证明采用反证法。我们使用不相交并集构造图D'，其中包含一个边e ∈ D，使得它在B或C中通过f和g没有原像。我们现在可以构造两个从D'到D的不同态射，这与推出的唯一性矛盾。

定理 3.8 (推出特征刻画 [EK79])。图8中的交换图解是一个推出，如果以下条件成立： (1) 态射b, c, f, g是单射的。 (2) 图解满足简化链条件。 (3) 态射g, f是联合满射的。

lemma po_characterization:
assumes
b: ‹injective_morphism A B b › and
c: ‹injective_morphism A C c › and
f: ‹injective_morphism B D f › and
g: ‹injective_morphism C D g › and
node_commutativity: ‹⋀v. v ∈ VA =⇒ f ∘→ bV v = g ∘→ cV v› and
edge_commutativity: ‹⋀e. e ∈ EA =⇒ f ∘→ bE e = g ∘→ cE e› and
reduced_chain_condition_nodes:
‹⋀x y. x ∈ VB =⇒ y ∈ VC =⇒ fV x = gV y
=⇒ (∃ a ∈ VA. (bV a = x ∧ cV a = y))› and
reduced_chain_condition_edges:
‹⋀x y. x ∈ EB =⇒ y ∈ EC =⇒ fE x = gE y
=⇒ (∃ a ∈ EA. (bE a = x ∧ cE a = y))› and
joint_surjectivity_nodes:
‹⋀x. x ∈ VD =⇒ (∃ v ∈ VC. gV v = x) ∨ (∃ v ∈ VB. fV v = x)› and
joint_surjectivity_edges:
‹⋀x. x ∈ ED =⇒ (∃ e ∈ EC. gE e = x) ∨ (∃ e ∈ EB. fE e = x)›
shows ‹pushout_diagram A B C D b c f g ›

以下定理蕴含了推出补的唯一性，已知如果所用规则中的态射K → L是单射的，即使匹配态射L → G是非单射的，该唯一性也成立[Ros75]。在我们的情况下，两个态射都是单射的。

定理 3.9 (直接推导的唯一性)。设(1)+(2)和(3)+(4)是如图12所示的直接推导。则D ≅ D'且H ≅ H'。

该定理在Isabelle/HOL中于direct_derivation区域内陈述。在assumes部分，引入了第二个直接推导，我们称之为dd2。

theorem uniqueness_direct_derivation:
assumes
dd2: ‹direct_derivation r b b' G g D' d' m H' f' m'›
shows ‹(∃ u. bijective_morphism D D' u)
∧ (∃ u. bijective_morphism H H' u)›

直接推导的唯一性证明（见图12）分两个阶段进行。首先，我们证明推出补的唯一性，这最初由Rosen [Ros75]证明。随后，我们证明给定D和D'之间的双射，推出对象在同构意义下也是唯一的。

定理 3.9。我们证明的第一阶段紧密遵循Lack和Sobocinski [LS04]的方法，除了最后一步，作者在那里依赖于黏附性。我们通过依赖推出特征刻画（参见定理3.8）来完成证明。给定图12中的两个推出图解(1)和(3)，具有单射的K → D和K → D'。为了证明D和D'之间存在双射，我们构造图7中的交换立方体，其中(1)作为底面，(3)作为前左侧面，并证明l和k是双射。对于后者，我们证明后右侧面和顶面是推出。（在[LS04]中，这通过黏附性证明，而我们则使用定理3.8的推出特征刻画来论证。）前右侧面是一个拉回构造（参见定义2.16），我们通过解释pullback_construction区域来告知Isabelle。

interpret fr: pullback_construction D G D' c m ..

我们使用Isabelle的简写符号..来表示标准策略，以完成从假设中得出的证明义务。注意，拉回对象连同两个态射都在区域内指定。后续代码将通过fr.A引用拉回对象，通过fr.b引用态射l，通过fr.c引用k（见图7）。（区域内的标识符由定义给出。因此，前右侧面的拉回对象被称为A，而不是解释参数K。）从引理3.3，在我们的形式化中通过fun_algrtr_4_7_2引用，我们知道后左侧面是一个拉回。

interpret bl: pullback_diagram "interf r" "interf r"
"interf r" "lhs r" idM idM b b
using fun_algrtr_4_7_2[OF r.k.injective_morphism_axioms]
by assumption

为了证明后右侧面是一个拉回，我们从前左侧面开始。由于前左侧面是一个推出且m是单射的，n'也是单射的（参见引理3.2）。由于沿着单射态射的推出也是拉回（参见引理3.1），前左侧面也是一个拉回。使用拉回组合（参见引理2.19），后面是拉回。

interpret backside: pullback_diagram "interf r" D' "interf r" G
‹d' ∘→ idM› idM m ‹g ∘→ b›
using pullback_composition[OF bl.pullback_diagram_axioms
dd2.pb1.flip_diagram]
by assumption

我们使用d和d'态射定义h: K → U为h x = (d x, d' x)，随后证明态射性质。

define h where
‹h ≡ (|node_map = λv. (dV v, d'V v)
,edge_map = λe. (dE e, d'E e)|)›

我们接着证明顶面和底面交换，即d' ◦ id = k ◦ h和g ◦ b = c ◦ d，分别成立。这确立了立方体右侧是拉回的事实。使用拉回分解（参见引理2.19），后右侧面是一个拉回。为了处理顶面，我们首先证明它是一个拉回，随后它也是一个推出。由于m是单射的，从引理3.1我们知道底面也是一个拉回。使用拉回组合（参见引理2.19），底面和后左侧面是一个拉回。通过底面的交换性g ◦ b = c ◦ d和后右侧面的交换性l ◦ h = d ◦ id，前右侧面和顶面是一个拉回。通过拉回分解（参见引理2.19），我们可以证明顶面是一个拉回。我们通过使用推出特征刻画（参见定理3.8）来证明这个拉回也是一个推出。因此，我们需要证明h是单射的，这由上述h的构造得出。

interpret h: injective_morphism "interf r" fr.A h
proof
show ‹inj_on hV Vinterf r›
using d_inj.inj_nodes
by (simp add: h_def inj_on_def)
next
show ‹inj_on hE Einterf r›
using d_inj.inj_edges
by (simp add: h_def inj_on_def)
qed

k和d'的联合满射性由拉回构造以及前左侧面和顶面的简化链条件（参见引理3.4）得出。注意，简化链条件对所有拉回都成立。最后，我们需要证明k和l是双射。由于顶面是一个推出且C → C态射是双射，由引理3.2，k也是双射。

interpret k_bij: bijective_morphism fr.A D' fr.c
using top.b_bij_imp_g_bij[OF r.k.G.idm.bijective_morphism_axioms]
by assumption

为了证明l是双射，我们通过使用推出特征刻画来证明后右侧面是一个推出。l的双射性由推出保持双射的事实得出。我们接着将态射u: D → D'定义为l^{-1}和k的组合。l的逆是通过使用我们形式化中关于双射态射的一个引理获得的，该引理使用obtain关键字陈述了逆的存在性（ex_inv）：

obtain linv where linv:‹bijective_morphism D fr.A linv ›
and ‹⋀v. v ∈ VD=⇒ fr.b ∘→ linvV v = v›
‹⋀e. e ∈ ED=⇒ fr.b ∘→ linvE e = e›
and ‹⋀v. v ∈ Vfr.A=⇒ linv ∘→ fr.bV v = v›
‹⋀e. e ∈ Efr.A=⇒ linv ∘→ fr.bE e = e›
by (metis l_bij.ex_inv)

我们通过将u定义为k ◦ l^{-1}来完成第一阶段，随后证明态射组合保持双射性（使用已证明的bij_comp_is_bij引理）。

define u where ‹u ≡ fr.c ∘→ linv›
interpret u: bijective_morphism D D' u
using bij_comp_bij_is_bij[OF linv k_bij.bijective_morphism_axioms]
by (simp add: u_def)

第二阶段是证明存在一个同构H → H'。我们首先获得u': H → H'和u'': H' → H，并证明它们互逆。我们使用图10中描绘的推出的泛性质，这要求我们证明交换性：f' ◦ b' = m' ◦ u ◦ d。所以我们代入u ◦ d = d'到图12中推出(4)的交换性方程（f' ◦ b' = m' ◦ d'）中。我们得到u ◦ d = d'如下：u ◦ d (1) = k ◦ l^{-1} ◦ d (2) = k ◦ l^{-1} ◦ l ◦ h (3) = k ◦ h (4) = d'。这里，(1)由u的定义保证，(2)由l和h的定义（使得图7中的后右侧面交换）保证，(3)由逆的消去保证，最后(4)由k和h的定义（类似于步骤(2)）保证。我们通过使用图11中描绘的推出的泛性质获得u'': H' → H。我们通过代入u^{-1} ◦ d' = d到图12中推出(2)的交换性方程（f ◦ b' = c' ◦ d）中来证明交换性f ◦ b = c' ◦ u^{-1} ◦ d'：u^{-1} ◦ d' (5) = u^{-1} ◦ u ◦ d (6) = d。这里，(5)由上面证明的方程u ◦ d = d'保证，(6)由逆的消去得出。最后一步是证明u' ◦ u'' = id和u'' ◦ u' = id。为了证明第一个方程，我们从f' = u' ◦ u'' ◦ f'和m' = u' ◦ u'' ◦ m'开始，这些由u'和u''的定义得到。使用图12中推出(4)的泛性质，连同H'，f'，m'，我们得出结论：恒等态射是唯一使得三角形交换的态射H' → H'。如果u' ◦ u''也使三角形交换，那么它就等于恒等态射。第一个三角形交换因为u' ◦ u'' ◦ f' (7) = u' ◦ f (8) = f'。这里，(7)和(8)由u'和u''的相应构造保证（见图10和图11中的三角形）。对于第二个三角形，我们首先使用图10中底部三角形的交换性，并在右侧复合u^{-1}：u' ◦ c' ◦ u^{-1} = m' ◦ u ◦ u^{-1}。通过逆的消去，我们得到u' ◦ c' ◦ u^{-1} = m'，并通过代入使用图11中底部三角形的交换性得到的c' ◦ u^{-1}，我们证明u' ◦ u'' ◦ m' = m'。证明u'' ◦ u' = id类似，为节省篇幅在此省略。

有了直接推导的唯一性（参见定理3.9），我们得到推出补的唯一性。

推论 3.10 (推出补的唯一性)。给定如图3所示的推出，其中A → B是单射的。则图D在同构意义下是唯一的。

为节省空间，我们省略证明。下一节介绍所谓的Church-Rosser定理，它指出并行独立的直接推导具有菱形性质。

4. Church-Rosser定理

Church-Rosser定理指的是两个图变换规则可以彼此独立地应用，无论是顺序地还是并行地，而不会改变最终结果。我们遵循[EEPT06]中给出的直接推导的独立性特征刻画。

定义 4.1 (并行独立性 [EEPT06])。图14中的两个直接推导G ⇒_{p1,m1} H1和G ⇒_{p2,m2} H2是并行独立的，如果存在态射L1 → D2和L2 → D1，使得L1 → D2 → G = L1 → G且L2 → D1 → G = L2 → G。

locale parallel_independence =
p1: direct_derivation r1 b1 b1' G g1 D1 m1 c1 H1 f1 h1 +
p2: direct_derivation r2 b2 b2' G g2 D2 m2 c2 H2 f2 h2
for r1 b1 b1' G g1 D1 m1 c1 H1 f1 h1
r2 b2 b2' g2 D2 m2 c2 H2 f2 h2 +
assumes
i: ‹∃ i. morphism (lhs r1) D2 i
∧ (∀ v ∈ Vlhs r1. c2 ∘→ iV v = g1V v)
∧ (∀ e ∈ Elhs r1. c2 ∘→ iE e = g1E e)› and
j: ‹∃ j. morphism (lhs r2) D1 j
∧ (∀ v ∈ Vlhs r2. c1 ∘→ jV v = g2V v)
∧ (∀ e ∈ Elhs r2. c1 ∘→ jE e = g2E e)›

定义 4.2 (顺序独立性 [EEPT06])。图15中的两个直接推导G ⇒_{p1,m1} H1和H1 ⇒_{p2,m2} H2是顺序独立的，如果存在态射R1 → D2和L2 → D1，使得R1 → D2 → H = R1 → H且L2 → D1 → H = L2 → H。

locale sequential_independence =
p1: direct_derivation r1 b1 b1' G g1 D1 m1 c1 H1 f1 h1 +
p2: direct_derivation r2 b2 b2' H1 g2 D2 m2 c2 H2 f2 h2
for r1 b1 b1' G g1 D1 m1 c1 H1 f1 h1
r2 b2 b2' g2 D2 m2 c2 H2 f2 h2 +
assumes
i: ‹∃ i. morphism (rhs r1) D2 i
∧ (∀ v ∈ Vrhs r1. c2 ∘→ iV v = f1V v)
∧ (∀ e ∈ Erhs r1. c2 ∘→ iE e = f1E e)› and
j: ‹∃ j. morphism (lhs r2) D1 j
∧ (∀ v ∈ Vlhs r2. h1 ∘→ jV v = g2V v)
∧ (∀ e ∈ Elhs r2. h1 ∘→ jE e = g2E e)›

定理 4.3 (Church-Rosser定理 [EK76])。给定两个并行独立的直接推导G ⇒_{p1,m1} H1和G ⇒_{p2,m2} H2，存在一个图G'连同顺序独立的直接推导H1 ⇒_{p2,m'_2} G'和H2 ⇒_{p1,m'_1} G'。

实际上，我们证明了更多，即G ⇒_{p1,m1} H1 ⇒_{p2,m'_2} G'和G ⇒_{p2,m2} H2 ⇒_{p1,m'_1} G'是顺序独立的。我们在parallel_independence区域内于Isabelle/HOL中表达该定理如下：

theorem (in parallel_independence) church_rosser:
shows ‹∃ g' D' m' c' H' f' h' g'' D'' m'' c'' H'' f'' h''.
sequential_independence r1 b1 b1' G g1 D1 m1 c1 H1 f1 h1 r2
b2 b2' g' D' m' c' H' f' h'
∧ sequential_independence r2 b2 b2' G g2 D2 m2 c2 H2 f2 h2 r1
b1 b1' g'' D'' m'' c'' H'' f'' h''›

定理 4.3。我们紧密遵循Ehrig和Kreowski [EK76]的原始证明，其中第一阶段，图14中的推出(1)-(4)被垂直分解为推出(11)+(12)，(21)+(22)，(31)+(32)和(41)+(42)，如图16所示。在第二阶段，这些推出被重新排列，如图17所示，并构造新的推出(5)。随后，我们证明两个垂直推出(11)和(12)。推出(31)和(32)类似可得，为节省空间未展示。

我们从构造拉回(12)开始，将其绑定到符号c12，以便后续引用，使用我们的pullback_construction区域。

interpret "c12": pullback_construction D1 G D2 c1 c2 ..

K1 → D的存在性由泛性质得出，D → D2由拉回(12)的构造得出：

obtain j1 where ‹morphism (interf r1) c12.A j1›
and ‹⋀v. v∈Vinterf r1 =⇒ c12.b ∘→ j1V v = m1V v›
‹⋀e. e∈Einterf r1 =⇒ c12.b ∘→ j1E e = m1E e›
and ‹⋀v. v∈Vinterf r1 =⇒ c12.c ∘→ j1V v = i1 ∘→ b1V v›
‹⋀e. e∈Einterf r1 =⇒ c12.c ∘→ j1E e = i1 ∘→ b1E e›
using c12.pb.universal_property_exist_gen[OF p1.r.k.G.graph_axioms
wf_b1i1.morphism_axioms p1.po1.c.morphism_axioms a b]
by fast

从(1) = (11) + (12)的事实，我们知道(11)+(12)是一个推出，并且由于K1 → L1是单射的，它也是一个拉回（参见引理3.1）。通过拉回分解（参见引理2.19），(11)是一个拉回。我们使用推出特征刻画（参见定理3.8）来证明它也是一个推出，这要求我们证明所有态射的单射性、简化链条件以及D → D2和L1 → D2的联合满射性。K1 → L1的单射性已给定，D → D2的单射性由推出(1)和K1 → L1的单射性得出（参见引理3.2）。为了证明L1 → D2的单射性，我们使用并行独立性（参见定义4.1）L1 → D2 → G = L1 → G和L1 → G的单射性。为了证明K1 → D的单射性，我们使用通过拉回(12)的泛性质得到的三角形L1 → D2 → G = L1 → G以及L1 → G和D2 → G两者的单射性。简化链条件由引理3.5得出。为了证明D → D2和L1 → D2的联合满射性（即D2中的每个x在D或L1中都有一个原像）。设y是x在G中的像。我们将推出(11)+(12)的联合满射性应用于y，即y在D1或L1中有一个原像。在前一种情况（y在D1中有原像z）：从拉回构造（参见定义2.16），我们在D中得到z和x的共同原像，这证明了前一种情况。在后一种情况，y通过D2在L1中有一个原像。由于D2 → G是单射的，该原像通过x被映射，这意味着x在L1中有一个原像。这证明了后一种情况。

推出(21)，(41)使用gluing区域构造（详细描述见[SP22]）。

interpret "c21": gluing "interf r1" c12.A "rhs r1" j1 b1' ..
interpret "c41": gluing "interf r2" c12.A "rhs r2" j2 b2' ..

D2 → H1和D1 → H2的存在性分别由推出(21)和(41)的泛性质得出。推出(22)和(42)通过使用推出分解得到（参见引理2.19）。这完成了证明的第一阶段。第二阶段重新排列推出，如图17所示，从而我们获得两个直接推导H1 ⇒_{p2,m'_2} G'和H2 ⇒_{p1,m'_1} G'。这里，我们组合来自第一阶段的推出（参见引理2.19）。例如，推出(31)和(22)在Isabelle/HOL中组合如下。

interpret "31+22": pushout_diagram "interf r2" c21.H "lhs r2" H1
"c21.c ∘→ j2" b2 s1 "h1 ∘→ i2"
using pushout_composition[OF "31.flip_diagram" "22.flip_diagram"]
by assumption

最终推出(5)被构造，推出被重新排列并垂直组合，如图17所示。Isabelle在此刻能够自动完成目标，因为我们实例化了所有必需的区域。顺序独立性由构造得出。这完成了证明的第二阶段。

在开发证明的过程中，我们通过仔细地以正确的顺序用正确的参数实例化区域，手动地规划了证明结构。这个过程由于涉及大量的类型参数而具有挑战性。然而，Isabelle的类型检查器通过在我们尝试以错误顺序实例化参数时捕获错误，提供了一些支持，帮助指导证明开发过程。

尽管有这种帮助，整体的证明结构是手动开发的，策略仅用于特定的子目标。手动方法使我们能够保持对证明流程的控制，并确保推理保持清晰易懂。虽然类型参数增加了证明的复杂性，但它们也提供了一种宝贵的保护，防止因错误顺序的实例化可能导致长时间调试的潜在不一致性。

5. 相关工作

Strecker [Str18] 使用Isabelle/HOL对图变换进行交互式推理。与我们工作的一个主要区别是，他引入了一种图变换形式，该形式与任何已建立的方法（如双推重写方法）都不匹配。因此，他的框架无法借鉴现有理论。另一个区别是，[Str18]侧重于验证某种形式的图程序的一阶性质，而当前论文关注的是形式化和证明DPO理论的基本结果。Strecker的形式化将节点和边标识符固定为自然数，而我们则保持它们抽象。与我们的开发类似，Isabelle的区域机制被使用。

我们对图的形式化遵循了Noschinski [Nos15]的工作，其中使用记录来分组组件，使用区域来强制性质，例如图或态射的良构性。[Nos15]的主要目标是形式化并证明经典图论的基本结果，如库拉托夫斯基定理。

Stark [Sta16] 在Isabelle/HOL中发展了一个"无对象"的范畴定义，这简化了范畴的规约，并允许将函子和自然变换定义为满足某些公理的函数。这里，主要关注点是在高阶逻辑中高效地表示抽象代数。这种方法的一个限制是必须定义一个特殊的零元素。因此，该形式化阻止了在整个宇宙上构建离散范畴，而是需要一个足够大的基类型。我们采用了一种更传统的方法来形式化范畴论相关概念，但不得不处理先前讨论的单宇宙和显式量化限制。

da Costa Cavalheiro等人 [dCCFR17] 使用Event-B规约方法及其相关的定理证明器来推理双推重写和单推重写图变换，其中规则可以具有属性和否定应用条件。Event-B基于一阶逻辑和类型化集合论。与我们的方法不同，[dCCFR17] 仅给出了推出的抽象定义与其集合论构造之间等价性的非形式化证明。相比之下，我们将抽象和操作视图都形式化，并使用Isabelle/HOL证明了它们的对应关系。由于Event-B基于一阶逻辑，可以表达和验证的性质相当有限。众所周知，有限图的非局部性质无法在一阶逻辑中描述[Lib04]。这个限制不适用于我们的形式化，因为我们可以充分利用高阶逻辑。

6. 结论

在本文中，我们显著推进了使用Isabelle证明助手（依赖其高阶逻辑实例化）对基本DPO图变换理论的形式化。我们详尽阐述了DPO理论的两个关键结果：直接推导的唯一性和Church-Rosser定理。我们的讨论包括一系列关键的引理，这些引理共同构建了最终证明。

我们还深入探讨了形式化的技术层面，包括全函数和偏函数、有限集和有限映射的应用。我们的方法在表达力和自动化支持之间取得了平衡。虽然有限集（映射）在某些证明中具有优势，但它们缺乏全面的引理集，需要我们在部分内容中投入大量的额外实现和证明工作。此外，为节点和边使用统一标识符的想法，虽然最初很有吸引力，但在我们的构造中导致了增加的复杂性，如第2节所述。这种复杂性延伸到了整个粘合和删除过程，影响了我们使用此构造所证明的性质。

展望未来，我们的目标是扩展我们的方法，以包含带属性的DPO图变换，如[HP16]所述。我们的长期目标是开发一个GP 2证明助手，能够实现对单个图程序的交互式验证。该工具可能会利用[WP21]中提出的证明演算，为图程序验证领域带来重大进展。

致谢 我们感谢Brian Courthoute、Annegret Habel和Thomas Türk就本文主题进行的讨论。

参考文献

References
[ADGR07] Jeremy Avigad, Kevin Donnelly, David Gray, and Paul Raff. A formally verified proof of
the prime number theorem. ACM Transactions on Computational Logic, 9(1):2, 2007. doi:
10.1145/1297658.1297660.
[Bal21] Clemens Ballarin. Tutorial to locales and locale interpretation, 2021. URL: https://isabelle.
in.tum.de/doc/locales.pdf, arXiv:https://isabelle.in.tum.de/doc/locales.pdf.
[BH18] Achim D. Brucker and Michael Herzberg. A Formal Semantics of the Core DOM in Isabelle/HOL.
In Companion Proceedings of the The Web Conference 2018, WWW ’18, page 741–749. International World Wide Web Conferences Steering Committee, 2018. doi:10.1145/3184558.3185980.
[CCP22] Graham Campbell, Brian Courtehoute, and Detlef Plump. Fast rule-based graph programs.
Science of Computer Programming, 214, 2022. doi:10.1016/j.scico.2021.102727.
[dCCFR17] Simone André da Costa Cavalheiro, Luciana Foss, and Leila Ribeiro. Theorem proving graph
grammars with attributes and negative application conditions. Theoretical Computer Science,
686:25–77, 2017. doi:10.1016/j.tcs.2017.04.010.
[Dí20] Javier Díaz. Finite map extras. Archive of Formal Proofs, October 2020. https://isa-afp.org/
entries/Finite-Map-Extras.html.
[EEPT06] Hartmut Ehrig, Karsten Ehrig, Ulrike Prange, and Gabriele Taentzer. Fundamentals of Algebraic
Graph Transformation. Monographs in Theoretical Computer Science. Springer, 2006. doi:
10.1007/3-540-31188-2.
[Ehr79] Hartmut Ehrig. Introduction to the algebraic theory of graph grammars. In Proc. GraphGrammars and Their Application to Computer Science and Biology, volume 73 of Lecture Notes
in Computer Science, pages 1–69. Springer-Verlag, 1979. doi:10.1007/BFb0025714.
3:36 R. Söldner and D. Plump Vol. 20:4
[EK76] Hartmut Ehrig and Hans-Jörg Kreowski. Parallelism of manipulations in multidimensional
information structures. In Proc. Mathematical Foundations of Computer Science (MFCS 1976),
volume 45 of Lecture Notes in Computer Science, pages 284–293. Springer, 1976.
[EK79] Hartmut Ehrig and Hans-Jörg Kreowski. Pushout-properties: An analysis of gluing constructions
for graphs. Mathematische Nachrichten, 91:135–149, 1979.
[Gon07] Georges Gonthier. The four colour theorem: Engineering of a formal proof. In Proc. Asian
Symposium on Computer Mathematics (ASCN 2007), volume 5081 of Lecture Notes in Computer
Science, page 333. Springer, 2007. doi:10.1007/978-3-540-87827-8\\_28.
[HAB+15] Thomas Hales, Mark Adams, Gertrud Bauer, Dat Tat Dang, John Harrison, Truong Le Hoang,
Cezary Kaliszyk, Victor Magron, Sean McLaughlin, Thang Tat Nguyen, Truong Quang Nguyen,
Tobias Nipkow, Steven Obua, Joseph Pleso, Jason Rute, Alexey Solovyev, An Hoai Thi Ta,
Trung Nam Tran, Diep Thi Trieu, Josef Urban, Ky Khac Vu, and Roland Zumkeller. A formal
proof of the Kepler conjecture. Forum of Mathematics, Pi, 5, 2015. doi:10.1017/fmp.2017.1.
[HK13] Brian Huffman and Ondřej Kunčar. Lifting and transfer: A modular design for quotients in
Isabelle/HOL. In Certified Programs and Proofs: Third International Conference, CPP 2013,
Proceedings 3, pages 131–146, 2013. doi:10.1007/978-3-319-03545-1_9.
[HMP01] Annegret Habel, Jürgen Müller, and Detlef Plump. Double-pushout graph transformation
revisited. Mathematical Structures in Computer Science, 11(5):637–688, 2001. doi:10.17/
S0960129501003425.
[HP16] Ivaylo Hristakiev and Detlef Plump. Attributed graph transformation via rule schemata: ChurchRosser theorem. In Software Technologies: Applications and Foundations – STAF 2016 Collocated
Workshops, Revised Selected Papers, volume 9946 of Lecture Notes in Computer Science, pages
145–160. Springer, 2016. doi:10.1007/978-3-319-50230-4_11.
[HR04] Michael Huth and Mark Dermot Ryan. Logic in Computer Science – Modelling and Reasoning
about Systems. Cambridge University Press, 2nd edition, 2004.
[HUW14] John Harrison, Josef Urban, and Freek Wiedijk. History of Interactive Theorem Proving. In
Handbook of the History of Logic, volume 9, pages 135–214. Elsevier, 2014. doi:10.1016/
B978-0-444-51624-4.50004-6.
[KEH+09] Gerwin Klein, Kevin Elphinstone, Gernot Heiser, June Andronick, David A. Cock, Philip Derrin,
Dhammika Elkaduwe, Kai Engelhardt, Rafal Kolanski, Michael Norrish, Thomas Sewell, Harvey
Tuch, and Simon Winwood. seL4: formal verification of an OS kernel. In Proc. Symposium on
Operating Systems Principles (SOSP 2009), pages 207–220. ACM, 2009. doi:10.1145/1629575.
1629596.
[Ler09] Xavier Leroy. Formal verification of a realistic compiler. Communications of the ACM, 52(7):107–
115, 2009. doi:10.1145/1538788.1538814.
[Lib04] Leonid Libkin. Elements of Finite Model Theory. Texts in Theoretical Computer Science. Springer,
2004. doi:10.1007/978-3-662-07003-1.
[LS04] Stephen Lack and Paweł Sobociński. Adhesive categories. In Proc. Foundations of Software
Science and Computation Structures (FoSSaCS 2004), volume 2987 of Lecture Notes in Computer
Science, pages 273–288. Springer, 2004. doi:10.1007/978-3-540-24727-2\\_20.
[NK14] Tobias Nipkow and Gerwin Klein. Concrete semantics: with Isabelle/HOL. Springer, 2014.
doi:10.1007/978-3-319-10542-0.
[Nos15] Lars Noschinski. A graph library for Isabelle. Mathematics in Computer Science, 9(1):23–39,
2015. doi:10.1007/s11786-014-0183-z.
[Plu16] Detlef Plump. Reasoning about graph programs. In Proc. Computing with Terms and Graphs
(TERMGRAPH 2016), volume 225 of Electronic Proceedings in Theoretical Computer Science,
pages 35–44, 2016. doi:10.4204/EPTCS.225.6.
[PNW19] Lawrence C. Paulson, Tobias Nipkow, and Makarius Wenzel. From LCF to Isabelle/HOL. Formal
Aspects of Computing, 31(6):675–698, 2019. doi:10.1007/s00165-019-00492-1.
[Ros75] Barry K. Rosen. Deriving graphs from graphs by applying a production. Acta Informatica,
4:337–357, 1975.
[SP22] Robert Söldner and Detlef Plump. Towards mechanised proofs in double-pushout graph transformation. In Proc. International Workshop on Graph Computation Models (GCM 2022),
volume 374 of Electronic Proceedings in Theoretical Computer Science, pages 59–75, 2022.
doi:10.4204/EPTCS.374.6.
Vol. 20:4 FORMALISING THE DOUBLE-PUSHOUT APPROACH TO GRAPH TRANSFORMATION 3:37
[SP23] Robert Söldner and Detlef Plump. Mechanised DPO Theory: Uniqueness of Derivations
and Church-Rosser Theorem. In Proc. International Conference on Graph Transformation
(ICGT 2023), Lecture Notes in Computer Science, pages 123–142. Springer, 2023. doi:
10.1007/978-3-031-36709-0_7.
[Sta16] Eugene W. Stark. Category theory with adjunctions and limits. Archive of Formal Proofs, June
2016. https://isa-afp.org/entries/Category3.html, Formal proof development.
[Str18] Martin Strecker. Interactive and automated proofs for graph transformations. Mathematical
Structures in Computer Science, 28(8):1333–1362, 2018. doi:10.1017/S096012951800021X.
[SW09] Norbert Schirmer and Makarius Wenzel. State spaces – the locale way. In Proc. International
Workshop on Systems Software Verification (SSV 2009), volume 254 of Electronic Notes in
Theoretical Computer Science, pages 161–179, 2009. doi:10.1016/j.entcs.2009.09.065.
[Wen] Makarius Wenzel. The Isabelle/Isar Reference Manual. https://isabelle.in.tum.de/doc/
isar-ref.pdf.
[Wen99] Markus Wenzel. Isar — A generic interpretative approach to readable formal proof documents.
In Theorem Proving in Higher Order Logics (TPHOLs 1999), volume 1690 of Lecture Notes in
Computer Science, pages 167–183. Springer, 1999. doi:10.1007/3-540-48256-3_12.
[WP21] Gia S. Wulandari and Detlef Plump. Verifying graph programs with monadic second-order logic. In
Proc. International Conference on Graph Transformation (ICGT 2021), volume 12741 of Lecture
Notes in Computer Science, pages 240–261. Springer, 2021. doi:10.1007/978-3-030-78946-6\\
_13.
https://arxiv.org/pdf/2312.15641