掘金 后端 ( ) • 2024-07-01 08:52

可逆计算理论提出了一个通用的软件构造公式

App = Delta x-extends Generator<DSL>

Nop平台的整个实现可以看作是对这个公式的一种具体落地实践。这其中,最关键也是最容易引起误解的部分是可逆计算理论中的差量概念,也就是上面公式中的Delta。

详细介绍参见可逆计算:下一代软件构造理论

可逆计算可以看作是针对差量概念的一个系统化的完整理论,所以业内目前常见的基于差量概念的实践都可以在可逆计算理论的框架下得到诠释。我在举例时经常会提到git和docker,比如

问: 什么是Delta? 每一次git的commit是不是一个delta?

答:git是定义在通用的行空间上,所以它用于领域问题是不稳定的,领域上的等价调整会导致行空间中的合并冲突。类似的还有Docker技术。很多年以前就有python工具能管理依赖,动态生成虚拟机。这里本质性的差异就在于虚拟机的差量是定义在无结构的字节空间中,而docker是定义在结构化的文件空间中。

有些人读到上面的文字后感觉有点被绕晕了。"类似的还有Docker技术" 这句话到底是在说这两种本质上是一样的?还是想说它们本质上不一样?

这里确实需要一些更详尽的解释。虽然都叫做差量,但是差量和差量之间仍然有着非常深刻的区别。总的来说git和docker本质上都涉及到差量计算,但是它们所对应的差量也有着本质上不同的地方,这里的精细的差异需要从数学的角度才能解释清楚。一般人对于差量概念的理解其实是望闻生义,存在着非常多的含混的地方,所以很多的争论本质上是因为定义不清导致的,而不是这个问题本身内在的矛盾导致的。

可逆计算理论对差量的理解和使用在数学层面上其实非常简单,只是它的应用对象不是一般人习以为常的数值或者数据,导致没有经过专门抽象训练的同学一时转不过来弯而已。

因为有些同学反映对于此前文章中提到的数学名词感觉懵懵懂懂,所以在本文中我会尝试补充一些更详细的概念定义和实例分析。如果仍然有感觉不清楚的地方,欢迎加入Nop平台的讨论群继续提问,讨论群的二维码见微信公众号的菜单。

一. 差量的普适性和存在性

在数学和物理领域,当我们提出一个新的概念时,第一步就是论证它的普适性和存在性。所以可逆计算对于差量概念的第一个关键性理解是:差量是普遍存在的

A = 0 + A

任何一个存在单位元的系统都可以很自然的定义出差量:任何一个全量都等价于单位元+自身,也就是说任何一个全量都是差量的特例。而单位元这个概念在一般情况下是自然存在的,比如什么都不干的情况下对应于空操作,而空操作和任何其他操作结合在一起都等价于这个操作本身,因此空操作就是一个自然存在的单位元。

很多人听到全量是差量的特例这句话之后可能会感到很疑惑,这很显然,但是它有什么意义吗?一般人无法将数学原理和真实的物理世界联系起来,导致他们会认为数学的精确定义是无用的。这里有个很关键的推论是这样的:既然全量是差量的特例,那么原则上全量可以采用和差量一模一样的形式,没有必要为了表达差量,单独设计一个不同的差量形式。比如说,JSON格式的差量可以用JSON Patch语法来表达,但是JSON Patch的格式与原始的JSON格式大相径庭,它这个差量形式就是特制的,而不是与全量格式保持一致的。

[
  {
    "op": "add",
    "path": "/columns/-",
    "value": {
      "name": "newColumn",
      "type": "string", // 或者其他数据类型
      "primary": false // 是否为主键
    }
  },
  {
     "op": "remove",
     "path": "/columns/2"
   }
]

Nop平台中的做法是:

<table name="my_table">
   <columns>
     <column name="newColumn" type="string" primary="false" />
     <column name="column2" x:override="remove" />
   </columns>
</table>

或者使用JSON格式

{
    "type": "table",
    "name": "my_table",
    "columns": [
       {
          "type": "column",
          "name": "newColumn",
          "type": "string",
          "primary": false
       },
       {
         "name": "column2",
         "x:override": "remove"
       }
    ]
}

JSON Patch的格式与原始JSON的格式是完全不同的,而且只能使用下标来标记列表中的行,而Nop中的Delta合并是通过name等唯一属性来定义行,在语义层面更加稳定(插入一行不会影响到所有后续行的定位),而且差量的格式与原始格式完全一致,只是额外引入了一个x:override属性。

在Nop平台中我们系统化的贯彻了全量是差量的一个特例的数学思想,各种需要表达差量的地方,比如前台提交到后台的修改数据、后台提交到数据库的变更数据等,我们全部采用所谓的同构设计,即提交的差量数据结构和普通的领域对象结构基本一致,通过少量扩展字段来表达新增、删除等信息。

认识到全量是差量的一个特例之后,还可以破除一个常见的误解:差量是一些局部的小的变化,实际上差量完全可以大到这个系统。在存在逆元的情况下,差量甚至可以比整体还要大!

二. 不同的空间有不同的差量定义

