罗德·伯斯塔尔：悼念

《Formal Aspects of Computing》：Rod Burstall: In Memoriam

Rodney Martineau Burstall（Rod）是计算机科学先驱，1934年生于利物浦，2025年逝世。他在人工智能、编程语言语义、逻辑证明等领域贡献卓著，开发了POP-2、NPL、Hope等语言，创立计算机科学范畴论应用，并开发了Lego证明系统。其工作融合理论与实践，强调社区合作，获ACM SIGPLAN奖项。

　　Rodney Martineau Burstall，一位在计算机科学领域有着深远影响的学者，以其广泛的学术贡献、开放的人格和对科研社区的持续投入而闻名。他的职业生涯跨越了几十年，从早期的运筹学研究到后来在人工智能、编程语言理论和形式化方法等领域的探索，展现了他作为科学家的多面性和前瞻性。Rod不仅在学术上取得了卓越的成就，更在个人风格和研究态度上留下了深刻的印记。他始终相信，科研不仅是一项严谨的学术活动，更是一种充满乐趣和创造力的人类行为。这种信念贯穿于他的研究生涯，也影响了他所指导的众多学生和研究团队。

Rod出生于1934年，成长于利物浦的一个普通家庭。他的父亲是一位绘图员，母亲则是一位家庭主妇。这种背景让他从小就接触到不同领域的知识，为他后来在计算机科学领域的跨学科探索奠定了基础。在南港的King George V Grammar School完成学业后，他前往剑桥大学攻读自然科学，随后在伯明翰大学获得运筹学的硕士学位。这一阶段的学习经历使他不仅掌握了数学和逻辑的基础知识，也培养了他对实际问题的解决能力。在工业界工作的经历，尤其是他在布鲁塞尔的Bureau Gombert和肯特的Reed Paper Group，进一步深化了他对编程实践的理解。他在布鲁塞尔期间撰写的第一个程序，为他后来在计算机科学领域的研究打开了大门。

Rod的职业生涯始于1962年，他回到伯明翰大学担任研究研究员，并在该大学攻读博士学位，研究启发式编程在运筹学中的应用。这一时期，他的研究兴趣逐渐扩展到人工智能和编程语言的理论基础。他与Donald Michie合作，后者在二战期间曾与图灵共同工作，这使得Rod有机会接触到当时前沿的计算机科学思想。在爱丁堡大学的早期研究中，Rod参与了Freddy项目的开发，该项目旨在创建第一个具备视觉识别能力的装配机器人。这一工作不仅推动了人工智能的发展，也体现了他对实际应用的关注。他所开发的视觉识别程序，能够通过计算关系结构的局部同构性来识别物体，这一技术在当时具有极大的创新性。

Rod在编程语言理论方面的贡献尤为突出。他与Robin Popplestone等人共同开发了POP-2语言，这是一种结合了LISP和Algol特性的语言，深受Christopher Strachey的CPL语言和Peter Landin的函数式编程思想的影响。POP-2的出现，标志着编程语言设计从实用主义向理论化的转变。它不仅为人工智能研究提供了强大的工具，也推动了对编程语言语义的深入研究。Rod后来又参与了NPL语言的开发，这是一种实验性的函数式语言，旨在支持程序的正确性证明和变换。NPL最终演变为Hope语言，而Hope语言的许多特性，如代数数据类型和模式匹配函数定义，后来成为现代函数式编程语言如Standard ML、Caml和OCaml的重要组成部分。

Rod对编程语言理论的贡献不仅限于语言设计本身，还包括对程序正确性证明方法的探索。他与John Darlington合作，开创了程序变换的研究，这一方法通过正确性保持的变换，将已知正确的程序转换为更高效或更易于理解的形式。他们的工作为后来的程序验证研究奠定了基础，也启发了全球范围内的研究者对如何构建可靠、可证明正确的程序进行深入思考。Rod还提出了“间歇性断言”（intermittent assertion）方法，这一方法允许在程序执行过程中，对某个断言的满足时间进行建模，从而实现对程序总正确性的证明。这种方法在程序验证领域具有重要意义，为后来的分离逻辑（separation logic）的发展提供了理论基础。

