愤世嫉俗者
PDF形式上称为 Pi 的微积分
关于 pi 演算的炒作
Stan Kelly-Bootle，作者
多米尼克·比汉曾在难得清醒的时刻（对我们俩而言）问我：“如果别人不知道你知道，那么知道一些事情有什么意义呢？”1 我用一句熟悉的谚语回答道：“重要的不是你不知道什么，而是你确信知道但其实不是那么回事的东西。”在阅读斯蒂芬·斯帕克斯对史蒂夫·罗斯-塔尔博特的采访时，我想起了这些可疑的认识论观点，该采访刊登在 2006 年 3 月的 杂志上。2 在推广罗宾·米尔纳的 pi 演算作为 BPM（业务流程管理）可证明可靠的支柱时，罗斯-塔尔博特缓解了我们对神秘、抽象的 pi 演算公理的恐惧，他强调外行/程序员“永远不需要看算法……永远不需要阅读文献，除非你晚上失眠。”
在学术 CS 逐渐渗透到实用计算的许多领域，这是一种完全有效的态度。抽象的概念，从某种意义上说，就是向我们隐藏更深层——不，是枯燥的——细节，这是计算的必要条件，本质上是基于我们对其他领域专家的尊重（直到证明并非如此）。当你拖放时真正发生了什么超出了所有合理的认知范围，所以别问！当然，熟悉的“需要知道”标准经常被淡化为至少“需要知道一点”的冲动，这是由于人类固有的好奇心。因此，即使我们没有在佩里耶泉水3 畅饮，也可以希望在专家们的争论爆发时理解要点，因为他们常常会这样做。
我一直有点着迷于集合论，因为我遇到了一位元数学家，我的英雄保罗·哈尔莫斯（不断掉名字了……），他那绝非幼稚的《朴素集合论》让我认真地探索了罗素、哥德尔、图灵、丘奇、策梅洛、弗兰克尔、科恩和米尔纳（我都没能近距离接触到他们）。形式逻辑、集合论和派生系统理论并非许多人认为的那样是枯燥、同义反复的死胡同，尽管即使是著名的数学家也发现公理方法是取得实际成果的学究式障碍！公理的基本概念、它们的完备性和一致性，以及命题“真”、“假”和“可证”的含义，都令人震惊地爆出了它们不公平的份额。希尔伯特梦想通过“纯粹”的逻辑和集合论为算术构建完整且一致的公理，分散了皮亚诺、弗雷格、罗素和怀特海、冯·诺伊曼以及许多其他人的注意力，直到哥德尔 1931 年的里程碑式论文发表。
简而言之，哥德尔证明，任何“有穷”形式公理系统，如果强大到足以支持我们日常的、平衡支票簿的算术，那么它要么是不完备的，要么是不一致的。当然，不完备性比不一致性更容易忍受。在一个不一致的形式系统中，所有命题都可以被证明既为假又为真，所以“你好，蓝屏墙！”或者更确切地说，一切都崩溃了——屏幕、墙壁以及所有。另一方面，不完备性只是 [原文如此！] 意味着并非所有真命题都可以在系统内被形式证明。这很烦人，但不太可能扰乱你的支票簿平衡。哥德尔构建的不可判定命题 G，巧妙而合法地，在其中嵌入了 G 不可证的命题。如果且仅当形式系统是一致的，那么这个命题的真理是显而易见的（因为 G-假意味着 G-真，这是不一致的明确标志，而 G-真，意味着 G 不可证，提供了一个一致但不完备的系统）。
简单的 [原文如此！] 解决方法是扩展公理列表（有限地），以便先前无法证明的真理现在成为公理（无需证明！）或可以从扩展系统中证明。唉，哥德尔的不完备性论证可以用来在扩展系统中构建一个新的、真但不可证的候选 G。以此类推。通过放弃“有穷”公理限制，已经取得了很大进展。例如，早在 1936 年，格哈德·根岑就使用“超限”归纳法证明了算术的一致性。
与此同时，早在 20 世纪 20 年代，形式系统世界遭受了许多人认为比哥德尔更严重的打击。这就是臭名昭著的 L-S（勒文海姆-斯科伦）定理，它处理我们从公理中推导出的模型，从而为干燥的骨架赋予血肉。当我们第一次看到给定的形式系统时，我们必须遵循它的原语、规则、定义和公理，而不会被无关的自然语言暗示所误导。因此，一个简单的几何公理集可能提供称为点、线、连接和交点的原语，以及诸如“至少存在三个不同的点”和“对于任意两个不同的点，都存在一条唯一的线，称为这两个点的连接”之类的公理，并且如此等等，具有令人痛苦的精确度。
你很难不将欧几里得几何的熟悉对象描绘出来——毫无疑问，负责的形式主义者也是受到相同概念的启发——然而，形式系统实际上并不依赖于特定的解释。事实上，如果我们开始从原语的名称而不是从公理隐含的属性中假设原语的属性，那么就会存在真正的危险。（欧几里得几何和非欧几里得几何的历史很好地说明了这种危险。平行线的某些性质在许多世纪以来一直被认为是自明的，尽管无法从公理中正确证明。）
在我的例子中，你可以互换点/线和连接/交点的传统含义，而不会影响公理的一致性或完备性（或缺乏）。或者你也可以同样用苹果/橙子代替点/线！然而，矛盾的是，我们的形式系统仍然是符号处理游戏，只有那些喜欢玩游戏的人才会感兴趣（是的，它们可能很有趣），除非它们可以被证明可以有效地模拟现实世界的某些方面。许多人认为，形式系统的最终“真实”一致性在于，当它可以被证明可以模拟“现实”的一部分，并且具有可靠的一致性记录时（例如用于计数的鹅卵石/算盘，或我们居住的局部欧几里得空间）。L-S 定理在某种程度上扰乱了这幅图景：任何形式系统都允许比“预期”的解释多得多的本质上不同的解释。4
现在，如果你已经从序言中幸存下来，那么就让我们进入 pi 演算。作为一个优雅的形式系统，它提供的原语很少：只有诸如 P、Q、x、y 等名称以及一些用于形式化操作名称的运算符符号。当名称被解释为进程和通道时，兴奋就来了，符号被用来指示并发进程可以交互的方式。一个本质特征是“结构同余”的定义，它允许你等同本质上相同的进程。完备性是通过定义 !P -> P | !P 来实现的，这被解释为允许无限数量的派生进程。
如果 pi 演算帮助我们编写并发进程并检测潜在的死亡之吻，那么它将受到 CS 工具包的欢迎。可以与 lambda 演算进行比较，lambda 演算有助于形式化顺序编程方法。为了提醒你形式系统与我们日常购物清单之间的潜在差距，请考虑 lambda 演算的定义
true := \x.\y.x false := \x.\y.y
这些不是本丢·彼拉多正在寻求的答案（“什么是真理？”约翰福音 18:38）。实际上，它们只是聪明的涂鸦，带有暗示性的名称，旨在反映我们日常二元逻辑的一些技术属性。L-S 告诉我们，还有可数无限多个有效的模型——但它们是什么（或可能是什么），勒文海姆和斯科伦都无法说清。
再次，人们可能会问，编程步兵需要了解多少关于这些有时令人昏昏欲睡的演算？人们认为，只需足够了解在适当的时候调用适当的库例程即可。[这用完了你本月“适当”的配额。——编者]
分歧出现的地方最好定位在论文《更好的数学能带来更好的业务流程吗？》5 中，琼·派克和罗杰·怀特海德质疑了 pi 演算和 BPM 的炒作。他们提出了合理的观点，即现实世界中的 BPM 及其前身 WFM（工作流管理）比任何基于 pi 演算或其扩展的系统都复杂得多。他们的主要反对意见是，pi 演算被吹捧为通往 BPM 的“唯一真理之路”。他们还质疑 BPM 本身是否是全新的“大事”，还是只是 1994 年工作流管理参考模型的翻版。派克和怀特海德反对 BPMI（BPM 倡议）一刀切的态度，即“任何不基于 pi 演算的产品，根据他们 [BPMI] 的定义，都不能提供真正的 BPM 解决方案。” 让我们希望并发调解的过程能够出现，从而满足双方的公理！
后记
比雅尼·斯特劳斯特鲁普好意地提醒我他对“代码与注释”争议的贡献（本专栏，2006 年 3 月）。由于 C++ 注释在语法上等同于单个空格字符，因此必须在扩展运算符重载以包括空格重载的计划中考虑它们（参见 http://public.research.att.com/~bs/whitespace98.pdf）。顺便说一句，重载空格的最初动机是允许数学家编写 x y 而不是 x*y 来表示乘法。理想情况下，我们希望将 x*y 写成 xy，这与古代传统相符，但这会产生将 xy 区分为 2 个字符的标识符和 xy 区分为两个 1 个字符的变量的乘积的问题。比雅尼引用了一位不太知名的斯堪的纳维亚人比约恩·斯塔夫特鲁普的工作，我猜他是神秘的 N. 布尔巴基的遥远、私生的后代。
我的 YACC（Yet Another Comment Compiler，又一个注释编译器）项目将受益于提议的元注释标记 \\，以补充常用的 C++ // 注释约定（\\ 意味着“将前面的字符串视为注释”）。
参考文献
- 在文学计算中，你既可以掉名字，也可以掉数字。精明的读者会注意到，我净化了多姆粗俗的口音，其中穿插着工业强度的粗俗词语以示强调，这些词语是不可印刷的。
- 与史蒂夫·罗斯-塔尔博特的对话。《》4(2): 14-23。
- 以前是亚历山大·蒲柏的“皮埃里亚泉”，直到我与法国韦尔热兹著名的气泡水灌装公司佩里耶签订了广告合同。
- 贝塞拉，L，巴恩斯，R. 2005。数学确定性的演变。《数学地平线》13（9 月），美国数学协会；http:// www.maa.org/mathhorizons。从泰勒斯到库克，再到莱布尼茨、康德、图灵、科恩等人的精彩但悲观的总结。
- 派克，J.，怀特海德，R. 2003。更好的数学能带来更好的业务流程吗？http://www.wfmc.org/standards/docs/better_maths_better_processes.pdf。
斯坦·凯利-布特尔 (http://www.feniks.com/skb/; http://www.sarcheck.com) 出生于英国利物浦，20 世纪 50 年代在剑桥大学攻读纯数学，之后在先驱 EDSAC I 上涉足不纯粹的计算机科学。他的许多著作包括《魔鬼的 DP 词典》（McGraw-Hill，1981 年）、《理解 Unix》（Sybex，1994 年）以及最近的电子书《计算机语言精粹：斯坦·凯利-布特尔读者》（CMP Media，2005 年）。《软件开发杂志》已将他评为首届斯坦·凯利-布特尔 ElecTech 年度奖的获得者，以表彰他在“技术和文学领域的终身成就”。诺贝尔和图灵都没有获得如此珍贵的同名认可。在他的笔名斯坦·凯利下，他作为歌手和词曲作者也享受着平行的职业生涯。
最初发表于 Queue 第 4 卷，第 4 期——
在 数字图书馆 中评论本文
© 保留所有权利。