现代抽象数学所带来的一个关键性认知是:运算规则是与某个空间绑定的。因为我们在中学所学的数学规则都是应用在自然数、有理数、实数这种习以为常的数值空间中,所以大部分人没有意识到运算规则仅在它对应的空间中有效,而且在定义的时候,运算规则和它所作用的空间就是作为一个整体来定义的。在数学中,包含单位元和逆元概念的最小化的数学结构是群(Group),下面我们就仔细分析一下群的定义。智谱清言AI给出的标准定义如下: 一个群 $ (G, *) $ 由一个集合 $ G $ 和一个二元运算 $ *: G \times G \rightarrow G $ 组成,使得以下四个条件成立:

  1. 封闭性(Closure):对于所有 $ a, b \in G $,$ a * b $ 也在 $ G $ 中。
  2. 结合性(Associativity):对于所有 $ a, b, c \in G $,有 $ (a * b) * c = a * (b * c) $。
  3. 单位元(Identity Element):存在一个元素 $ e \in G $,对于所有 $ a \in G $,有 $ e * a = a * e = a $。这个元素 $ e $ 被称为群的单位元。
  4. 逆元(Inverse Elements):对于每个 $ a \in G $,存在一个元素 $ a^{-1} \in G $,使得 $ a * a^{-1} = a^{-1} * a = e $。这个元素 $ a^{-1} $ 被称为 $ a $ 的逆元。

首先我们注意到,在群的定义中,基础的集合G和它上面的运算*是一个整体,单独的G和单独的运算都无法构成群。但是在日常交流中,我们一般会将群$(G, *)$简称为群G,这可能会给一些人造成误导。

群定义中的*仅仅是一种抽象的符号标识,它并不代表乘法。在不同的空间中我们可以定义不同的运算,而在不同的运算中单位元和逆元的定义也是不同的。比如说,实数空间$\mathbb{R}$ 上的加法和乘法各自构成群,但它们不是同一个群的运算。下面是智谱清言AI给出的详细定义,

  1. 加法群 $(\mathbb{R}, +)$:

    • 封闭性:对于所有$a, b \in \mathbb{R}$,a + b 也在$\mathbb{R}$ 中。
    • 结合性:对于所有$a, b, c \in \mathbb{R}$,有$(a + b) + c = a + (b + c)$。
    • 单位元:存在一个元素$0 \in \mathbb{R}$,对于所有$a \in \mathbb{R}$,有$0 + a = a + 0 = a$。这个元素$0$ 是加法的单位元。
    • 逆元:对于每个$a \in \mathbb{R}$,存在一个元素$-a \in \mathbb{R}$,使得$a + (-a) = (-a) + a = 0$。这个元素$-a$ 是$a$ 的加法逆元。 因此,实数空间$\mathbb{R}$ 在加法运算下构成了一个群,称为加法群。
  2. 乘法群 $(\mathbb{R}^*, \cdot$):

    注意,乘法群不包括零,因为零没有乘法逆元。因此,我们考虑的是非零实数构成的集合$\mathbb{R}^*$。

    • 封闭性:对于所有$a, b \in \mathbb{R}^$,$a \cdot b$ 也在$\mathbb{R}^$ 中。
    • 结合性:对于所有$a, b, c \in \mathbb{R}^*$,有$(a \cdot b) \cdot c = a \cdot (b \cdot c)$。
    • 单位元:存在一个元素$1 \in \mathbb{R}^$,对于所有$a \in \mathbb{R}^$,有$1 \cdot a = a \cdot 1 = a$。这个元素$1$ 是乘法的单位元。
    • 逆元:对于每个$a \in \mathbb{R}^$,存在一个元素$a^{-1} \in \mathbb{R}^$,使得$a \cdot a^{-1} = a^{-1} \cdot a = 1$。这个元素$a^{-1}$ 是$a$ 的乘法逆元。 因此,非零实数构成的集合$\mathbb{R}^*$ 在乘法运算下构成了一个群,称为乘法群。

可逆计算理论中的差量概念,本质上是来源于群的思想的启发,因此对于每一种差量,我们总是可以仿照群的定义,从以下的几个方面进行分析:

  1. 差量运算是在哪个空间中定义的?

  2. 差量运算的结果是否仍然在这个空间中?

  3. 差量运算是否满足结合律?能否先执行局部的运算,然后再和整体进行结合?

  4. 差量运算的单位元是什么?

  5. 差量运算是否支持逆运算?逆元的形式是什么?

三. Git中的差量运算

1. Git的差量运算是在哪个空间中定义的?

Git的diff功能是把文本文件先拆分成行,然后再对文本行的列表进行比较。因此,Git的差量结构空间可以看作是行文本空间。这是一个通用的差量结构空间。每一个文本文件都可以映射到行文本空间中成为一个行文本列表,换句话说,每一个文本文件在行文本空间中都有一个属于自己的表象(Representation)。

2. Git的差量运算的结果是否仍然在行文本空间中?

Git的apply功能可以将patch差量文件应用到当前的文本文件之上,得到的仍然是一个”合法的“文本文件。但是如果细究起来,这里的合法性并不是那么牢靠。

首先,Git中的patch具有很强的特异性,它与自己的应用目标是紧密捆绑在一起的。比如说,从项目A构造出来的patch无法直接应用到另外一个不相关的项目B上。一个patch就是针对一个指定版本(状态)的base文件。在这种情况下,我们很难认为patch在概念层面是一种独立的实体,存在独立的价值。

第二,多个patch应用到同一个base文件之上时可能会出现冲突,在冲突的文件中我们会改变文件原始的结构,插入如下标记内容:

  • <<<<<<< HEAD:标记当前分支(通常是你的目标分支,即HEAD所指向的分支)的内容开始。
  • =======:分隔当前分支和被合并分支的内容。
  • >>>>>>> [分支名]:标记被合并分支(通常是你要合并的分支)的内容开始。

出现冲突的本质原因是差量运算超出了原定的结构空间,产生了某种异常结构。这种结构并不在原先合法结构的定义范围之内。