在编程语言的语义研究方面，Rod同样发挥了关键作用。他与Christopher Strachey共同提出了“存储”（store）的概念，即存储可以被看作是从“位置”（L-values）到其内容的映射。这一观点为后来的语义学研究提供了新的视角，使得程序的行为可以通过数学逻辑来描述和分析。此外，他还在逻辑和代数的结合方面进行了开创性的工作。他与Peter Landin利用代数和同态的思想，构建了程序正确性的证明框架，并将这些方法应用于编译器的正确性证明。这种跨学科的研究方法，使他能够从更高的抽象层次理解编程语言的本质，也为后来的计算范畴理论（Computational Category Theory）提供了理论支持。

Rod的研究还涉及形式化方法和自动证明支持系统的开发。他在1960年代末期和1970年代初期，就开始探索如何将数学逻辑应用于程序验证。他的学生J Strother Moore、Rodney Topor和Raymond Aubin在这一领域进行了深入研究，推动了程序验证方法的发展。Rod在1980年代中期开发了IPE（Interactive Proof Editor），这是一种交互式证明编辑器，用于帮助研究者构建和验证数学证明。随后，他在1990年代领导开发了LEGO证明助手，这一系统结合了多种类型理论，包括爱丁堡逻辑框架（Edinburgh Logical Framework）、Coquand的构造演算（Calculus of Constructions）以及Zhaohui Luo的统一类型理论（Unified Theory of Dependent Types）。LEGO系统支持以自然演绎风格进行交互式证明开发，并能够生成明确的证明对象，为形式化方法的应用提供了强大的工具。

Rod的研究不仅限于理论，他还关注如何将这些理论应用于实际问题。例如，他与Joseph Goguen合作，提出了代数规范语言Clear，这一语言为程序行为的描述提供了新的方法。他们还引入了“机构”（institutions）的概念，这是一种用于描述程序规范模块如何组合和参数化的抽象框架。这一理论为后来的程序规范和验证研究提供了重要的数学基础，使得规范语言的设计和实现更加系统化和模块化。此外，Rod对程序模块化和抽象的探讨，也影响了后来的编程语言设计，如Standard ML中的模块系统，这一系统由Dave MacQueen设计，深受Rod研究的影响。

Rod的研究兴趣还延伸到计算与哲学的交叉领域。他深受佛教思想的影响，对意识、现实感知以及人类与计算机之间的关系进行了深入思考。他认为，计算机不仅是工具，更是人类思想的延伸，它帮助我们构建一个由我们主导的小世界。在这个世界中，我们扮演着“上帝”的角色，拥有对程序执行的完全控制权。然而，他也意识到，这种控制可能限制了我们对更广阔世界和现象的理解。他主张，计算机应该被视为一种开放的工具，帮助我们探索未知，而不是仅仅用来实现我们的意志。这种思想在他的研究中得到了体现，也影响了他对于程序正确性、形式化方法和计算本质的理解。

Rod的学术生涯充满了合作与交流。他不仅在爱丁堡大学培养了众多学生，还与世界各地的研究者保持着密切联系。他曾在美国、法国、比利时和日本等地担任访问学者，与这些国家的研究机构和工业界建立了广泛的联系。他的研究团队包括了Robin Milner、Gordon Plotkin、John Darlington等杰出的学者，这些人的工作在后来的计算机科学发展中占据了重要地位。Rod的个人秘书Eleanor Kerse在他的职业生涯中扮演了重要角色，她不仅协助他处理繁重的行政事务，还帮助他保持良好的组织和时间管理，尽管她努力的成果并未完全奏效。

