您好,欢迎收听《阐释》,一个意想不到的哲学播客。我是马特·泰希曼,今天和我一起的是加布里埃拉·冈萨雷斯,她是达尔可编程配置语言的创造者,长期以来一直是Haskell编程语言的布道者,Haskell for All博客的作者,以及Arista Networks的工程经理。
她来讨论代数和编程的交集。加布里埃拉·冈萨雷斯,欢迎。非常感谢您邀请我参加您的播客。非常荣幸能邀请您。我认为,当很多人听到“代数”这个词时,他们想到的是高中代数。比如,数学老师给你一个问题,2乘以X等于16,现在解X。
而那些在大学里学习更多数学的人,通常会遇到所谓的抽象代数,它与高中代数有点关系,但更普遍一些。那么,抽象代数究竟是什么呢?所以,当我们想到代数时,我们通常会想到数字,也许是在简单的算术中。抽象代数背后的思想是,你采用这些代数运算,但它们作用于非数字的事物。
例如,我们将讨论如何添加代码或程序之类的东西,而不仅仅是简单的数字。这就是它抽象的原因。它不再作用于数字了。抽象代数比这更普遍一些。这是一种对正在发生的事情的一阶近似,但我感觉这是一种有用的入门方式。所以,在某种我们可以精确表达的意义上,你可以添加和乘以除数字以外的其他东西。嗯哼。是的。
好吧,这太疯狂了。那么,我不知道,我有两杯水,我把一杯倒进另一杯。这就像加法吗?我想,是的,添加非数字的东西的例子是什么呢?我喜欢举的一个例子是食谱。例如,你可以想象一下
让我们考虑加法和乘法。在食谱中,想象一下乘法意味着你指定要使用不止一种成分。通常,当你阅读食谱时,你会说,好的,成分是A、B和C。所以你可以想象一下,你可以用代数表示为A乘以B乘以C。
然后,在食谱中,你通常可以将一种成分替换为另一种成分。例如,也许你替换,我不知道,我不擅长这个,比如用糖代替蜂蜜。我编造的。是的,或者龙舌兰或其他甜味剂。没错,是的。所以你可以用加法来表示。其思想是,A加B意味着你可以使用成分A或成分B。
如果你仔细想想,如果我们使用这种约定来定义食谱,那么我们许多代数直觉都是正确的。让我举个例子。你可能在学校学过的一个算术规则是分配律的概念,你这么说,如果我取A并将其乘以B加C,这与A乘以B加A乘以C相同。
如果你从食谱的角度考虑一下,它表示,好的,如果我需要成分A,并且我需要成分B或C,这与说我需要成分A和成分B,或者我需要成分A和成分C相同。所以,即使我们不再谈论数字,谈论食谱时,这种代数直觉仍然成立。好的,明白了。起初我有点被
乘法意味着“与”,加法意味着“或”的想法搞糊涂了,因为,我不知道,我只是习惯于将乘法视为数字运算。但看起来我们在这里要讨论的是,也许是乘法和加法的本质的一部分,是为了使这个分配律适用。也就是说,如果你试图剥离什么是乘法运算,什么是加法运算,直到最基本的要素,你可能会得到的东西之一就是这个分配律。
对我来说,实际上,我第一次遇到代数作用于非数字事物的想法并不是抽象代数,实际上是线性代数。而且我认为也是向量代数。两者之一,按某种顺序。我还记得讲师费了很大的劲来解释,我认为实际上是向量空间,
说实话,我不记得所有细节,但他们花了大量时间说:“好的,所以你知道,你可以想象在这些向量空间中,如果你添加两个向量,则加法是可交换的,也是结合的,并且它也有一些恒等式。”我对这些非常简单的算术规则的整个演示几乎感到厌倦或不以为然。
直到后来,回想起来,我才意识到整个令人失望或简单化实际上才是重点,对吧?所以,数学不应该很复杂。其思想是我们希望能够将复杂的概念简化为更简单的概念,因为我们至少对数字的加法和乘法有直觉。
如果我们可以将这种直觉重新用于更复杂的事物,例如向量空间,或者线性代数中的矩阵,或者我刚才举的食谱的例子,那么这将使我们能够在思考这些事物时增强我们的直觉,而不是陷入低级细节中。所以,如果一个食谱说你需要香蕉和蜂蜜或龙舌兰,这与说
你需要香蕉和龙舌兰或香蕉和蜂蜜是同义的。没错。你可以概括这一点。例如,不要仅仅将成分列表视为满足代数属性,你实际上可以想象食谱本身,食谱中的实际步骤序列,也可以以同样的方式被视为代数。
例如,你可以想象A乘以B意味着先做A,然后做B。而A加B可以被视为说你可以做A或做B。好的,很有趣。所以现在我们已经改变了我们正在查看的食谱的哪个方面。
我们还注意到食谱中的其他内容也具有这种加乘结构或这种“或”和结构。所以看起来“与”通常与乘法一起出现,“或”通常与加法一起出现,在这些类比中。是的。例如,布尔代数就是这种简单版本。所以,我的意思是,你实际上可以两种方式都做。但布尔代数中的约定通常是乘法意味着“与”,加法意味着“或”,并且
同样的规律仍然适用,所以你可以想象A与B或C相同于A与B或A与C。所以布尔代数也像某种程度上概括了这里发生的事情的核心本质。所以,你和我,都是电脑的忠实粉丝,我不得不说这个
食谱中的乘法式运算和加法式运算确实让我想起了编写计算机程序,因为当你编写计算机程序时,你所做的很多事情就是告诉计算机先做这个,然后做那个,然后在某些条件下做其中一件事情,然后做这个,然后做那个。这实际上很像写食谱。所以这会是另一个这样的例子吗?是的,所以所有编程语言都会有一些概念
做这个,然后做那个。实际上,对于编程语言来说,能够说“做这个”或“做那个”并不常见,实际上根本不常见。我确实能想到一个来自我最喜欢的编程语言Haskell的例子。所以Haskell是一种称为软件事务内存的特定领域语言,它允许你做到这一点。它允许你指定
顾名思义,事务,这基本上是我们对可变变量的原子操作。但是这些原子操作通常会竞争,你基本上可以说的是,你可以有“或”的概念,我说我有两个我想运行的事务,有时事务可能会由于某种原因失败。
例如,一个事务可能会说:“我有这个前提条件。也许某个变量需要大于零,或者某个布尔值需要为假,并且这个事务必须满足该条件才能继续进行。”所以你可以做的是,你实际上可以添加两个事务,并说:“先尝试事务A”,如果该事务由于前提条件而无法取得进展,则改为回退到事务B,
所以,如果你想象一下排序是乘法,事务之间的交替是加法,那么它仍然遵守相同的代数规则,你可以说:“好的,所以如果我做事务A乘以事务B加C,换句话说,如果我有事务A后跟事务B或事务C,那么这应该给我相同的结果
尝试运行事务A后跟事务B,或尝试运行事务A后跟事务C。无论哪种方式,你都会得到相同的结果。它满足相同的分配律。所以说一个更详细的例子是,首先,尝试在网络中的这台机器上运行第一部分。然后,如果网络中的那台机器不可用,则尝试在另一台机器上运行它。这就像……
分布式软件应用程序的上下文中的“或”。是的,这在精神上非常相似。其思想是机器的存在或可用性有点像前提条件。这里的加法是说,检查这个程序的前提条件是否满足。如果没有,则回退到第二个程序,该程序可能在你的示例中运行在不同的机器上。计算机编程中还有什么其他例子具有这种加乘结构?
我认为许多程序员都能理解的一个非常简单的例子是正则表达式,简称regex。所以在正则表达式中,它通常是你有一种语言来指定字符串中的模式。因此,你使用正则表达式使用此模式与字符串匹配。
在最简单的情况下,正则表达式会告诉你模式是否匹配。所以这就像如果我想编写代码来识别这是一个电子邮件地址,因为它具有电子邮件地址的形状,或者这是一个电话号码。这具有电话号码的形状。我会使用正则表达式。是的。在网络安全中,你也会经常看到正则表达式出现。例如,他们可能会寻找某种签名来检测某些东西是否是恶意软件,例如已知的错误字符串。
因此,正则表达式通常有一些核心基本操作。所以首先你可以说最简单的正则表达式字符串将是类似“a、b、c”的东西。所以这就像首先匹配字符“a”,然后匹配字符“b”,然后匹配字符“c”。并且你在正则表达式中有一个“或”的概念。所以你可以说“a或b”。这与说“匹配a或匹配b”相同。
所以其思想是,正则表达式中的排序的作用与乘法非常相似,“或”或交替的作用与加法非常相似。事实上,你还可以执行其他正则表达式操作。例如,存在一个clean star的概念,它表示“匹配零次或多次”,或者plus,它表示“匹配一次或多次”。这些实际上也有代数解释,但我现在不会深入讨论这些。
所以,即使正则表达式语言不使用加号或乘法符号,从道德上讲,它基本上是一种代数形式。这很酷。它确实看起来像很多东西。比看起来的要多得多具有这种结构。
那么,这是那些我们已经想出一个数学抽象,而数学抽象在看似非常不同的事物之间找到了这种统一性的案例之一吗?还是说,如果我们眯起眼睛看一看,我们实际上可以看到成分比我们想象的更像正则表达式?是的。正如我们所说,
许多这些例子在精神上非常相似,所以你可以想象成分列表有点像正则表达式,你这样说:“好的,我正在匹配这个成分和那个成分”,或者“我正在匹配这个成分或另一个成分”。
那么,它是否匹配我对食谱所做的操作?那就是类比吗?所以它可以与成分列表或实际步骤序列进行类比。所以数学的巧妙之处在于,一旦你开始用这些更抽象的概念来思考,你就会开始看到各个应用领域之间所有这些联系。所以我们可以看到食谱有点像正则表达式,有点像布尔值。
所以数学非常擅长跨各个领域的思想交叉传播,因为这样你就可以利用你在一领域的直觉,并将其应用于推理其他领域。哇。所以如果我对成分有了很好的见解,这仅仅与它们的加法性和乘法性有关,我或许可以将其应用于我使用正则表达式或……
分布式软件或其他领域所做的任何事情。让我举一个例子来说明为什么在各个数学领域之间寻找联系可能会有所帮助。例如,在乘法中,每当你对某个东西求幂时,换句话说,将某个值提高到某个幂时,
有一种快速的方法可以做到这一点,而不仅仅是取该数字并将其自身反复相乘。实际上,一种更有效的方法是取该数字并不断对其平方,这导致了一种更有效的求幂算法。但这很酷,因为如果你可以对非数字的东西求幂,那么你实际上可以重用相同的算法,它仍然有效并且产生相同的加速。
例如,假设你有一种将正则表达式编译为有限状态自动机的方法。正则表达式具有乘法的概念。事实上,它们也有指数的概念。所以如果你继续这个类比,如果你在一个正则表达式中说,“我想匹配某个表达式n次”,这类似于取该表达式并将其提高到n次幂。所以每当你试图编译或解释该正则表达式时,
你可以使用相同的快速求幂技巧来解释该求幂的正则表达式。它仍然有效,因为该求幂技巧实际上并不关心底层事物是否是数字。它只关心它是否具有某种乘法概念,正则表达式就是这样。算法之所以有效是因为它针对这种抽象的乘法概念起作用,而不是针对数字本身起作用。
好的,明白了。所以我们真的开始看到抽象化的回报了。如果我们试图将加法和乘法提炼到它们的本质,而不假设我们是否正在使用数字或某种东西或两种东西,或者对加法和乘法的任何解释方面进行任何假设,但我们真的只是将其提炼到像这些是可交换运算、它们是分配运算、它们是结合运算等等。如果我们将其提炼到这样的东西,
你对加速算法的技巧所做的假设越少,它就越能很好地推广。是的。所以在抽象代数中,他们有各种不同的抽象接口族,你可以对它们进行编程,引用一下。让我们从半群的概念开始。所以半群是想象一下你只有加法,你还有一个规则,那就是
+运算必须是结合的,这意味着如果我说“将x和y相加”,然后“相加z”,这应该与我将x与(y+c)相加的结果相同。所以,然后你可以取该半群接口,并向其中添加一些附加功能以将其转换为幺半群。幺半群与半群相同,但它还有一个零的概念。
例如,我们提到x + 0应该总是等于x,0 + x也应该总是等于x,这些被称为恒等式定律。因此,还有更丰富的接口建立在半群和幺半群之上。有时你可能有一些东西可以以两种不同的方式成为幺半群。例如,我们谈到了数字。所以数字,你可以将它们视为一个幺半群,其中加法是加法,0是0。
但是,如果你真的想的话,你可以说:“好吧,实际上,我将让'+'表示乘法,并将'0'表示为1。”同样的规则仍然适用,因为乘法是结合的,而1是它的恒等式。因此,数字可以通过加法或乘法被视为幺半群。另一个可以以两种不同方式成为幺半群的例子是布尔值。所以那里有一个幺半群是
其中加法是“与”,零是“真”,结合律仍然成立,恒等式定律仍然成立。布尔值的另一个模型是加法是“或”,零是“假”,结合律仍然成立,恒等式定律仍然成立。所以,当你有一些结构像数字或布尔值时,
它在两种不同的意义上都是幺半群,我们实际上可以尝试混合它们,我们说:“好的,这两个幺半群中的一个将使它成为加法,而这两个幺半群中的另一个将使它成为乘法,然后这两个恒等式中的一个,我们将称之为零,另一个恒等式,我们将称之为一。”通常你知道选择哪个,取决于哪种方式使分配律成立。例如,对于数字,
将0设为0,将1设为1会给你正确的分配律。对于布尔值,它可以是任一方式。你会发现,当你具有两种在相同类型的数值上重叠的幺半群时,这些算术运算会非常常见。所以每当你具有两种以这种方式重叠的幺半群时,所以它们具有0、1、加法、乘法,
并且它们满足各种结合律,它们满足恒等式定律,并且它们满足分配律。我们称之为半环。还有其他对此的概括。例如,如果你对此进行更多研究,你可以了解环和群等等。但对于今天的谈话,我们将主要介绍半环。所以我们将自然数,计数数,
视为半群。好吧,我们还没有零,这听起来可能很疯狂,但实际上,我的意思是,在古希腊,他们还没有零。它后来在印度被发明出来。所以,好的,想象一下我们只有1、2、3、4、5等等等等。然后我们可以对它们做的唯一一件事就是加法。一旦我们将零纳入其中,我们就从半群的结构变成了幺半群的结构。幺半群是一个半群,除了,也就是说,它在其上定义了这个结合运算,加上一个
但它也具有一个恒等元素。任何东西加上恒等元素都是那个东西本身。而且,你知道,我们通常,我认为,直觉地认为零就像什么也没有,或者没有它,或者任何东西,就像在这种解释中一样。但实际上,在这个上下文中,零起到的唯一关键作用就是这个恒等式。事实上,如果我们将任何数字加到零,我们就会得到那个数字。这是我们在这个上下文中关心零的唯一原因。类似的另一个例子是列表。
所以非空列表,即必须至少包含一个元素的列表,与没有零的数字非常类似。你可以想象一下,你可以取非空列表并将它们连接起来,你保证结果仍然是非空列表,但没有恒等元素,还没有零。然后,如果我们将它们更改为列表,则可以为空,现在你可以将它们连接起来,但现在你也有零值,这将是空列表
重要的是要强调,从技术上讲,即使是带有0的自然数和空列表仍然是半群。记住,半群是一个接口。它是你声明支持的操作。当你针对抽象接口进行编程时,你不必使用所有可用的操作。所以任何作用于半群的东西都将作用于非空列表,并且它也将作用于列表。
但是任何作用于幺半群的东西,所以针对这个幺半群接口进行编程的算法只适用于列表,但不适用于非空列表,因为它们不支持该抽象接口。
然后半环的东西有点像双幺半群,我们有两个可以执行的结合运算和两个不同的恒等元素,每个恒等元素都对应于该运算。所以我们将对应于加法式运算的那个称为零,并将对应于乘法式运算的恒等元素称为一。然后还有一些关于它们如何很好地协同工作的规则。所以我们有这个各种不同类型的抽象代数的集合。我们有半群、幺半群和半环,对吧?
我们介绍了恒等元素的概念。在我们前面讨论的例子中,例如食谱或正则表达式,恒等元素是什么?是的,对于正则表达式,零将是一个总是无法匹配任何内容的正则表达式。它永远不会成功。一将是一个匹配空字符串的正则表达式,通常在正则表达式表示法中用epsilon表示。
你可以想象一下,例如,0将满足这里的吸收律。所以在正则表达式表示法中,它们并没有真正表示0的表示法。但是你可以想象一下,如果他们这样做了,如果你写了一个像0、A这样的正则表达式,那么根据吸收律,0乘以A应该等于0。所以如果你试图匹配总是会失败的东西,然后匹配A,那么它本身就不能匹配,因为第一部分会失败,并且根本不会到达A。
所以就像零乘以五等于零一样,一个说失败的程序与一个说查找字符M然后失败的程序相同。没错。
所以对于成分列表,就像同样,我们并没有,我们并没有真正为此成分列表表示,但是你可以想象零将是一种无法满足的成分。比如你可能永远买不到的东西。它无价。我不知道。而一将是成分的空集。它很容易满足。你总是拥有它。所以我们没有为此表示,但从概念上讲,如果我们这样做了,你可以这样写。然后关于……
并发和并行编程。是的,在我前面提到的软件事务内存示例中,零将是总是失败的事务,而一将是总是成功且什么也不做的事务。你提到过
如果我们要严格地给正则表达式一个恒等元素、一个零和一个一,我们将添加一些语言中还不存在的东西。也许这会引发一个问题,好吧,看,我们已经编写正则表达式几十年了。那么为什么要费心研究它们的代数属性呢?我认为一个非常重要的原因是
我们希望能够重用这些抽象接口。所以正则表达式DSL是一个不错的DSL。DSL是特定领域语言。对于那些在家记分的人来说。但是如果我们可以对这个抽象接口进行编程,我们仍然可能希望能够重用其他工具。让我举个例子。所以在Haskell中,有一个sum函数。事实上,许多编程语言都会有一个sum函数,你向它提供一个元素列表,它将把这些元素加起来。
但是记住,我们在这里试图概括数字的概念。那么,如果我们可以对非数字的东西求和呢?例如,如果我们可以对正则表达式的列表求和呢?所以你可以想象一下,如果正则表达式可以实现加法、乘法、零和一的这个抽象接口,那么我们可以将零个或多个正则表达式放在列表中,然后调用该列表上的sum。现在我们将得到一个将匹配该列表中这些正则表达式之一的正则表达式。
在编程世界中,我们针对抽象接口进行编程的原因是为了能够在多个不同领域重用相同的函数。例如,sum函数可以用于非数字的东西。在数学中,也有类似的重用概念。其思想是,如果你可以针对抽象接口证明某些东西,那么该证明适用于支持相同抽象接口的任何东西。对,所以……
许多编程语言都带有一个sum函数,这样如果我给该函数提供列表1、2、3,它将把列表中的所有数字加起来,并返回6。但是,具有更通用的加法概念的一个直接非常酷的回报是,我们还可以对非数字的其他东西的列表求和,任何其他具有相同结构的东西。
嗯哼。
尽管计算机编程往往会经历很多时尚潮流,但从抽象数学中汲取灵感以及你使用的模式和你在代码中编写的代码可以为我们提供更持久的动力。所以我想知道你是否可以说说这是为什么。是的,所以……
当我第一次开始编程时,我对函数式编程一无所知。我是在QBasic和后来的C、C++、Java上长大的。哦,伙计,每天给我一些Nibbles。喜欢那个。是的,我还记得Nibbles程序。是的,我记得在我很早开始编程的时候……
我尝试解决一些问题,但从未清楚解决问题的正确方法是什么,因为总是有很多不同的时尚潮流。有面向对象的编程,有过程式编程,即使在这些子领域内,也存在各种非平凡的设计决策来决定如何构建问题。我有点漫无目的地试图弄清楚我应该遵循的是哪一天的潮流,这似乎都非常临时和随意。
我只是想要一些更永恒的东西,一些更不言自明、不证自明的东西。我第一次体会到这一点是在学习 Haskell 或更普遍的功能编程时。这是第一个向我展示数学和计算机科学之间交集的东西。
一旦我开始在我的代码中看到所有这些数学模式,对我来说,这满足了不言自明、不证自明的标准。我认为这会持续下去,它具有持久的力量,其他一切只是其上的装饰。我觉得我的经历有点相似,也许部分原因是硬件可用花了这么长时间。
你可以真正使用 Haskell 等语言的地方,你知道,很多东西都是作为纯数学来探索的。其中一个很酷的回报是,每当有什么东西准备好投入生产,准备好让你开始用它编写软件并将其发布到世界上的时候,它在发布之前就已经经过了严格的数学研究。编写程序让你的电脑做一些事情而不
在一个也被彻底探索为纯数学的框架中。是的,我想强调的一点是,这不仅仅是与数学有联系,因为你可以把几乎任何东西都数学化,如果你在上面撒上足够的正式性的话。
足够的希腊字母。是的。我小时候经常这样做。我非常喜欢数学。在我发现电子游戏之前,我基本上会花我的空闲时间来为我周围各种现实生活中的现象想出随机的数学难题,以让自己忙碌。是的。
而且……我看到一本益智书即将出版。因此,这不仅仅是存在数学联系,而是存在简单的数学联系。例如,如果我们可以在代码和简单代数之间找到联系,那就更好,因为简单代数是在很小的时候就教给学生的,所以他们可以重复使用他们在那里的直觉。
所以我发现,我真正喜欢函数式编程的地方,与其说是它只是数学的,不如说是因为它所连接的数学非常简单。我想回顾一下我之前提到的例子,关于我第一次学习向量空间时,讲师非常死板地、非常缓慢地讲解基础知识,我觉得很失望。
当你第一次偶然接触函数式编程时,你会觉得很失望,因为他们会教你这些非常简单和无聊的东西,比如如何创建一个记录,如何创建一个和类型,
列表函数,一个常量函数,它总是返回相同的东西,大惊小怪,你在想,那又怎样呢,所以像这里所有其他语言一样,只是向我抛出所有这些非常华丽的抽象,比如参与者或分布式编程,而函数式编程却向我抛出所有这些非常无聊的概念。我
然后,当你学习函数式编程时,真正的突破在于意识到这些无聊的概念实际上是你所需要的一切,其他一切都是从这些简单的数学基元组装而成的。所以我们一直在讨论代数概念。因此,在函数式编程中,还有乘法和加法的另一个概念。因此,记录类型可以被视为零个或多个类型的乘积。这就是乘法的概念,但现在它是在类型级别而不是术语级别。
同样,在函数式编程中,存在和类型的概念,这同样是加法的类型级别概念。然后还有一个零的概念,所以有一个空或无效类型,它是无人居住的。还有一个一的概念,至少在 Haskell 中,他们称之为单元类型,它有点像一个空元组或一个没有字段的空记录。它们的行为与我们之前讨论过的代数运算有点相似。
另一个例子是函数类型类似于幂运算。因此,从 a 到 b 的函数可以被视为 b 的 a 次幂。因此,函数式编程的关键见解是,这些简单的代数类型实际上是你编程所需的一切。其他一切只是这些核心基础抽象的装饰。
是的,我发现的一件事是,对于以前没有做过的人来说,这有点难以解释,但你实际上可以构建出真正华丽的界面,就像你提到的参与者模型等等,这是一种令人惊奇的方式。
仅仅从这些非常简单的抽象中构建出来,因为它们是作为基本构建块而设计的简单抽象。然后你会发现,你不需要有特殊的代码来向编译器窃窃私语,以神奇的方式让事情发生,而你无法预测或真正研究或了解任何关于这些方式的信息。你只需要使用普通的香草,无论你使用的是 Haskell 还是类似的语言。
这当然是我体验过这种表达能力的一个地方。是的,我认为这可以追溯到可移植性和领域之间交叉授粉的概念。我认为许多听众会发现,如果他们学习函数式编程,他们学习的许多习惯用法实际上可以很好地转化为其他编程语言,因为它们是基础语言。
然而,例如,如果你试图将面向对象的习惯用法转换为函数式编程语言,它就不会很好地转换,因为它们在本质上不是那么基础。
因此,关于数学和与数学相关的领域(如函数式编程)的很多内容都是关于这种交叉授粉的概念。我们希望能够将我们在一个领域中学到的东西,能够重复使用或转移到另一个领域。这就是为什么我们非常关心这些基础的可重用抽象接口的原因。
而我们之前一直在讨论的抽象代数,只是一个例子,我们可以在一个领域中建立代数联系,我们也可以在其他领域中找到代数联系。所以你提出的另一个引人入胜的论点是,抽象代数比许多其他抽象数学领域更适合人类推理。我不确定你当时可能想到了什么,也许是拓扑学或分析学之类的东西。我不知道。但这个论点是如何进行的呢?
这里的关键词是“等式推理”。因此,在等式推理中,其思想是通过简单的替换来理解程序的行为。因此,在大多数编程语言中,你理解程序执行方式的方法是将程序模拟为某个子例程,并在某些站点列中跟踪某些状态。
在函数式编程语言中,你引用“模拟”语言的方法是简单地用它们所指代的事物来替换值。这称为等式推理。从这些抽象接口的角度考虑问题,往往会使这种等式推理更好地扩展到更大的示例。因为如果你第一次进行等式推理,它会非常乏味。说实话,这是一件苦差事。大多数人不会这样做,他们只是有点轻描淡写。
但是,如果你可以从抽象运算(如加法和乘法)的角度来考虑问题,这些运算配备了结合律、恒等律、分配律、零律等定律,那么这些定律对于简化推理过程非常有用。你经常可以使用它们来简化非常复杂的表达式。
这有点类似于你在学校学习的关于代数表达式(如多项式)的符号推理。你也可以对代码做完全相同的事情,因为代码的行为可能有点像这些多项式,你可以简化代码,而无需知道底层变量甚至指的是什么。是的,哲学家们可能会在“指称透明度”和“指称不透明度”的标签下熟悉这些概念。一个表达式是指称透明的,只要你可以
其中的任何子表达式,用于另一个指代相同事物的表达式。令人惊奇的是,是的,这个主题在哲学逻辑中已经耗费了大量的墨水,结果它实际上对计算机编程非常有用,因为你可以取一个程序,其中包含 XYZ,如果代码是指称透明的,只需将其中的不同表达式替换为等于相同事物的其他表达式,就可以非常轻松地转换代码。
所以这里关键的是,你可以抽象地推理代码。让我给你一个非常简单的例子。假设我有一个函数,其输入是 x,其输出是 x + 0。如果我知道 x + 0 总是 x,我可以去掉 +0,即使我不知道 x 是什么。这就是我所说的抽象或符号推理的例子。
而且很多时候,当我们需要证明代码是正确的时,我们希望证明代码即使在我们不知道输入是什么的情况下也是正确的。部分原因可能是运行该函数并在实时数据上对其进行测试并不容易、安全或便宜。因此,我们需要能够理解函数的作用,即使数据尚未出现。这就是为什么我们需要这种关于程序的符号推理能力的原因。
是的,完全正确。你永远不知道用户会如何使用程序。他们总是会做一些你从未想过的事情。而且,如果你不小心用户会做一些奇怪的事情,你就会得到蓝屏死机和各种不愉快的事情。我们希望,你知道,提前阻止这种情况发生。Gabriela Gonzalez,非常感谢你加入我们。这太棒了。非常欢迎。感谢你邀请我参加你的播客。Elucidations 博客已经迁移。我们现在位于 elucidations.now.sh。在博客上,你可以找到我们以前所有剧集的完整目录。
如果你有任何问题,请随时在 Twitter 上联系 atelucidationspod。再次感谢收听。