第三,即使多个patch没有发生冲突,合并后的结果也可能破坏源文件应有的语法结构。导致合并的结果虽然是一个”合法的“的行文本文件,但是它却不是一个合法的源码文件。为了保证合并结果一定具有合法的语法结构,我们必然是需要在抽象语法树的结构空间中进行合并

在群定义的四大天条中,排在第一条的就是所谓的封闭性,这无疑是在暗示着它无可辩驳的重要性。但是一般没有受过抽象数学训练的同学却经常会忽略这一点。封闭性很重要吗?不封闭会死吗?数学的力量来自于连续的自动化推理,如果在推理的过程中随时可能突破到已知空间之外,进入某种未知状态,那就意味着数学推理的大厦随时可能会发生坍塌,唯一的指望只能是祈祷幸运女神的伴随和祈求上帝的救赎(程序员手工编辑冲突内容类似于上帝之手的介入)。

3. Git中的差量运算是否满足结合律?

如果我们手里有多个patch文件,patch1、patch2、patch3...,这些小的patch文件能否被合并成一个大的patch文件?如果可以合并,得到的结果与合并的顺序有关吗? (patch1 + patch2) + patch3与 patch1 + (patch2 + patch3)的结果是否等价?

如果Git的差量满足结合律,那就意味着我们可以在独立于base文件的情况下实现patch文件的合并,比如说通过如下指令实现合并patch。

git merge-diff patch1.patch,patch2.patch > combined.patch

但很可惜,实际情况是,以上指令并不存在。Git合并多个patch时,必须逐个将patch应用到base文件上,然后再反向生成diff。

git apply --3way patch1.patch
git apply --3way patch2.patch
git diff > combined.patch

结合律是数学领域中一条特别基本的普适规律,现有的各种主要数学理论全部预设了结合律的存在(包括号称最纯粹、最泛化的范畴论)。在数学的世界中,没有结合律几乎是寸步难行。

我所知道的唯一的不满足结合律的数学对象是八元数(octonions)。八元数是四元数(quaternions)的扩展,而四元数是复数的扩展。八元数目前只有一些很小众的应用。

结合律为什么重要?首先,结合律使得我们可以实现局域化的认知。在存在结合律的情况下,我们不需要考虑本体的存在,不需要考虑离我们很远的推理链条中发生的事情,只要将全部精力放到直接与自己发生相互作用的对象上就好了。只要研究清楚了一个对象可以和哪些元素结合,它们之间发生结合运算之后产生的结果是什么,那么在范畴论的意义上就是彻底掌握了关于这个对象的一切知识(在马克思主义哲学中,这对应于人是他所参与的一切生产关系的总和)。

第二,结合律使得复用成为可能。我们可以将相邻的几个对象预先结合在一起,形成一个完整的、具有独立语义的新的元素。

x = a + b + c = a + (b+c) = a + bc
y = m + b + c = m + bc

在上面的例子中,在构造x和y的过程中我们可以复用预结合产生的对象bc。但是很有趣的是,如果复用真的能够发生作用,那么要求同样的对象可以和很多对象结合。比如 a+bcm+bc。但是,在Git的差量运算中,patch没有这样的自由可结合性,它只能应用于固定版本的base文件,因此基本上可以认为它不具备可复用性

... + a + b + c + ...  
    == ... + (a + (b + c)) + ... 
    == ... + ((a + b) + c) + ...

满足结合律意味着可以自由的选择是否与临近的对象结合,决定先进行左结合还是先进行右结合,亦或是不结合等着别人主动来结合。在形式上,这意味着我们可以随时在计算序列中插入或者删除括号,计算的顺序不影响最终得到的结果。因此,结合律的第三个作用是,为性能优化创造了可能性

function f(x){
    return g(h(x))
}

函数运算满足结合律,因此编译期在编译的时候可以直接分析函数gh的代码,抽取出它们的实现指令,然后在完全不了解函数f的调用环境的情况下,对gh的指令进行合并优化。此外,结合律也为并行优化创造了可能性。

a + b + c + d = (a + b) + (c + d) = ab + cd

在上面的例子中,我们可以同时计算a+bc+d。很多快速算法都依赖于结合律所提供的这种优化可能性。

4. Git的差量运算的单位元和逆元是什么?

Git的差量运算的单位元显然就是一个空的patch文件,它表示什么都不做。有些同学可能会感到奇怪,既然单位元什么都不做了,那它还有什么存在的必要性吗?首先,我们需要了解一下单位元的特殊性:单位元一旦存在,它就会无处不在

$$ ab = eeeaeebeee $$

在任何对象的前后都可以插入任意数量的单位元。这意味着表面上看起来a和b是直接发生相互作用,实际上它们是浸泡在单位元的海洋中,间接发生相互作用的。so what,这个单位元海洋能闹出啥动静吗?要真正理解单位元的重要性,还需要结合着逆元的存在性来看。

$$ e = a*a^{-1} = a^{-1}*a $$

现在单位元海洋就不是空无一物了,它提供无限多种中间运算过程,只是最后的计算结果是归于虚无而已。

$$ a*b = a e * b = a * cd * d^{-1} * c^{-1} * b $$

假设现在我们已经构造好了$acd$,则我们可以复用这个构造结果来构造$a*b$

$$ acd * d^{-1} * c^{-1} * b = ab $$

