罗宾·米尔纳的学术和家庭背景

理论计算机科学电子笔记162（2006）3-36www.elsevier.com/locate/entcs罗宾·米尔纳下面你会发现一个罗宾米尔纳采访的成绩单，在剑桥举行的3。2003年9月采访由Martin Berger主持。感谢本田康平、基思·克拉克、卡拉·本杰明和托尼·斯托克曼的帮助和建议。马丁·伯格：你出生在什么时候，什么地方，什么样的家庭背景？罗宾·米尔纳：我父亲是一名陆军军官。我1934年出生在南部海岸的普利茅斯，因为我们是军人家庭，所以经常搬家。我记得战争期间我们住在苏格兰的爱丁堡。我想我们搬到爱丁堡时，我大约五岁。我在爱丁堡住了三年，然后去威尔士上学。这是一所私立学校，由于战争，学校被疏散到威尔士，战后学校最终搬了回来，所以我回到了肯特郡。这是一所学校，通常人们会支付很多钱，但我们没有很多钱。但我有一种奖学金，因为我正在接受培训，这样我就可以获得奖学金，进入一所所谓的公立学校。所以你父母很重视你的学业成绩？嗯，是有点像。当我十三岁的时候，我参加了一所公立学校的奖学金我被录取了，这是你可能会称之为我的快速教育的开始你有兄弟姐妹吗？我有一个妹妹，是的，她比我大。她住在威尔士，现在退休了。 她有一个家庭，一个儿子。他有孩子。 她是一个寡妇，不幸的是。 她在威尔士照看一个药草园你上的是伊顿公学：你在那里最喜欢的科目是什么我总是对数学比其他任何东西都更感兴趣，但正如你可能知道的那样，在那些日子里，古典教育在那种学校里是必不可少1571-0661/2006 Elsevier B. V.出版doi：10.1016/j.entcs.2005.12.0744罗宾·米尔纳访谈/电子笔记理论计算机科学162（2006）3你学过希腊语还是拉丁语？我从10岁开始学习希腊语，从8岁开始学习拉丁语，我认为这两种语言都是有缺陷的数学形式，因为它们是以如此精确的方式教授的。但就古典文化而言，我们并没有被教导得那么多。无论如何，我对历史不是特别感兴趣。但我可以写拉丁文诗歌，因为拉丁文诗歌非常准确，毫无疑问，什么音节应该长，什么音节应该短：正如我所说，数学的一种缺陷形式。当然，我也在做真正的数学，我被允许全职做数学，从16岁开始。在我八岁到十三岁的时候，在我的预备学校里有一位好老师，我从他那里学到了很多东西，仅仅因为他非常喜欢它。在伊顿公学至少还有一个，我记得他也负责划船，但我记得他很鼓舞人心，他教我射影几何。他觉得它很美，我们也觉得它很美。这是一次很好的经历。这把我带到了十八岁。然后我拿了剑桥的奖学金。我去了国王你哪一年去剑桥的？我在1952年拿到了剑桥大学的奖学金，但后来我服了兵役。这把我带到了你去剑桥之前就参军了？是的我就在那个时候，我的小组中有两个人去了韩国，但我没有。我去了苏伊士运河。当时，英国人仍在掌权。那里一定很暖和天气很暖和，也很干燥。天不下雨是因为太干燥了。我你的父母理解你对数学的迷恋吗？或者他们只是看起来很困惑？哦，不，他们你不能去找你的父母，问哦，不！家里没有人。但这很好，因为我上的是寄宿学校。我一年有八个月住在那里。所以我有很多人可以倾诉。因为这个国家的教育系统很奇怪罗宾·米尔纳访谈/电子笔记理论计算机科学162（2006）35私立学校--他们是一个温室，但你学到的一件事就是要非常努力地学习。你做多少工作的标准，特别是如果你应该做这类事情，而不仅仅是一个运动员，是非常高的。你会学到，整晚都在思考一个数学问题，而不是去睡觉，这这种事情在那里很自然在伊顿公学，你哦，不，因为有一群大约70名学者，他们将与学校的其他人分开，被学校的其他人视为集体疯狂。所以没关系。你在伊顿公学的朋友们，有谁是今天的名人吗？是的，比如理查德·莱亚德，他现在是莱亚德勋爵，在伦敦经济学院工作，一个非常有效率的经济学家，一个很棒的他们都是很好的人，我很喜欢他们。在军队里，你是做普通的粗活还是参与密码学之类的工作？哦，不！我是皇家工兵团的指挥官，我照看重型机械...推土机我负责训练人们驾驶推土机和大型移动铲斗。这是你小时候的梦想吗不，这绝对不行！特别是我我们当时在沙子上挖洞然后你去了剑桥的国王是的，在你是如何发现这种转变的？你学过数学？是的，我学了两年数学因为我参加的考试，我确实漏掉了第一年，我从第二年开始，这可能是一个错误，因为我在军队呆了两年后失去了联系。但我基本上是在两年后拿到学位的，主要的学位论文，尽管我必须在剑桥住三年。1956年，我在这里参加了EDSAC机器的课程我认为编程真的很不优雅。你在我看来，编程并不是一件很美好的事情。所以我下定决心，这辈子再也不碰电脑了！这门编程课程是你大学学习的一部分吗？不，那是夏天的十天课程。当然，我没有意识到数字计算机是一项巨大的成就。我当时不知道图灵。所以我不知道逻辑工作。正是因为我自己的无知，我6罗宾·米尔纳访谈/电子笔记理论计算机科学162（2006）3到哲学。我学过哲学史。当时我也做了一定数量的分析哲学。我对罗素的摹状词和名称理论既感兴趣又感到困惑。这与我们现在的想法有关。但当我离开剑桥时，尽管人们建议我留下来，我对学术已经厌倦了。这似乎有点令人惊讶，你可能已经在剑桥在20世纪50年代，并没有意识到图灵是的，它看起来很奇怪，有趣的是，剑桥的计算人员对它的理论方面并不感兴趣他们不是数学家？不，工程成就是EDSAC计算机的主要成就，它建于1949年。这是一个伟大的成就，但这项工作和图灵图灵曾是国王学院的研究员在国王学院教我数学的那个人是图灵的朋友。但我没有意识到这一点，因为我们没有谈论图灵。所以我对他一无所知。你的数学教育不是逻辑方面的？不，逻辑是很晚才出现的，当我大约29，30岁的时候。63年64年1964年，你在剑桥毕业后做了什么，在你去城市之前？我去了伦敦，做了一些兼职工作。我在59年当了一年的老师小学还是高中？这是在一所中学里。所谓的文法学校。然后我在1960年离开了那里，一年后，我去了Ferranti，在那里我做了三年的编程尽管你反对？是的我没有带着极大的热情进入它，但我意识到我应该找份工作。听起来你当时很不确定。是的 完全不确定。 在Ferranti，我负责一个程序库。那是在伦敦吗这是在伦敦，是的。我确保他们出售的所有新机器都能正常工作。我有第一次编写编译器或编译器的一部分的经验。然后我想，也许我应该找一份学术工作，我做到了：我去了罗宾·米尔纳访谈/电子笔记理论计算机科学162（2006）371963年进入城市大学。在那里，我有一种双重生活：我教工程师数学，这是非常常规的，但我也开始对人工智能感兴趣。我对CPL特别感兴趣，这是一种受Christopher Strachey启发的编程语言，它最终通过BCPL导致了每个人都知道的C。你不，我没读过博士。没有你的帮助就能得到教职？不，没问题。你必须意识到，城市大学直到最近才成为一所先进技术学院，它刚刚成为一所大学。但无论如何，在那个时候--甚至是现在--你不必有博士学位就可以获得在这个国家工作。我们在这方面是相当独特的，但我仍然是少数。我从来没有读过博士的经历，在某些方面，也许我所做的比读过博士更独立。我没有被引导。我只是引导自己。我对关系代数产生了兴趣，特别是因为数据库。我想知道这是什么状态-塔斯基的关系代数。 当然，这与我这是一个使用代数或逻辑的例子- 制定问题和答案。我没怎么说。真正激发我兴趣的是程序验证和语义学的含义。当我去斯旺西在1968年我采取了一项研究工作，我放弃了教学，并成为一个研究助理大卫库珀谁是系主任在斯旺西。他在那里有一个小组，致力于程序验证、自洽定理证明和语义学。那是在达纳·斯科特提出他著名的领域理论的时候。他在69年做了一系列的演讲，我去了牛津，听了他的演讲。太令人兴奋了。所以，从某种意义上说，它开始移动得非常快。机器用逻辑证明定理的想法，以及用逻辑来理解机器在做什么的想法.这种双重关系开始激励我，因为它显然不是很简单。这种关系不仅仅是一种反向关系“我咬你，你咬我”：计算机说：“我会自动化你的逻辑”，逻辑说：“我会告诉你你的程序是什么意思”。这是两种不同的关系。当然，在经典数学中，你已经把逻辑形式化了，但你也用逻辑来赋予逻辑意义和推理。他们声称（Meta）语言有等级，但实际上是的，我想是一样的。我当然不知道。 特别是，它与计算机一起生活。8罗宾·米尔纳访谈/电子笔记理论计算机科学162（2006）3你对关系代数、数据库、程序验证的兴趣，是由你需要解决的一些特定问题引发的，还是一般的智力好奇心？这些问题当时就在空气中吗哦，是的，这些都是一个人可以做的事情，以进入学术方面的问题。我在斯旺西为自己写了一个自动定理证明器，并在那个方向上做任何有趣的事情的困难中变得支离破碎，我仍然是。我非常钦佩罗宾逊的归结原理，这是一个了不起的突破;但事实上，你可以用全自动定理证明来证明的知识量仍然很小。所以我总是对放大人类智能比我对人工智能更感兴趣。这意味着我开始对如何验证程序感兴趣。我知道弗洛伊德的工作。托尼·霍尔也在研究这类东西。我得到在那段时间里认识他。当然，我把我的定理证明器应用于弗洛伊德的断言。我从程序中生成验证条件。但后来花了很长时间来证明它们。我的定理证明器做不到这一点，于是我想：“我能证明一个真正的程序吗？”我找了一个化学家，我忘了他的名字，他写了一个与他的研究有关的Fortran程序，我想，让我们来证明一些东西。我对这个程序相当困难的事实很着迷;他使用Fortran数组来编码他自己的矩阵，但出于效率的原因，他把它们都嵌入到一个大的Fortran数组中。所以你有这个有趣的代表性问题。验证的问题是一个模拟或数据表示的问题，我意识到这将是一个多么大的问题事实上，我对模拟产生了兴趣，我在这方面做了一些工作，但只是程序之间的模拟。这不是一个非常数学深刻的作品，虽然托尼霍尔是非常好的，但一些具体的东西代表一些更抽象的东西的想法显然是重要的。所以，人类所做的就是从具体的表征中抽象出来，不管这种表征是什么。这就是算法和程序之间关系的本质。你的下一步是什么在此期间，我和大卫·库珀一起访问了美国。我们去了梅伦大学，那里有佐哈尔·曼纳，他曾在斯坦福大学与麦卡锡一起工作。我和Zohar Manna谈到了我一直在做的关于程序模式和验证的事情。结果，我从1970年开始和麦卡锡一起工作，从71年初开始有趣的是，他们只是在找一个能做点实事的人。司各特最近提出了一种域的逻辑，域的层次的逻辑，类型论的层次，这对我来说似乎是实用的东西。这就是LCF的由来。因为我很罗宾·米尔纳访谈/电子笔记理论计算机科学162（2006）39对人工辅助--或者我会说机器辅助--证明感兴趣当我意识到我可以用这种逻辑写出编程语言的语法，我可以用这种逻辑写出语义时，我真的花了很多时间。我也可以写下逻辑中的语义功能。这是领域理论语义学吗是的我可以编写翻译器，从一些琐碎的高级语言到一些琐碎的汇编代码。 我可以把通勤图的四边都写下来：你可以编译，然后获取目标代码的语义，或者获取源语言的语义，然后用目标语义编码，你会得到同样的答案。我们在LCF做的第一件事就是验证- 在原则上验证-通勤图。 这是一个相当大的一步。 但是验证编译器比验证单个计算机程序容易得多！你在什么意义上理解“验证编译器”？它是否假定您具有汇编语言的语义和高级语言的语义？是的你用什么作为你的汇编语言的语义？一些微处理器的状态转换？是的所以你去了一个非常可观的细节量？源语言的语义对象有一定的编码。我们并不是第一个想到这一点的人，他们的建议是“使用代数”！基本上，我们在斯坦福的很多时候都在使用代数，一个代数在另一个代数中但与此同时，我不知怎么对并发感兴趣了，我不知道怎么回事。 我记得，虽然没有把它与验证联系起来，但我对交互自动机感到好奇。我有一个想法，自动机理论是不够的，因为它没有说这是两个自动机相互作用。除了Krohn-Rhodes表示定理，它说的是将一个自动机的输出输入另一个自动机。但自动机之间没有互动。当互联网在南加州发展的时候，你在斯坦福大学。面向对象的工作又是怎样的呢？他们想在物体之间传递信息。是不是让你很不爽？我不知道也许吧我知道模拟语言。我10罗宾·米尔纳访谈/电子笔记理论计算机科学162（2006）3模拟是在63或64年或类似的时候发明的当时我们有很多模拟引起了我的兴趣，因为它是关于你如何在计算机中表示真实世界的。我记得我对如何在模拟过程中定义代理人感到困惑。例如，如果你让人沿着链传递水桶，那么你就模拟了人，但是你不应该以完全相同的方式模拟水桶吗？从水桶的角度来看，人类正在从水桶旁边经过，从人类的角度来看，水桶正在从人类旁边经过。因此，对于代表真实世界的过程，可能意味着什么，有一些特别的松散。如果你从模拟的角度来处理问题，那么许多计算模型肯定是不合适的：图灵机、λ演算、香农...他们都是非常非正式的关于从一个实体到另一个实体获取信息意味着什么。你可能是对的，但了解模拟语言一定是我认为自动机应该相互作用的原因之一。当然，我不知道佩特里的工作，这又开始于63年。我完全不知道。但后来让我印象深刻的是，佩特里的伟大之处在于，他实际上曾担心过自动机理论，以及自动机之间的相互作用可能意味着什么。这是一个转换图，这是另一个转换图，但左图中的转换必须与右图中的转换一致。而这种变迁的共享就是Petri表示通信的方式。佩特里的工作有趣的地方在于，他讨论了两个自动机如何相互作用，然后他把整个自动机放进一个佩特里网，他没有用模块化的方式来做。但事实上，他用这个来代表办公系统和现实世界的信息系统，表明他把眼光放得很高。Wasn’t我想是的，但他也把他的模型应用到了办公系统上。当我知道他的工作时，我真的不记得了。 当然，当我很久以后从事CCS的工作时，我意识到了这一点。在70年代末，我拜访了他，但那时他对模块化语义更感兴趣，因为指称语义的伟大之处在于它是组合的，在“组合”这个词的最准确意义上。当时的并发理论更像是一个枝节问题？它是，但我秘密地意识到，然后工作在验证和自动定理证明对我来说是非常令人兴奋的，但它它所做的是为那些真正关心正确性的人提供帮助我想做一些罗宾·米尔纳访谈/电子笔记理论计算机科学162（2006）311这将把这种理解带到更广阔的领域。我关心的不仅仅是计算机辅助证明，尽管这将是其中非常 在我看来，这种相互作用开始打破了模式，打破了人们一直试图用数学方法理解的极限。你当时把这些想法传达给社区容易吗像丘奇-图灵命题这样的东西一定非常强大。我可以想象人们会说：为什么你遇到过这种态度吗？或者人们对你的建议持开放态度吗？有些人是的我73年在比萨参加了一个会议。这是一次工作会议。意大利人当时也很感兴趣。所以我的第一篇关于过程的论文，我试图用领域理论的方式来写，大约是那个时候。语义学家试图将一种熟悉的语义思想应用于并发，这对它来说是一件陌生的事情。你在爱丁堡找到临时或永久的工作了吗？我在1973年得到了一个固定职位。那是从美国回来的，这是一件好事，因为我们希望我们的家人在欧洲接受教育，而不是在美国。在我们去爱丁堡之前，你能多说一点关于你自己的家庭吗？你什么时候结婚的？是的我63年结婚我们有我们的孩子，而我住在伦敦，在城市大学工作，在63年和68年之间你有几个孩子？我有三个孩子，但其中一个死了。我现在有两个孩子，一个儿子和一个女儿，他们每个人都有一个女儿。我女儿现在住在苏格兰。她教瑜伽，以前经营过一家培训残疾人的咖啡馆。总之，我们经常去那里，看那一家人。当我们去澳大利亚的时候，我们也会看到我儿子你儿子住在澳大利亚？不，他住在这里。 但他要去澳大利亚看她。你儿子是做什么的？他你我没试过我可能在早期避免尝试;总的来说，我12罗宾·米尔纳访谈/电子笔记理论计算机科学162（2006）3你在剑桥不读书的时候都做些什么我花了我的大部分时间在大学做音乐;作为一个学生在剑桥我没有满足大多数数学家。我的大部分社交生活都与演奏室内乐有关。我我在想我是不是该当个音乐家。我想知道我是否应该适当地训练，迟到，成为一个专业的音乐家。你的水平很高是的，我演得很好。你对哪种音乐感兴趣大部分是古典音乐。古典音乐：20世纪？巴赫？......这是什么？一切.一切.我认为每种风格都有精彩的音乐作品，也有糟糕的音乐作品。贝多芬的作品有糟糕的，也有精彩的。前几天晚上我听了狄多和埃涅阿斯的歌;珀塞尔很聪明，但并不总是这样。巴赫偶尔会很无聊，有些20世纪的音乐很精彩，有些勃拉姆斯很糟糕，有些勃拉姆斯实际上很精彩。我认为你必须认识到什么是真正令人兴奋的，尽管为什么你最后没有成为一名音乐家？我不知道我想因为我不作曲，我不是很擅长，虽然我很了解和声，但我不是很有创造力。其他事？我意识到我可能训练得有点晚了。但我从来没有想做数学作为一种爱好，所以我决定保持音乐作为一种爱好！我在很好的业余管弦乐队演奏。你不，我你有没有被问到你的正式工作和你的音乐能力之间是否有联系？我的回答是：是的，为什么不呢？数学家对音乐很感兴趣。也许他们对音乐的结构感兴趣。我怀疑数学是否与你所认为的音乐乐句、音乐中的音色或激情有任何关系。或者反过来说：你的数学创造力与你的音乐能力有关吗？我不知道我认为人对什么是优雅有一定的概念。这罗宾·米尔纳访谈/电子笔记理论计算机科学162（2006）313在计算机和音乐方面，包括我自己的一些不雅的对我来说，语义学在很大程度上是关于美学的。是的，尽管有标准，严格的标准，来判断什么是正确的，什么是数学上可行的。例如，组合性，在某种严格意义上，你确实需要它。但除此之外Petri-net社区说组合性是无趣的。他们过去是这样做的，但他们错了。他们现在正在改变。但他们在很多其他事情上都是对的，所以我很高兴地说，他们在这里错了，而不是太挑剔。Petri网实际上是理解并发性的一个非常重要的发展。我似乎记得唐·克努特曾经说过，他早期的学生都是音乐家，而他后来的学生都是极限运动。你注意到类似的变化了吗？我后来你去爱丁堡当教授了？我当上了讲师。你为什么想让你的孩子在欧洲接受教育？总的来说，我们倾向于发现美国儿童成长得太快，特别是在加利福尼亚州。我们并不打算永远生活在美国无论如何，我们想如何生活和我们想如何抚养我们的孩子是紧密相连的，所以我们想回来。爱丁堡是个好地方。只是当时刚好有工作。你在爱丁堡的目标是什么？我认为我在做这两件事：我继续进行验证工作，但我也想让并发成为主要的智力挑战，尽管两者非常接近。一些一流的人来和我一起做定理证明和LCF研 究 ： Malcolm Newey ， LockwoodMorris ， Mike Gordon ， ChrisWadsworth。我们确实设计了一个系统，这个系统本身并没有立即得到大量的应用，但是迈克·戈登把它带到了剑桥，这就是LCF系统。他开始做硬件验证。 然后，另外一两个人开始设计验证系统，或者更确切地说，是在我们系统的模型上进行计算机辅助证明的系统，特别是康奈尔大学的康斯特布尔和他的NuPrl。这个想法是你有一个元语言-我们称之为ML -你可以用它来表达你的证明策略，并且有一个严格的纪律，你可以控制你的定理证明器，这样它就不会违反逻辑规则。这是我们设计的支柱。以至于我们会拒绝14罗宾·米尔纳访谈/电子笔记理论计算机科学162（2006）3如果我们违反了规则，我们将是有效的。我们不会在汇编代码中或直接在Lisp中编码一些证明过程。这一切都必须通过逻辑推理规则所以如果你熬夜用电脑做证明，你就不必事后想“天哪，我是不是抄了几个因为LCF系统不允许你这么做！当然，它有一些特性，可以帮助你表达你对证明可能如何进行的想法。包括证据策略之类的？是的，这是一个智力上的挑战：你如何得到一个可信的证明变量，你如何构建我们寻找证明的方式，如何用较小的策略来定义较大的策略，等等，这些都是通过其他系统发展起来的，比如剑桥的迈克·戈登他根据LCF的原理设计了他的HOL高阶逻辑系统。你真好。我在70年代后半期非常忙，但同时发展我对并发的想法，CCS大约在1980年在我们谈论CCS之前，你能说几句关于ML的话吗？这是你在证明助手方面工作的重要结果之一。 你是什么时候意识到你手头有一种通用语言，可以在各种其他环境中使用的？这非常有趣，因为我们并没有真正尝试这样做。这并不完全归功于我们的洞察力。这部分归功于Luca Cardelli，他现在在微软实验室工作。他当时是Gordon Plotkin的学生，他把我们的ML实现带到了一台更快的机器上，因为他想为他的论文处理一些公式，据我所知，这是关于并发的。无论如何，作为一个快速的实现者，在几周内，他在一台不同的机器上实现了ML，而这台机器恰好是我们可以教学生的机器。 还有一个人--我记不清是谁了--决定用那台机器教大二的学生机器学习。通过这一系列事件，我们开始意识到我们确实有一些东西可以普遍使用。事实上，人们开始产生ML的不同方言-我包括法国人。我会在这个时候来的。由G'erardHut开发的Frenc也将其用于机器辅助证明。最终，大约在1983年，我们认为我们可以把不同的方言结合在一起，把它们变成一种语言。这就是标准ML的演变过程。从1983年到1990年花了7年时间。最后，它看起来像很多艰苦的工作！ 我们最终得到的是一种正式定义的编程语言，它被合理地使用;它是如何严格定义语言的范例。同时，它也是一种工作语言。它很好地站在罗宾·米尔纳访谈/电子笔记理论计算机科学162（2006）315那边但它并没有像人们所希望或期望的那样在世界范围内使用。我认为这是因为在发展语义的同时发展一种语言是非常困难的。语言确实在进化，但进化的方式与形式语义并不一致。我们你所说的进化编程语言或语义是什么意思？你能举个例子说明一下吗？是的我不确定这是不是最好的例子，但是想想ML的类型系统：记录处理没有特别的考虑。关于记录处理的类型有很多理论，记录处理的非常重要的类型系统，但在ML中没有。它不在里面的原因是因为我们不知道如何证明定理，如何把它做对。如果ML能够朝着记录的类型系统的方向发展，那就太好了;但是要确保这些定理成立，确保“类型良好的程序不会出错”，这是很难做到的。无论如何，获得语义和证明定理是一项巨大的工作。它是相当非模块化的：如果你改变了一个位，你往往会改变其他地方的其他位。修改一个定理，或者检查它是否仍然成立，是一项艰巨的任务。这如果你看看像Ocaml这样的语言，我认为它是目前ML最先进的方言，它是第一个实用可行的语言你可以用它做大多数事情，而不是低级编程。你对它的样子，里面有什么，省略了什么感到惊讶吗是你期望的那样吗？例如，你有模块和对象，尽管这两个概念有很大的重叠。我认为这是一个很好的故事，说明了一种语言是如何进化的，并且仍然保持非常强大。但是在进化过程中携带严格的语义是非常困难的，这是我们必须为未来的语言解决的问题。我认为Caml是一个巨大的成功，因为它表明，一种语言，开始作为一个理论，然而，cal承诺可以实现任何工程语言也可以实现的目标。但是最成功的语言C语言的出现是因为有人想在一些备用机器上编写计算机游戏，所以那倒是但好的语言也不是通过语义学来产生的。我们必须解决一些问题，我认为这你什么时候不再和曼梯勒港有关系了我继续参与其中。我们在1990年提出了形式语义学。在此之前我一直都很投入。然后我们在97年修改了它。这是大量的工作，但肯定不是全职的，修改语义。16罗宾·米尔纳访谈/电子笔记理论计算机科学162（2006）3到那时，我的主要任务是明确的并发，试图从智力上理解并发。我开始把它看作是一种模特练习，而不是语言练习。我们正在模拟世界上发生的事情，如果你喜欢的话，就像Petri建模的过程。我们并不是在寻找能够使计算有意义的最小基元集。事实上，我们正处于一种紧张的状态：我们正在寻找一小部分原语，但它们必须很好地与世界上正在发生的事情相适应，不仅是微观上的，而且是宏观上的。这对我来说是一个挑战：挑选在相当高的层次上可以理解的通信原语，以及这些系统在非常低的层次上实现的方式在某种程度上，我认为我们已经成功了。在CCS和CSP中，通信原语在一定程度上对抽象层次的变化具有鲁棒性。但是，重点仍然应该放在模拟真实系统中发生的事情上，无论它们是像操作系统这样的人造系统，还是它们已经存在。这里有一个微妙的变化，从图灵式的问题，什么是基本的，最小的原语集，你可以找到理解计算。我认为其中一些适用于并发，比如命名：命名的最小原语集是什么？所以其中一些适用。但是当我们朝着移动性发展，理解全球移动的系统时，你需要致力于更丰富的语义原语集。我认为我们正处于（a）找到一小部分基元和（b）准确地模拟现实世界之间的紧张状态。你能描述一下从CCS到Pi的历史时间轴吗？你的第一个并发形式主义是什么什么不管用？它是如何被感知的？我认为这我在1978年研究我所谓的行为原语集包括并行合成，预编译和那些东西。我想让这一小部分原语做所有的事情，或者做尽可能多的事情标记迁移系统的想法变得非常重要，因为它取代了那些不起作用的东西因为把东西编码到域理论中，等价性要么太丰富，要么太贫乏，我的意思是太大或太小。他们没有达到我认为的正确的行为对等概念。在这方面，领域论似乎不可避免地缺少了什么。因此，标签转换系统--但自动机已经有标签了！是的，没错，凯勒给过渡系统贴上了标签。 标签作为一种互动工具的想法变得非常重要。所以很罗宾·米尔纳访谈/电子笔记理论计算机科学162（2006）317自动机理论？在某种程度上，使其成为共享动作已经在Petri中出现。但从代数和构图的角度来做，这是一件重要的事情。79年我在奥胡斯演讲时，这就是CCS这本书的发展过程。你问的是它是如何发展的。人们可能不知道的我清楚地记得他在奥胡斯的办公室里的讨论，我们无法让它工作。所以CCS变成了没有通道通信的Pi演算。你知道CCS有缺点吗你绝对不行但在我看来你有两个层次：你有数据，然后你有数据被移动，但你你喜欢移动价值，但不移动移动的手段。我认为，在不移动的情况下观察并发结石非常重要。因为这样你就可以看到没有运动可以做多少事情。答案是：可以做的事情很多。CSP的人已经证明了这一点。可以处理大量的系统。然后你可以开始看到障碍在哪里，你不能建模的东西无论如何，无论你对发明没有移动性的东西有什么理由于是CCS就成了现在的样子有没有一个你证明的定理让你觉得“好吧，CCS绝对足够有趣”？我很欣赏你说“CCS不太正确，但它仍然很有趣，我们可以用它来理解很多事情”。我会对它不满意并把它扔掉。任何特定的关键事件，让你觉得两个关键事件：一个是能够证明行为等价实际上是一致的。这可不容易我以前一直在做这个。如果你认为它们是全等类的话，你会觉得你得到了某种新的本质，因为这样你就可以把全等类看作是你所谈论的“真实的东西”。这些都是你的语义的外延。这是一个一致性是很重要的，因为原始人似乎是他们自己，而不仅仅是一个优雅的集合。如果他们拒绝这个全等性证明，那就太糟糕了。一切就到此为止了。另一件事是-亨尼西-米尔纳逻辑是的你可以用双相似性来表示，18罗宾·米尔纳访谈/电子笔记理论计算机科学162（2006）3大卫·帕克，以前被称为“观测等价”。当然，这是相同的关系，几乎相同的关系，但当然，双相似性技术非常重要。所以，无论是哪一个，它都被亨尼西-米尔纳逻辑所捕获。事实上，你可以写规范，或者你可以有一个非常非常简单的逻辑，准确地捕捉到这种关系。这是一个无限逻辑，所以在某种意义上它并不简单。是的，这是一个无穷逻辑，它有求和，在无穷和，但如果你削减，你得到相当不错的无穷逻辑，如果你做某些事情CCS。我同意，它并不完全整洁，但它足够接近。我记得我对一些Petri网的人说：“看，因为我们现在有了一个与行为等价性相匹配的逻辑，这不是很有趣吗？”我发现他们对此反应不太好。无论如何，对我来说，这是一个事件，它说-除了做对一些事情和对这个无限概念的怀疑-我们走在正确的轨道上。关于过程计算者，有一件事让我印象深刻，那就是他们对等价性和一致性的痴迷。其他社区不关心这些事情，他们不明白为什么我们这样做，我们不明白为什么他们不这样做。 如果你同意我的评价，你对这些东西的痴迷，你认为它们很重要的美感，是从哪里来的？一个工作的程序员从来不处理真正的组合系统，他们总是在后台处理操作系统。 你认为这和你的数学教育有关吗？因为你接触过代数？也许吧但是，在指称语义学中，你有这样的想法，你理解程序的意义，并且意义是某种函数这似乎是数学家哦，当然，当然。但你也相信，通过数学计算，你提供了一个坚实的基础，使人们能够走得更远，尽管他们难道计算的世界不是合成的吗？是的，但你必须非常努力地推动这些事情。有人会对你说：“当然它不是合成的，看看操作系统”然后你可以说，好的，等一下，我们必须让操作系统成为参与者之一，这个代理群体中的一个代理，正在交互。我们我们必须问自己，它们是如何相互作用的？有没有一种意义上说，一个单一的程序与操作系统交互？所有这些问题都需要解决。 这几乎就像我们必须证明我们可以组成。在我们找到之前没人会注意的。最终人们希望，或者我希望他们希望，能够以讨论函数的方式来所以罗宾·米尔纳访谈/电子笔记理论计算机科学162（2006）319短期收益！关于等价：你最初是从弱迹的角度考虑的？通过大卫·帕克，你被引导到互模拟？哦，不，绝对不是。在1980年关于CCS的原版书中，有一个概念叫客观等价，还有一个概念叫强等价.强等价性，尽管它没有用最大定点来定义，但共归纳地，结果与双相似性相一致。这是因为图像的有限转换。因此，强等价性与强双相似性恰好一致。但我们忽略了共归纳证明技术。弱观测等价被证明并不完全一致，因为它被定义为Ω链的极限，每个成员都比前一个成员稍细。事实证明，我们错误地认为最大定点将作为下降的欧米伽链的极限。它必须去一个更高的序数。除了这种差异，而且这种差异只以一种相当复杂的方式出现，我们已经有了弱双相似性，但当然不是互模拟证明技术，这是如此重要。这是因为大卫·帕克在1981年访问爱丁堡。那是他的休假，他住在我家，读我的书，他在早餐时间下来，当我洗碗时，说：“这有什么问题”。然后我说“天哪怎么了”“这不是最大定点”我说然后我们去散步，答案是：是的，当然！我们不仅有了一个有很好收益的共归纳证明技术，而且我们也有了与已经存在的非常接近的巧合所以当我们去散步的时候;主要的话题是：我们应该叫这个东西什么？大卫想称之为“模仿”，我说“这很难说，让我们称之为互模拟”。他说“那有五个音节”，我说，“没关系，人们会很高兴的”。 我给它起了名字，但他提出了这个想法。 事实上，它与我所做的非常接近。 但证明的技巧和背后的数学原理 在我看来，大卫·帕克是谁？他最初与David Luckham和Michael Pa- terson一起从事程序模式的工作他们以在程序模式方面的工作而闻名。这是在Scott之前，所以他们在研究命令式程序的语义，并研究这些东西的等价性的可判定性，在函数符号的所有解释下，并找到一些非常漂亮的结果。他在麻省理工拿到了博士学位，但他是英国人。不管怎样，他是我很好的朋友。我在斯旺西的时候我们就认识了。在我们再次聚在一起讨论这个并发性问题之前，20罗宾·米尔纳访谈/电子笔记理论计算机科学162（2006）3他研究过μ演算和极大定点。所以他准备了最大的固定观点。人们在互模拟之前就知道并关心最大定点了吗哦，是的，非常确定。最大和最小定点。大卫是一个伟大的专家，当你有一个最大和一个最小定点运算符时，你会得到非凡的丰富性，比如mu演算。所以他把所有的知识都用上了。对他来说，这非常突出了我在CCS做错了什么。基本上，他是带着这个东西来的，它很合适。当我在1990年写这本书时，我试图讲述这个故事，关于它是如何适应的，以及它是多么重要他很早就去世了，大约在1990年。对我来说，他能得到公正的认可很重要。CCS已经设计好了，但这种特殊的双相似技术似乎非常重要，至少对我们这些相信等价和一致的人来说是这很重要的原因甚至现在我正在和托尼·霍尔交谈，他对一个程序满足其规格意味着什么的想法更感兴趣。我们现在试图调和CCS方法，它将表示视为同余类，而CSP讨论集合论的表示，如故障和迹等，并且具有非常好的排序关系，因此如果指定大于实现，则意味着实现是正确的。进程之间的排序概念当然是进程演算中的另一个重要内容。我认为我们两者都想要;我们想要外延的概念，也许它们是同余类，我们想要表示对一个具体化的改进或细化的排序或预排序这些细化关系的逆是什么？我怀疑这与交易有关？我想这里没有对称性。如果有人陈述了一个具体化，那么他们所说的是：我想要一个程序来满足这个，并且会有许多不同的程序来满足它。给定这个程序，你可以进一步细化它，它当然仍然会满足原来的规范，因为这是细化排序。但是粗化它可能意味着它不能满足它最初所满足的那个规范，因为你会在不同的方向上粗化它。所以粗化我觉得这样当然，人们往往对执行细节不感兴趣。人们有时希望将大量命令视为原子blob，希望忘记大部分细节。也许你正在谈论一个不同的抽象机器，在不同的环境中建模。罗宾·米尔纳访谈/电子笔记理论计算机科学162（2006）321抽象层次是的，但精炼不是正好相反吗？你有一个命令，上面写着我认为这是一种不同的修饰。假设你在逻辑上陈述了一个细节。你说所有的交流都必须满足以下公式。这使得整个空间的程序，以满足这一点。但他们都将在特定的抽象层次上讨论通信。你也许有些人会称之为抽象细化，也许会有可能是我把事情搞混了！但我想每个人都对此感到困惑。不同层次的抽象并不等同于从规范到实现的细化你在奥胡斯和莫恩斯·尼尔森谈过，你出版了你的CCS书。接下来呢你还在推动流动性，我猜？如何过渡到Pi？在我看来，关键的步骤是将所有东西折叠成名称，并找到使其工作的标记转换。是这样吗是的你知道尼尔森和恩伯格的论文吗？我看到它被引用。我没有亲自读过。它收录在《证明、语言和互动》（麻省理工学院出版社）中，这是一本2000年为我撰写的论文集，由戈登·普洛特金、科林·斯特林和马兹·托夫特编辑。我 可以 给 你看 。 Nielsen 和 Engberg 在1986 年 写了 一 篇名 为 “A calculus ofcommunicating systems with label passing”的论文。 关键是他们克服了我和莫根斯发现的一个困难，因此他们在那篇论文中为π演算迈出了实质性的一步。他们从来没有出版过。现在它被发表在那本散文集上。我们（JoachimParrow，David Walker和我）在我们关于Pi演算的第一篇论文中引用了他们的原始报告。我们把一些我们认为他们所做的贡献的摘要，以及我们为π演算所做的补充。有趣的是，正如我记得在1980年与Mogens交谈时，其中一件不适合的事情因为重命名可以是无限的？不。事实上，在进程外部应用重命名操作符不同于在整个进程中对名称进行语法替换。我记得，Mogens和我现在如果你看看Engberg和Nielsen22罗宾·米尔纳访谈/电子笔记理论计算机科学162（2006）3可能还有其他原因;我不记得为什么标签传递在我和莫恩斯的 在任何情况下，我们没有作出这一大步的圆周率演算，他和U e后。知道了这一点，约阿希姆·帕罗、大卫·沃克和我非常努力地工作，试图只得到一种名字。莫根斯和乌埃有各种各样的名字。我们做了很多工作来简化它。我们尝试了在消息中只绑定名称的想法。我们尝试了各种不同的方法，以确保我们不会错过任何一个技巧。我们花了大约三年的时间，从86年，87年，到88年，89年才把它弄清楚。这不仅是一个削减东西的问题，但要确保你不能削减更多，因为我们希望它尽可能接近定义。这是一个有趣的过程，我保留了一堆我们都写的备忘录。它总是需要尝试不同的可能性，似乎有相当多的可能性。作为可能性之一，你有没有，我们现在称之为异步Pi-演算，在那里你我想我们需要求和是因为它给出了标准形式，它给了我们CCS的代数。我们不愿意没有它。在我看来，保持总和，虽然也许不是完全必要的，给你更简单的应用，更简单的插图。无论如何，这是CCS的传统。 把它放在外面似乎不安全。我我发现求和的故事很吸引人，因为虽然这些演算似乎只有一个计算操作，数据交换（Pi的名称），如果你有不受限制的求和，还有第二种无声的通信，可以传达选择哪个被加数。这也是最终导致无限制求和在计算上更具表现力