Rod的学术贡献不仅体现在他的研究领域，也体现在他对科研社区的建设上。他创建了“Bob Boyer纪念学会”（BBMS），这是一个每周举行的非正式研讨会，吸引了众多研究者和学生参与。这种开放的学术交流方式，为爱丁堡大学的计算机科学研究营造了良好的氛围，也为后来的“计算机科学基础实验室”（Laboratory for Foundations of Computer Science）的成立奠定了基础。这一实验室由Rod、Matthew Hennessy、Robin Milner和Gordon Plotkin共同创建，成为计算机科学理论研究的重要中心。

Rod的研究风格强调简洁、优雅和实用性。他相信，科学研究应当以解决实际问题为目标，同时也要具备理论深度。他的许多研究工作，如程序变换、类型理论、程序正确性证明等，都体现了这种理念。他不仅在理论上取得了突破，还致力于将这些理论应用于实际编程和软件开发中。例如，他提出的“交付物”（deliverables）概念，强调程序与证明的结合，这一思想后来成为“带证明的代码”（proof-carrying code）的重要基础。

Rod的研究生涯虽然漫长，但他的工作始终围绕着一个核心问题：如何通过数学和逻辑的方法，使计算机程序的正确性成为可验证和可控制的特性。他提出的方法和思想，不仅在当时具有开创性，也为后来的计算机科学研究提供了重要的理论支持。他的研究跨越了多个领域，从人工智能到编程语言理论，从形式化方法到计算哲学，展现了他作为科学家的广度和深度。

Rod的学术成就得到了广泛的认可。他在1989年被选为欧洲科学院（Academia Europea）成员，在1995年成为苏格兰皇家学会（Royal Society of Edinburgh）的成员。2009年，他因在编程语言领域的杰出贡献，获得了ACM SIGPLAN编程语言成就奖。这些荣誉不仅是对他个人工作的肯定，也反映了他在计算机科学领域的重要地位。

Rod的研究不仅影响了学术界，也对工业界产生了深远的影响。他与Xerox Parc、IBM实验室、ICL Kidsgrove和Digital Equipment Corporation的System Research Center等机构合作，推动了编程语言和形式化方法在实际应用中的发展。这些合作不仅使他的理论得到了实践验证，也促进了计算机科学与工业界的深度融合。

Rod的研究风格和人格魅力，使他成为许多学生和同事心中的榜样。他始终保持着对新思想的开放态度，乐于倾听和学习，同时也乐于分享自己的见解。他的工作方式强调团队合作和社区建设，这使得他的研究团队始终保持活力和创造力。他不仅是一位杰出的科学家，更是一位充满人文关怀的导师和研究者。

Rod的去世是计算机科学界的一大损失。他的工作和思想将继续影响未来的计算机科学研究，而他所倡导的开放、合作和创新的精神，也将成为后人学习和效仿的典范。他的学术遗产不仅体现在他所发表的论文和开发的编程语言中，也体现在他所培养的学生和研究者身上。这些学生和研究者将继续沿着他所开辟的道路，探索计算机科学的未知领域，推动这一学科的发展。

Rod的个人生活同样丰富多彩。他与芬兰妻子Sissi在1959年结婚，他们育有三个女儿：Kaija、Taru和Taina。这个家庭氛围温暖而开放，为他的研究团队提供了良好的支持和环境。尽管Sissi和Kaija的离世对Rod造成了巨大的打击，但他仍然保持了对生活的热爱，并在晚年与Laila Kjellstr?m建立了深厚的伴侣关系。他的个人经历和信仰，也影响了他的学术思想，使他能够从更广阔的视角看待计算机科学的发展。

Rod的研究生涯不仅是一段学术旅程，更是一段充满人文关怀和哲学思考的探索。他的工作和思想，为我们理解计算机科学的本质、程序的正确性以及人与计算机之间的关系提供了重要的视角。他的贡献将继续激励未来的计算机科学家，推动这一学科向更高的层次发展。