在我们所处的物理世界中,在人力所不能及的量子虚空中,表面上看起来空空如也,实际上只是正粒子和反粒子相互竞争达成了某种动态平衡。如果附近恰好存在一个黑洞,由于黑洞的引力场很强,可能会导致随机涨落创生的正反粒子被拉开,最终其中一个堕入黑洞视界,另外一个逃离黑洞。这就是传说中的霍金辐射、黑洞蒸发。

在可逆计算理论中,逆元的引入正是实现粗粒度复用的关键所在。

X = A + B + C
Y = A + B + D 
  = A + B + C + (-C) + D 
  = X + (-C+D) = X + Delta

假设X由A+B+C构成,我们现在想生产A + B +D所组成的Y,如果存在逆元和单位元,则我们可以从X出发,在完全不拆解X的前提下,通过一系列的差量运算将X转换为Y。利用结合律,我们可以将-C和D聚集在一起,形成一个完整、独立的Delta差量。在可逆计算的视角下,软件复用的原理发生了本质性的变化:从组件复用的相同可复用转换到可逆计算的相关可复用:任意的Y和任意的X之间都可以通过Delta建立转换关系(Transformation),从而形成复用,而不需要它们之间构成传统的部分-整体这样的组合关系(Compostion)。

逆元和单位元对于解方程这种复杂的推理模式也是必不可少的。

A = B + C
-B + A = -B + B + C = 0 + C
C = -B + A

解方程时之所以可以移项,本质上是在方程两侧都加上逆元,然后再省略生成的单位元。

Git可以反向应用patch,也可以利用patch指令来生成反向patch

git apply -R original.diff

patch -R -o reversed.diff < original.diff

但是因为没有结合律,Git中对于反向patch的应用也就乏善可陈了。

根据本节的分析,Git虽然提供了某种差量运算,但是它的数学性质却很难让人满意,这也就意味着基于Git的差量很难进行大规模的自动化处理,随时都会因为差量运算失效而导致需要人工介入。但是与Git相比,Docker的情况就要好很多,它的差量运算堪称完美。

四. Docker中的差量运算

1. Docker的差量运算是在哪个空间中定义的?

Docker所依赖的核心技术之一是所谓的堆叠文件系统OverlayFS,它依赖并建立在其它的文件系统之上(例如 ext4fs 和 xfs 等等),并不直接参与磁盘空间结构的划分,仅仅将原来底层文件系统中不同的目录进行 “合并”,然后向用户呈现,这也就是联合挂载技术。OverlayFS在查找文件的时候会先在上层找,找不到的情况下再到下层找。如果需要列举文件夹内的所有文件,则会合并上层目录和下层目录的所有文件统一返回。

Docker镜像的Delta差量是定义在文件系统空间中,所谓的Delta的最小单位不是字节而是文件。比如说,如果我们现在有一个10M的文件,如果我们为这个文件增加一个字节,则镜像会增大10M,因为OverlayFS要经历一个copy up过程,将下层的整个文件拷贝到上层,然后再在上层进行修改。

有些人可能会认为Git和Docker的差量的区别在于一个是线性列表,一个是树形结构。但是这并不是两者之间的本质性差异。真正重要的区别是Docker的差量结构空间中存在着可以用于唯一定位的稳定坐标:每个文件的完整文件路径可以看作是在文件结构空间中定位的唯一坐标。这个坐标或者说所有坐标组成的坐标系之所以被称为是稳定的,是因为当我们对文件系统进行局部改变时,比如新增一个文件或者删除一个文件,不会影响到其他文件的坐标。而Git中不同,它是使用行号来作为定位坐标的,因此只要新增行或者删除行,就会产生大量后续行的坐标变动,因此Git所提供的坐标系是不稳定的。

如果从哲学的角度去考虑,Docker的结构设计包含名和实两个部分,每个文件都有自己专属的名,也就是它的文件路径,可以用于在差量结构中间中进行唯一定位。这个所对应的对于差量合并而言并不重要,也无人关心,直接覆盖就可以了。而在Git的设计中,行号只能看作是一种临时的名,它要受到其他行的影响,为了准确定位行,patch文件中还会包含相邻行的内容,相当于是根据来作为一种定位的辅助手段。以直接限制了patch的独立性。

Docker的坐标系只管到文件级别,如果我们想在文件内部进行唯一定位并实现差量计算,那应该怎么办?Nop平台通过XDef元模型在DSL领域模型文件内部建立了领域坐标系,可以精确的定位到XML或者JSON文件中的任意节点。除此之外,Nop平台还内置了一个类似OverlayFS的虚拟文件系统,它将多个Delta层堆叠为一个统一的DeltaFileSystem。

有人可能要问,是不是一定要采用树形结构空间?也不一定。比如说,AOP技术所应用的结构空间可以看作是包-类-方法这样一个固定的三层结构空间,而不是支持任意深度嵌套的树形结构空间。类似的,在关系数据库领域,我们使用的是表-行-列这样一种三层结构空间。只要定位坐标是稳定的,我们都可以基于它们发展一些系统化的差量运算机制。

Tree结构具有很多优点。首先,它实现了相对坐标与绝对坐标的统一:从根节点开始到达任意节点只存在唯一的一条路径,它可以作为节点的绝对坐标,而另一方面,在某一个子树范围内,每一个节点都具有一个子树内的唯一路径,可以作为节点在子树内的相对坐标。根据节点的相对坐标和子树根节点的绝对坐标,我们可以很容易的计算得到节点的绝对坐标(直接拼接在一起就可以了)。

Tree结构的另一个优点是便于管控,每一个父节点都可以作为一个管控节点,可以将一些共享属性和操作自动向下传播到每个子节点。

关于差量结构空间,还有一个需要注意的细节:当存在逆元的情况下,差量结构空间必然是一种正元素和负元素混合产生的扩展空间,而不是我们习惯的正元素空间。当我们说”Docker的差量运算是定义在文件系统空间中"的时候,这个文件系统一定是需要支持负文件这个概念的。Docker具体的做法是通过一个特殊约定的Whiteout文件来表示删除一个文件或者目录。也即是说,我们将删除这个转瞬即逝的动作转换为了一个静态的、持久存在的、可操作的对象(文件或目录)。在数学上相当于是将 A - B转换为 A + (-B),这是一个非常不起眼但又非常关键的概念转换。

差量结构空间必然是正元素和负元素混合产生的一种扩展空间“,这句话听起来可能有点莫名奇妙,我再补充一点示例说明。假设我们现在处理的是一个有一定复杂度的多维空间,

X = [A, 0], 
Y = [0, -B],
X + Y = [A, -B]

如果X表示在第一个维度上增加A,而Y表示在第二个维度上减少B,那么如果再允许X和Y之间进行结合运算,我们得到的结果就是一个同时包含+A-B的混合物。如果我们只允许每个维度上的值都是正对象,那么这个混合物就是一个非法对象。为了确保Delta合并运算总可以成功,我们唯一的选择只能是扩展原有的正对象空间为允许同时包含正对象和负对象的扩展空间。再比如,在Nop平台的ORM模型定义中,我们规定的差量结构空间是一个DSL语法空间,在这个空间中我们可以表达如下的Delta,

X = 增加表A(+字段C1,+字段C2)
Y = 修改表A(+字段C3)
Z = 修改表A(-字段C3, +字段C4)
X + Y = 增加表A(+字段C1, +字段C2,+字段C3)
X + Y + Z = 增加表A(+字段C1, +字段C2,+字段C4)
X + Z = ?

在上面的例子中,X表示增加一个表A,它包含两个字段C1和C2。Y表示修改表A,为它增加字段C3,那么X和Y执行结合运算后得到的结果是:增加表A,包含字段C1、C2和C3。继续和Z结合,得到的结果是:增加表A,包含字段C1、C3和C4。这其中,C3字段在Y中增加,在Z中减少,最后的结果相当于C3被删除了。现在问题就来了:X和Z进行结合运算的结果是什么?因为根据X的定义,此时表A上没有字段C3,那么Z要求删除一个表A上不存在的字段,这怎么执行?我们在数据库里执行这种语句,直接就会报错。为了保证差量运算总是可以执行,我们的选择是承认如下定义是一个合法的差量定义:

U = 增加表A(+字段1, +字段2, -字段3, +字段4)

这样的话,我们就可以表示出X和Y进行结合运算的结果

X + Z = U

有些人可能要问,最终我们生成建表语句的时候不允许出现负字段,这要怎么办?很简单,扩展空间其实是一个允许计算发生的可行空间(抽象数学空间),它包含了所有可能发生的运算,这些可能的运算只是发生在抽象的数学空间中,并不会真正影响到我们的物理世界。当我们真的需要根据运算结果生成建表语句,到数据库中创建真正的数据库表时,我们可以增加一个投影运算,将对象从可行空间投影到只包含正对象的物理空间。

P(U) = 增加表A(+字段1, +字段2, +字段4)

这个投影运算负责删除所有的负对象,只保留所有的正对象。

在数学上这是一种非常标准的工作套路:将非法的运算结果添加到原先的空间中,从而形成一个扩展空间,使得运算在扩展空间中变成合法的运算。比如说我们必须要把复数添加到解空间中,这样的话二次方程才存在通用的解,否则有些二次方程在实数空间中是无解的。

$$ x^2 + 1= 0 \Longrightarrow x = ? $$

2. Docker的差量运算的结果是否仍然在文件系统空间中?

与Git不同,Docker的差量运算总是产生合法的合并结果。首先,任意两个Delta层都可以自由合并,并不像Git那样存在很强的容许限制

FROM registry.access.redhat.com/ubi8/ubi-minimal:8.8
WORKDIR /work/
RUN chown 1001 /work \
    && chmod "g+rwX" /work \
    && chown 1001:root /work
COPY --chown=1001:root target/*-runner /work/application

EXPOSE 8080
USER 1001

ENTRYPOINT ["./application", "-Dquarkus.http.host=0.0.0.0"]

我们可以随意修改DockerFile中的FROM配置。当升级操作系统镜像层的时候,我们不需要修改应用层的DockerFile,也不需要修改应用层的任何文件,直接重新打包就可以了。而在Git中,如果直接更改原始的Base文件,则依据于原有Base文件制作的所有patch都会失效。

打包成镜像之后,Docker的上层镜像会通过唯一的Hash码来绑定它所依赖的下层镜像,但是这可以看作是一种实际应用中的安全保证手段。在概念层面上,上层镜像与下层镜像是独立的,当下层镜像的内容发生变化的时候,上层镜像的内容包括DockerFile都不需要做任何的改变,只需要重新打包就可以了。

第二,Docker的差量合并永远不会出现冲突的情况。这使得镜像构建的自动化程度得到了极大的提升。结合上一节的内容,这实际上是意味着在Docker的差量结构空间中,任意的两个Delta都可以发生相互作用

Docker镜像的合并核心规则就是按照名称进行覆盖,而且覆盖的方向就是确定性的从上到下,显然不会出现冲突的情况。

如果已经存在一些Delta,那么这些Delta通过差量运算可以产生更多新的Delta。很自然的,我们要问,这些原始的Delta从哪里来呢?我们肯定是希望可用的Delta越多越好。在数学中,一个标准的工作套路是先论证某种数学对象具有很多优秀的性质,然后再想办法构造出大量这种对象出来。反映到软件领域,就对应于用生成器来生成Delta。

Docker的神来之笔是引入了DockerFile和Docker Build工具。它复用了Linux世界积累了数十年的历史遗产,每一个用于文件操纵的命令行工具都立刻转化为Docker差量结构空间中的一个有效的Generator。每一个Generator都具有明确的业务含义,可以独立的被理解和使用,并且可以串接在一起组成更复杂的Generator。如果从数学角度去理解,Docker的差量结构空间定义了基本的加减法,但是我们能不能在这个空间中再定义函数概念,从而将空间中的一个结构转换为另外一个结构?Generator可以看作是差量结构空间中的映射函数,而且它确确实实可以被表达为程序语言中的一个函数

与之相比,Git的差量结构空间就缺乏一个有意义的Generator映射机制。因为底层的Delta就缺乏独立存在的意义,在它之上要建立一个有意义的函数映射机制就更是难上加难。虽然说patch本身采用的也是文本表达形式,我们可以在任意程序语言中编写文本处理函数来生成patch,但是因为缺乏通用性,一般只是在极少数情况下,我们会针对特定的场景编写自己专用的某些Generator或者Transformer工具,而不像Docker那样,可以复用大量别人已经编好的Generator,并且毫无阻碍的把它们组合在一起使用。

一个好的数学空间需要有良好的基本单元和基础运算性质,还要在其上能够引入丰富的动力学特性。Generator的引入确保我们可以源源不断的产生新的Delta结构,同时也可以将不同抽象层次的Delta结构适配到一起。

可逆计算理论将Generator和Delta的构造规律总结为一个通用的软件构造公式,并为它的落地实现提供了一个标准的技术路线

App = Delta x-extends Generator<DSL>

这里的DSL指的是领域特定语言(Domain Specific Language,

DSL),同时它也隐含的定义了一种差量结构空间。一个程序语言能够描述的所有结构的整体构成一个差量结构空间(AST语法树空间)。与文件系统空间不同,并不存在统一的AST语法树空间,我们只能对每种程序语言单独去研究它的AST语法树空间。不过,在Nop平台中,我们并不直接使用通用语言来编写业务逻辑,而是大量使用DSL。比如说IoC容器使用beans.xml,ORM引擎使用的app.orm.xml,逻辑编排引擎使用的task.xml等,都是专用于某个领域的DSL。在Nop平台中,所有的XDSL都使用XLang语言中的XDef元模型语言来定义语言的语法结构,这些语法结构共享了XLang语言中定义的通用的差量合并语法规则,从而确保所有使用XDef定义的DSL都支持差量合并运算,并自动定义一个差量结构空间。也就是说虽然不存在统一的AST语法树空间,但是在差量运算这个层面,我们是可以定义出统一的差量合并运算,并且统一实现的。

可逆计算理论中的Generator泛指一切在差量结构空间中执行的结构生成和结构变换功能,它可以是一个独立的代码生成工具,也可以是语言内置的编译期元编程机制,如宏函数等。Nop平台为所有的DSL都增加了标准化的编译期元编程语法。也就是说在各个DSL中不需要定义元编程相关的语法,可以复用XLang中定义的标准语法和标准库。

<workflow>
   <x:gen-extends>
      <oa:GenWorkflowFromDingFlow xpl:lib="/nop/wf/xlib/oa.xlib">
        { 
          // 类钉钉工作流设计器所生成JSON
        }
      </oa:GenWorkflowFromDingFlow>  
   </x:gen-extends>  
   <!-- 这里的内容会和x:gen-extends生成的内容执行Delta差量合并 -->
</workflow>
  • 可以利用XLang内置的x:gen-extends语法把类钉钉工作流的JSON格式转换为NopWorkflow的DSL格式。
  • x:gen-extends生成的基础之上,还可以进行局部修改。

Generator作用到DSL之后得到的结果可能是一个新的DSL,这样就可以继续使用XLang的机制进行差量化处理。但是也可能会脱离Nop平台,生成某种通用程序语言代码,比如Java、Vue等,此时我们就只能利用语言内置的extends等机制实现部分差量合并运算能力。通用程序语言的AST语法树空间虽然也可以定义差量合并运算,但是它们的数学性质就没有XDSL中那么良好。关于XDSL的进一步介绍,可以参见XDSL:通用的领域特定语言设计

// _NopAuthUser是代码生成器自动生成的部分,手写的代码与自动生成的代码通过extends语法实现隔离
class NopAuthUser extends _NopAuthUser{
   // 在手写的代码中可以增加新的函数和属性,它们相当于是在基类基础上的Delta差量
   public boolean isAdminUser(){
      return getRoles().contains("admin");
   }
}
  • java的extends语法不支持删除语义,同时也不支持类似Tree结构的深层嵌套合并。

Git和Docker都可以看作是利用某种大家已经熟知的、已有的差量结构空间(行文本空间和文件系统空间)。而可逆计算理论是总结出相关的规律,支持系统化的构建专用的差量结构空间。Nop平台为此提供了一系列可复用的基础技术架构工具。Docker可以看作是可逆计算理论的一个具体应用实例。

App = DockerBuild<DockerFile> overlay-fs BaseImage

3. Docker中的差量运算是否满足结合律?

Docker利用OverlayFS将文件系统分成多个层,上层的文件自动覆盖下层的文件。当在Docker中删除一个文件时,实际上是在上层中添加了一个特殊的Whiteout文件来掩盖底层的文件。这允许容器看起来好像文件已经被删除,即使下层中仍然存在该文件。 从数学的角度去分析,Docker的差量运算就是简单的覆盖操作,它自动满足结合律。

  A ⊕ B = B 
  (A ⊕ B) ⊕ C = A ⊕ (B ⊕ C) = C

结合律的存在使得Docker镜像的制作在某种程度上可以脱离基础镜像进行。实际上,一个Docker镜像就是一个普通的tar包,解包后成为文件系统中的几个目录和文件。只要知道少数几条规则,就可以直接跳过docker应用程序,直接用tar指令制作Docker镜像。

Docker镜像获得了概念层面上的独立性,因此可以通过集中的DockerHub来管理和分发这些Delta切片。所有满足结合律的Delta差量都可以建立类似Docker镜像的这种独立管理、分发机制

4. Docker的差量运算的单位元和逆元是什么?

显然什么都不做就是Docker的差量空间中的单位元。而Whiteout文件可以看作是逆元。不过这里有个微妙的地方。在群的定义中,逆元的概念是针对每个元素单独定义的,每个a都有一个对应的$a^{-1}$ ,这些逆元并不相同(逆元相等等价于元素本身相同)。也就是说,群结构中的逆元具有某种特异性:$a^{-1}$是专用于抵消$a$的影响的。但是,Docker中的Whiteout文件仅仅是用于占位使用,它的内容其实是空的。一旦存在Whiteout文件,就会自动表示删除下层对应文件名的文件,无论该文件中的内容是什么。因此,Whiteout文件在作为逆元使用时,它是缺乏特异性的,它可以用于取消同样路径名的、具有任意内容的下层文件。

在数学层面上,这种特异性的缺乏最终表现为删除操作的幂等性

$$ Delete * Delete = Delete $$

删除一个文件两次,等价于删除一次。

数学上可以证明,幂等性与群结构是冲突的。一旦存在幂等元素,就不可能构成群结构。

$$ 幂等性: a * a = a
\begin{aligned} a &= ae = a * (aa^{-1})
&= a* a * a^{-1} = (a* a) * a^{-1}
&= a* a^{-1} \ &= e \end{aligned} $$

以上推导说明,如果一个群结构中存在幂等的元素,那么它一定就是单位元。由反证法可以推出,如果存在非单位元的幂等元素,就必然不可能构成群结构。因为一般情况下,在实现逆向操作的时候为了简化所需要记录的信息,我们总是采用幂等删除的设计,所以在数学层面上我们所定义的并不是真正的群结构,只是某种支持可逆运算的结构。

Monad和伴随函子

有人可能会问,如果没有逆元会怎么样?那就是函数式编程中让人心心念念的Monad啊。群的定义中包含四大天条:封闭性、结合性、单位元和逆元。只满足前两条称为半群,满足前三条称为幺半群(单位元又称为幺元),也就是Monad。所以Monad在数学层面上是一个相当贫瘠的结构,并没有多么了不起的作用。即使在范畴论中,真正核心的概念也是所谓的伴随函子(Adjoint Functor),这可以看作是可逆运算概念的一种推广。

关于Monad的介绍,可以参见我的文章写给小白的Monad指北

以下是智谱清言AI给出的伴随函子的定义:

伴随函子的定义涉及一对函子,以及它们之间的一种特殊关系。具体来说,给定两个范畴 $\mathcal{C}$和 $\mathcal{D}$,如果有一对函子:

$$ L: \mathcal{C} \rightarrow \mathcal{D} $$

$$ R: \mathcal{D} \rightarrow \mathcal{C} $$

并且对于所有 $\mathcal{C}$中的对象 $c$和 $\mathcal{D}$中的对象 $d$,都存在一个自然双射:

$$ \text{Hom}{\mathcal{D}}(L(c), d) \cong \text{Hom}{\mathcal{C}}(c, R(d)) $$

那么我们就说 $L$和 $R$是一对伴随函子,$L$是 $R$的左伴随,$R$是 $L$的右伴随。

举例来说,Nop平台的报表引擎负责根据对象数据生成Excel,而导入引擎负责解析Excel得到对象数据,它们可以看作是Excel范畴和对象范畴之间的一对伴随函子。

给定Excel范畴中的任意一个合法的Excel(满足某种规范要求,但是并不是固定格式),导入引擎都可以自动解析这个Excel得到对象数据。也就是说,我们并不是针对每一个Excel单独编写一个特殊的解析器,而是编写了一个通用的Excel解析器,它可以自动解析Excel范畴内的每一个Excel。因此,这个导入引擎就不是一个普通的函数,而是作用在Excel范畴中每一个具体的Excel文件上的函子(Functor)。类似的,对于对象范畴内的每一个对象,我们都可以根据某种规则自动导出生成一个Excel文件。类似于将对象导出为JSON文本格式,报表引擎在导出对象数据为Excel文件时并不需要任何额外的信息。

  • 在集合范畴中,函数是从一个集合到另一个集合的映射,这些映射在范畴论中被称为态射。每个集合在这个范畴中被视为一个对象。因此,函数就是集合范畴中从一个对象到另一个对象的态射。
  • 函子是范畴论中从一个范畴到另一个范畴的映射,它不仅将每个对象映射到另一个范畴的对象,还将每个态射映射到另一个范畴的相应态射,同时保持了态射的复合和范畴的结构。也就是说,如果有两个连续的态射 f:A→B 和 g:B→C,那么在目标范畴中,F(g∘f)=F(g)∘F(f)。
  • 函子的作用是全局性的,它涉及到范畴中的所有对象和所有态射,而不仅仅是单一对象或单一态射。换句话说,函子是某种高阶的描述,而函数是相对低阶的描述,在高阶的描述中定义的一个普通的点和箭头,翻译到低阶描述时都对应一大堆的处理规则。

一个Excel文件经过导入引擎解析得到对象数据,然后再经过报表引擎生成Excel文件,得到的Excel并不一定是与原先的Excel一模一样的Excel,而是在某种程度上与原有的Excel等价的一个Excel(比如某些样式信息发生了变化,或者单元格的相对位置等与业务无关的附加信息发生调整)。换句话说,在某种意义上,输入的Excel和输出的Excel具有某种等价关系 $Excel \simeq Export * Import(Excel)$。

同样的,一个JSON对象经过报表引擎导出为Excel,再经过导入引擎解析重新得到JSON对象时,可能一些属性值会出现细微的变化。比如说,一些值原本是空字符串,处理一圈回来之后可能变成了null,或者某些具有缺省值的字段在结果中丢失等。但是在某种意义上说,对象仍然保持某种等价关系 $ Obj \simeq Import * Export (Obj) $

伴随函子可以被视为可逆运算的一种推广,但这种推广是在范畴论的抽象框架下进行的,它涉及到函子和态射的复合,而不仅仅是单个运算的可逆性。在伴随函子的上下文中,$L $和$R $不是直接互为逆运算,而是通过所谓的自然同构相互“逆转”。具体来说,$L $和$R $在某种意义上互为逆运算,因为$R $将$L $的像映射回$\mathcal{C} $中的对象,而$L $将$R $的像映射回$\mathcal{D} $中的对象,但这种映射是通过自然同构来“修正”的。

五. 在不同的表示空间中有不同的差量

差量是定义在支持某种差量合并运算的模型空间中的变化量,不同的模型空间具有不同的差量形式。对应于同一个物理世界中的变化,差量的定义并不是唯一的。投射到不同的表示空间中我们会得到不同的差量运算结果。

首先,所有的结构都可以在通用的二进制比特空间中得到表示,比如函数A存储在文件中时对应于二进制数据10111...,而我们希望将它转换为函数B,它对应的二进制表示为010010...。在抽象的数学层面,寻找将函数A变换为函数B的差量X,相当于是求解如下方程 A⊕X=B。很显然,如果将⊕定义为二进制比特层面的异或操作,则我们可以自动求解得到 X=A⊕B

 A ⊕ B = A ⊕ (A ⊕ X) = (A ⊕ A) ⊕ X = 0 ⊕ X = X

在证明中我们用到了异或操作的归零律、结合律和恒等律

虽然在二进制比特空间中我们总是可以求解得到函数的差量,但是这个差量却没有什么业务价值(对于二进制级别的压缩软件等还是有价值的)。我们既不能直观的理解它,也缺少便利的手段来直观的操纵它。

对于同样的一个函数,如果投射到行文本空间中去观察,函数的差量对应的就是行文本的Diff结果。

既然有这么多可选的差量结构空间,那么哪一个才是最优的选择?这个问题的回答可以类比坐标系选择问题。同样的一个物理事实可以使用无数多种坐标系去建立描述,但是其中可能会存在一个特别的、针对这个特定问题定制的坐标系,在物理学中我们称之为内禀坐标系。在这个坐标系中建立的描述可以突出最核心的物理意义,简化相关的描述。比如说,在一个球面上发生的物理现象当然可以在通用的三维直角坐标系中进行描述,但是如果我们使用球面坐标系往往可以实现简化。

可逆计算理论指出可以针对特定的业务领域建立一个专用的DSL语言,利用这个DSL语言很自然的建立一个领域坐标系,然后再在这个领域坐标系所定义的差量结构空间中表达差量。因为这个领域坐标系是针对领域问题特制的,因此它往往可以实现差量表达的最小化。比如说,发生了一个业务层面的变化导致需要增加一个字段,如果采用通用语言去表达,则很多地方可能都需要做相应调整,前台、后台、数据库都要一起修改。而如果使用领域模型描述,这种变化可能就只体现为局部的一个字段级别变化,然后由底层引擎框架自动将领域描述翻译为实际执行的逻辑功能。

六. 总结

世界的本体是不可观测的。物理学格物以致知,我们所能感受到的不过是深不可测的世界本体之上被激发的一丝涟漪(差量)而已。

要深入的理解差量概念,需要从数学中群结构的定义出发:封闭性、结合性、单位元、逆元。这其中,逆元是一个非常关键性的概念。在软件领域,函数式编程炒热了Monad一词,它基本是满足群结构定义四大天条中的前三条,可以看作是幺半群结构,但是缺少逆元的概念。

满足封闭性和结合性称为半群,在此基础上增加单位元,则称为幺半群。

可逆计算理论明确指出了逆元概念在软件构造领域的重要性,并结合产生式编程,提出了一个系统化的实施差量计算的技术路线

App = Delta x-extends Generator<DSL>

在可逆计算理论的指导下,我们有必要重新思考软件的构造基础,基于差量的概念重建我们对于底层软件结构的理解。在5到10年内,我们可以期待整个业界发生一次从全量到差量的概念范式转换,我愿将它称之为软件智能生产领域的差量革命

基于可逆计算理论设计的低代码平台NopPlatform已开源: