微博

ECO中文网

 找回密码
 立即注册

QQ登录

只需一步,快速开始

查看: 3551|回复: 0
打印 上一主题 下一主题
收起左侧

1991 罗宾·米尔纳

[复制链接]
跳转到指定楼层
1
发表于 2022-4-16 17:34:48 | 只看该作者 回帖奖励 |倒序浏览 |阅读模式

马上注册 与译者交流

您需要 登录 才可以下载或查看,没有帐号?立即注册

x
A J Milner

PHOTOGRAPHS
BIRTH:
13 January 1934 Yealmpton, near Plymouth, England;

DEATH:
20 March 2010 in Cambridge, England

EDUCATION:
Eton; Kings College Cambridge 1954-’57 B.Sc. (mathematics) 1956; Part II (moral sciences) 1957.

EXPERIENCE:
Second Lieutenant, Royal Engineers (1952-1954); Mathematics teacher, Marylebone Grammar School (1958-1959); Programmer, Ferranti, (1960-1962); Lecturer, The City University, (1963-1967); Researcher, Swansea University (1968-1970), Stanford University (1971-1972); Lecturer/Personal Chair (1984) Edinburgh (1973-1995); Chair, Cambridge University Computer Laboratory (1995-2001); Chair, Department of Computer Science, University of Edinburgh (2009–2010).

HONORS AND AWARDS:
British Computer Society Technical Award (1987); Distinguished Fellow of the British Computer Society (1988), Founding Member Academia Europaea (1988); Fellow of the Royal Society (1988); Turing Award (1991); Fellow of the Royal Society of Edinburgh (1993); Fellow of the ACM (1994); Royal Medalist of the Royal Society of Edinburgh (2004); Foreign Associate of the National Academy of Engineering (2008).

ARTHUR JOHN ROBIN GORELL ("ROBIN") MILNER DL Author Profile link
United Kingdom – 1991
CITATION
For three distinct and complete achievements:

LCF, the mechanization of Scott's Logic of Computable Functions, probably the first theoretically based yet practical tool for machine assisted proof construction;
ML, the first language to include polymorphic type inference together with a type-safe exception-handling mechanism;
CCS, a general theory of concurrency.
In addition, he formulated and strongly advanced full abstraction, the study of the relationship between operational and denotational semantics.
SHORT ANNOTATED
BIBLIOGRAPHY
ACM TURING AWARD
LECTURE
RESEARCH
SUBJECTS
ADDITIONAL
MATERIALS
Working in challenging areas of computer science for twenty years, Robin Milner has established an international reputation for three distinct achievements, each of which has had a marked, important, and widespread effect on both the theory and practice of computer science. In addition, he formulated and strongly advanced full abstraction, the study of the relationship between denotational semantics (which formalizes the meaning of programs using abstract mathematical descriptions of behavior called denotations), and operational semantics (which models program execution).

A key ingredient in all of his work has been his ability to combine deep insight into mathematical foundations of the subject with an equally deep understanding  of practical and aesthetic issues, thus allowing the feedback of theory into practice in an exciting way. Further, his style of scholarship, rigor, and attention to detail sets a high example for all to follow.

Milner was born into a military family residing on the South coast of England. He was awarded a scholarship to Eton College in 1947, and subsequently served in the Royal Engineers, attaining the rank of Second Lieutenant. He then enrolled at King's College, Cambridge, graduating in 1957. At Cambridge, Milner studied Mathematics (B.Sc.), then Moral Sciences (Philosophy) (Part II).

His first encounter with computing, as an undergraduate in 1956, was uninspiring. He took a 10-day course in programming on Maurice Wilkes’ EDSAC (Electronic Delay Storage Automatic Calculator). His reaction was characteristically decisive: “Programming was not a very beautiful thing. I resolved I would never go near a computer in my life.” He found the activity of “writing one instruction after the other” to be “inelegant” and “arbitrary”.

Robin was, however, interested in tools as prosthetic devices that serve to extend our reach. He was intensely practical, as evidenced by the wooden geometric shapes on the light-strings on his lamps, and the comprehensive collection of chisels, gimlets and awls arranged neatly in the utility room (a spotlessly clean workshop that also served as the laundry) in his Cambridge home. Robin later became fascinated with computers as tools. He realized, very early, that that they were not just mere calculating devices, but could become ‘tools of the mind’.

Milner never studied for a PhD. After one year as a school teacher, and two years of national service in Suez, his next engagement with computers came at the computer manufacturer Ferranti, where he “made sure that all the new machines they were selling were actually working,” and also wrote parts of a compiler. In 1963 he moved to academia with a passionate belief that a deeper understanding of programming could form the basis for a more elegant practice.

At City University, London, he wondered how question-answering in databases might relate to relational algebra, but “didn’t get very far with that.” Then, at Swansea University in Wales, he began to publish on “program schemes,” an early flowchart-like operational model of computer programs.

Milner went to Oxford to hear lectures from Christopher Strachey and Dana Scott, who had been thinking about computable functionals, an abstract mathematical model for the meaning (“denotational semantics”) of a program, and about a logic of computable functionals (LCF) for reasoning about “denotation” objects. Milner said that getting interested in program verification and semantics was the real start of his research career. At Swansea he wrote his first automatic theorem prover, but was still “shattered with the difficulty of doing anything interesting”.

He was then invited to Stanford, where he spent two years (1971-1973) as a research associate with John McCarthy’s Artificial Intelligence Project. Milner was more interested in how human intelligence might be “amplified” than in what an artificial intelligence might achieve independently. Milner thought that machines might help humans apply the Scott-Strachey approach to denotational semantics to practical examples. The calculations required were laborious and error-prone, but many were mechanical and amenable to computerization.

He started work, together with Whitfield Diffie, Richard Weyhrauch, and Malcolm Newey, on an implementation of Scott’s LCF which he described as

…designed to allow the user interactively to generate formal proofs about computable functions and functionals over a variety of domains, including those of interest to the computer scientist - for example, integers, lists and computer programs and their semantics.

This LCF proof-assistant included a sub-goaling facility that allowed the user to divide the search for a proof into searches for smaller subproofs, with the machine keeping track of how to put the pieces of the proof back together. It also included a powerful simplification mechanism that allowed the machine to shoulder the burden of performing the more routine calculations.

The beauty of this architecture is that improvements in mechanization can easily be incorporated to build a more powerful assistant without invalidating existing proofs. Furthermore, patterns of proof can be coded as tactics that can be used in many proofs. Proof search is a combination of subgoaling and simplification steps. A tactic (an example might be induction on n) automates some combination of steps. Tactics allow common patterns to be reused; they are not simply a list of one instruction after the other. These ideas have themselves been reused, and built upon, to create proof assistants for a variety of logics.

Milner was still dissatisfied with the difficulty of using the then-existing programming languages – he was programming in LISP – and with the possibility of error. How could one be sure that the system could not introduce an inconsistency, and hence be useless because it could prove anything? When he moved to Edinburgh, in 1974, he embarked on ambitious program to develop and implement a practical programming language that drew on LISP, but was also much influenced by Peter Landin’s ISWIM (If you See What I Mean), an ‘abstract’ language that was never really implemented but which has clear mathematical foundations and operational semantics based on Landin’s ‘SECD’ abstract machine.

Milner’s new language was designed as a metalanguage (hence its name, ML) for the implementation of a new proof-assistant called Edinburgh LCF. It was a robust and efficient practical tool well-adapted for this task, and was defined with the mathematical clarity exemplified by Landin’s work. A further discussion of ML can be found here.

ML was way ahead of its time. It is built on clean and well-articulated mathematical ideas, teased apart so that they can be studied independently and relatively easily remixed and reused. ML has influenced many practical languages, including Java, Scala, and Microsoft’s F#. Indeed, no serious language designer should ignore this example of good design.

Meanwhile, Milner continued to worry about the foundational issues of semantics, in particular the link between the properties of the mathematical denotation of a program, and its operational behavior. If two programs can be observed to behave differently, they must have different denotations, otherwise the semantics would be unsound. Ideally, the converse should hold: any two observationally indistinguishable programs should have the same denotation.

However, Gordon Plotkin discovered a key limitation of sequential programming, which meant that the natural Scott-Strachey model for an ISWIM-like language could have two programs that are observationally indistinguishable, but have different denotations. Milner constructed the first fully abstract model in which two observationally equivalent programs must have the same denotation.

Milner worried about modeling non-deterministic programs and concurrent processes, which Scott-Strachey semantics didn’t address conveniently. The advent of timesharing and networking made this a practical as well as a theoretical issue. A simple functional model of sequential computation does not account for the possibility of interference between two programs that share the same memory, nor does it account for the interactions in a client-server architecture, or the interactions between a system and its users.

It is possible to create clever denotational models that account for such features, but Milner wanted a “semantic theory in which interaction or communication is the central idea.” His first concern was about “the choice of interpretation and of mathematical framework, a small well-knit collection of ideas, which justifies the manipulations of the calculus.” After a long period of reflection and experimentation, he settled on Robert M. Keller’s deceptively simple model of labeled transition systems with synchronized communication, to which he applied the notion of observational equivalence. This formed the basis for his1980 book Calculus of Communicating Systems (CCS) [2], which sets out a ‘general theory of concurrency’.

But he was not satisfied. He observed that “there is still latitude for choice in the definition of observational equivalence,” and conjectured that CCS might be extended by allowing “labels to be passed as values in communication.”

Shortly after the publication of CCS, Milner learnt of David Park’s notion of “bisimulation”, a subtle but compelling refinement of the notion of observational equivalence. Milner completely reworked his theory in a new book, Communication and Concurrency [3] in 1989. CCS is little-changed, but the whole theory, in particular the treatment of observational equivalence, is more elegant and less arbitrary.

These three strands of his early works – proof, concurrency, and ML – are highlighted in Milner’s Turing Award citation. The award trophy, representing computing’s highest honor, sat inconspicuously in his kitchen between a vase and a bowl of fruit.

An account that stopped at this point would not do justice to his legacy. In addition to making his own technical contributions to the field, Milner eloquently articulated a vision of Computer Science as an intellectual endeavor. His inaugural address for the Laboratory for Foundations of Computer Science at the University of Edinburgh asked, “Is Computing an Experimental Science?”, and argued that theories of computation should be tested against their impact on practice.

In accepting his honorary doctorate from the University of Bologna in 1997, he reflected on the power of programming

Every tool designed by man is a prosthetic device, and for every prosthetic device there is a means of control. Many tools are physical, and their control is manual. In contrast, computers are the most complex tools ever invented, and they are tools of the mind; the means of control is hardly muscular - it is primarily linguistic. Quite simply, the versatility of computers is exactly equal to the versatility of the languages by which we prescribe their behaviour, and this appears to be unbounded.

and then articulated his vision of informatics

Computing is not only about a computer's internal action; it is about the way a computer behaves as part of a larger system. The terms in which the computer behaviour is prescribed must harmonize with the way we describe information flow in such systems. Thus computing expands into informatics, the science of information and communication […] it can provide an exact view of the world which is not the province of any previously existing science.

His technical work continued with this broader perspective. Working with Joachim Parrow and David Walker, he developed the π-calculus in 1992, in which labels are passed as values to create a calculus of communicating systems that can naturally express processes with changing structure. For Milner’s definitive account, see Communicating and Mobile Systems: The π-calculus [5].

He was increasingly concerned about ensuring the impact of theory on practice.  For example, he contributed as an invited expert to the Web Services Choreography Description Language (WS-CDL); aspects of this business-process description language are inspired by the π-calculus.

The calculus also led to further formal calculi for describing and reasoning about other systems, including the spi calculus for cryptographic protocols and the stochastic π-calculus for cellular signaling pathways. Such widely differing applications reinforced Milner’s vision of informatics as a science of information and interaction that can be applied in many domains. “Informatics,” he said, “is a synonym for computer science. The ‘info’ words have an advantage: they express the insight that informatic behavior is wider than what computers do, or what computing is.”

Milner retired in 2001, but he did not stop. The π-calculus had been applied to new examples of interaction that he had not anticipated, but he now saw even more. For example, a

“daunting range of concepts [is] needed to understand ubiquitous computing: data provenance, privacy, authorization, trust (among agents), self-awareness, self-management, reconfiguration, failure recovery, goals, beliefs, ..., and the list can be extended much further.”

He embarked enthusiastically on the development of a further model, “a topographical model which aims to provide a theoretical foundation for mobile interactive systems”.

This ambitious enterprise led to the “bigraphical" model reported in his final book, The Space and Motion of Communicating Agents [7] in 2009. In it Milner seeks to account for agents with locality and connectivity that may be reconfigured through motion (placing) and interaction (linking). His goal is to model “not only interactive behavior among artificial agents, but also interaction with and among natural agents. Ultimately our informatic modelling should merge with, and enrich, natural science.”

Bigraphs model the concurrent and interactive behaviors of mobile communicating agents. Applications include computational systems biology, where the agents include genes and proteins, and the internet, where the agents include people, computers, and programs. Like Milner's earlier work, this is destined to have far-reaching and profound significance, both within computer science and beyond.

He was interviewed as ‘Geek of the Week’ just a few weeks before his death, and said, of his work on bigraphs,

I would dearly love to follow this kind of work through to the front line of design and experience, but I don't think I'll be around for long enough. I'm making up for it by listening and talking to those who will be!

Robin’s listening and talking stimulated various groups to work on bigraphical programming languages, and on the application of bigraphs to model natural systems. He returned part time to a chair at Edinburgh, still full of plans and projects for the future, when he died of a heart attack on 20th March 2010, just a few days after the funeral of his beloved wife Lucy.

Author: Michael Fourman



A J Milner

照片
诞生。
1934年1月13日,英国普利茅斯附近的Yealmpton。

逝世
2010年3月20日在英国剑桥

教育经历。
伊顿公学;剑桥大学国王学院1954-57年理学士(数学)1956年;第二部分(道德科学)1957年。

经历:英国皇家工程兵少尉(1952年)。
皇家工程兵少尉(1952-1954);Marylebone文法学校数学教师(1958-1959);Ferranti公司程序员(1960-1962);城市大学讲师(1963-1967);斯旺西大学研究员(1968-1970),斯坦福大学(1971-1972);爱丁堡大学讲师/个人主席(1984)(1973-1995);剑桥大学计算机实验室主席(1995-2001);爱丁堡大学计算机科学系主席(2009-2010)。

荣誉和奖项。
英国计算机学会技术奖(1987年);英国计算机学会杰出会员(1988年),欧洲科学院创始成员(1988年);英国皇家学会会员(1988年);图灵奖(1991年);爱丁堡皇家学会会员(1993年);ACM会员(1994年);爱丁堡皇家学会皇家勋章获得者(2004年);国家工程院外籍院士(2008年)。

ARTHUR JOHN ROBIN GORELL ("ROBIN") MILNER DL作者简介链接
联合王国 - 1991年
褒奖
因为三项独特而完整的成就。

LCF,斯科特的可计算函数逻辑的机械化,可能是第一个基于理论而又实用的机器辅助证明构造工具。
ML,第一种包括多态类型推理以及类型安全的异常处理机制的语言。
CCS,一个关于并发的一般理论。
此外,他提出并大力推进完全抽象,研究运算语义和指称语义之间的关系。
短篇注释
书目
亚马逊图灵奖
讲座
研究
主题
额外的
材料
罗宾-米尔纳在计算机科学的挑战性领域工作了20年,因三项独特的成就而建立了国际声誉,其中每一项都对计算机科学的理论和实践产生了明显、重要和广泛的影响。此外,他提出并大力推进完全抽象,即研究指称语义学(使用称为指称的抽象数学行为描述来正式确定程序的意义)和操作语义学(为程序执行建模)之间的关系。

他所有工作的一个关键因素是,他能够将对该学科数学基础的深刻见解与对实践和美学问题的同样深刻的理解结合起来,从而使理论以一种令人兴奋的方式反馈到实践中。此外,他的学术风格、严谨性和对细节的关注为所有人树立了一个高度的榜样。

米尔纳出生在一个居住在英格兰南海岸的军人家庭。1947年,他获得了伊顿学院的奖学金,随后在皇家工程师部队服役,获得了少尉军衔。然后他进入剑桥大学国王学院学习,于1957年毕业。在剑桥,米尔纳学习数学(理学士),然后是道德科学(哲学)(第二部分)。

他在1956年作为本科生第一次接触到计算机,并不令人振奋。他在莫里斯-威尔克斯的EDSAC(电子延迟存储自动计算器)上学习了10天的编程课程。他的反应是典型的决定性的:"编程不是一件非常美丽的事情。我下定决心,我这辈子都不会接近计算机"。他发现 "写一个又一个指令 "的活动是 "不优雅的 "和 "任意的"。

然而,罗宾对工具感兴趣,认为它们是用来扩展我们的能力的假肢装置。他非常实用,从他的灯绳上的木质几何形状,以及他在剑桥家中的杂物间(一个一尘不染的工作室,同时也是洗衣房)里整齐排列的凿子、镊子和锥子的全面收藏就可以看出。罗宾后来对作为工具的计算机着了迷。他很早就意识到,计算机不仅仅是单纯的计算设备,而是可以成为 "思想的工具"。

米尔纳从未攻读过博士学位。在当了一年学校教师和在苏伊士服了两年兵役之后,他的下一个计算机工作是在计算机制造商Ferranti,在那里他 "确保他们销售的所有新机器都能实际工作",并且还编写了部分编译器。1963年,他带着对编程更深入的理解可以形成更优雅的实践的信念,转入学术界。

在伦敦城市大学,他想知道数据库中的问题回答如何与关系代数相联系,但 "在这方面没有取得很大进展"。然后,在威尔士的斯旺西大学,他开始发表关于 "程序方案 "的文章,这是一种早期的类似于流程图的计算机程序操作模型。

米尔纳去牛津听了克里斯托弗-斯特拉奇和达纳-斯科特的讲座,他们一直在思考可计算函数,一个关于程序意义("指称语义")的抽象数学模型,以及关于可计算函数的逻辑(LCF),用于推理 "指称 "对象。米尔纳说,对程序验证和语义学感兴趣是他研究生涯的真正开始。在斯旺西,他写了他的第一个自动定理检验器,但仍然 "被做任何有趣的事情的困难所击垮"。

随后,他被邀请到斯坦福大学,在那里,他在约翰-麦卡锡的人工智能项目中做了两年(1971-1973)的研究助理。米尔纳对人类智能如何被 "放大 "更感兴趣,而不是对人工智能可能独立实现的目标感兴趣。米尔纳认为,机器可以帮助人类将斯科特-斯特拉奇的方法应用于实际例子中的指称语义。所需的计算是费力和容易出错的,但许多计算是机械的,可以用计算机来完成。

他与Whitfield Diffie、Richard Weyhrauch和Malcolm Newey一起开始工作,对Scott的LCF进行实施,他将其描述为

......旨在让用户以交互方式生成关于各种领域的可计算函数和函数的形式化证明,包括那些计算机科学家感兴趣的领域--例如整数、列表和计算机程序及其语义。

这个LCF证明助手包括一个子目标设施,允许用户把对一个证明的搜索分成对更小的子证明的搜索,机器会跟踪如何把证明的碎片重新组合起来。它还包括一个强大的简化机制,允许机器承担执行更多常规计算的负担。

这种架构的好处是,机械化的改进可以很容易地被纳入,以建立一个更强大的助手,而不会使现有的证明无效。此外,证明的模式可以被编码为战术,可以在许多证明中使用。证明搜索是subgoaling和简化步骤的结合。战术(一个例子可能是n的归纳法)将一些步骤的组合自动化。战术允许共同的模式被重复使用;它们不是简单的一个又一个指令的列表。这些想法本身已被重用,并在此基础上创建了各种逻辑的证明辅助工具。

米尔纳仍然对使用当时存在的编程语言的困难感到不满--他是用LISP编程的--并且对出错的可能性感到不满。我们怎么能确定这个系统不会引入不一致,从而毫无用处,因为它可以证明任何东西?当他在1974年搬到爱丁堡时,他开始了雄心勃勃的计划,开发和实现一种实用的编程语言,借鉴LISP,但也受到Peter Landin的ISWIM(If you See What I Mean)的很大影响,这种 "抽象 "语言从未真正实现,但它有明确的数学基础和基于Landin'SECD'抽象机器的操作语义。

米尔纳的新语言被设计为一种金属语言(因此它的名字是ML),用于实现一种叫做爱丁堡LCF的新证明辅助工具。它是一个强大而有效的实用工具,很好地适应了这项任务,并以兰丁的工作所体现的数学清晰度来定义。关于ML的进一步讨论可以在这里找到。

ML在当时是非常领先的。它是建立在简洁和良好的数学思想上的,被分离出来的,所以它们可以被独立地研究,并相对容易地重新混合和重复使用。ML影响了许多实用语言,包括Java、Scala和微软的F#。事实上,任何严肃的语言设计者都不应该忽视这个良好设计的例子。

同时,Milner继续担心语义学的基础问题,特别是程序的数学符号的属性和它的操作行为之间的联系。如果两个程序可以被观察到有不同的行为,它们必须有不同的指称,否则语义学就不健全。理想的情况是,反之亦然:任何两个在观察上无法区分的程序都应该有相同的指称。

然而,Gordon Plotkin发现了顺序编程的一个关键限制,这意味着类似ISWIM语言的自然Scott-Strachey模型可以有两个在观察上不可区分的程序,但有不同的指称。Milner构建了第一个完全抽象的模型,其中两个观察上相等的程序必须有相同的指称。

Milner担心对非决定性程序和并发进程进行建模,而Scott-Strachey语义学并没有方便地解决这个问题。分时和网络的出现使这成为一个实际的也是理论的问题。一个简单的顺序计算的函数模型并没有考虑到共享同一内存的两个程序之间的干扰的可能性,也没有考虑到客户机-服务器架构中的交互,或者一个系统与用户之间的交互。

创造巧妙的指称模型来解释这些特征是可能的,但是米尔纳想要一个 "以互动或交流为中心思想的语义理论"。他首先关注的是 "解释和数学框架的选择,一个小型的、良好的思想集合,它证明了微积分的操作是合理的"。经过长时间的思考和实验,他选择了罗伯特-凯勒(Robert M. Keller)的具有同步通信功能的标记过渡系统的看似简单的模型,他将观察等价的概念应用于此。这构成了他1980年出版的《通信系统计算》(CCS)[2]一书的基础,该书提出了一个 "并发的一般理论"。

但他并不满意。他观察到 "在观察等价性的定义中仍有选择的余地",并猜想CCS可能通过允许 "标签在通信中作为值传递 "而得到扩展。

在CCS出版后不久,米尔纳了解到大卫-帕克的 "二元化 "概念,这是观察等价概念的一个微妙但引人注目的改进。米尔纳在1989年的一本新书《通信与并发》[3]中完全重写了他的理论。CCS变化不大,但整个理论,特别是对观察等价的处理,更加优雅,不那么随意。

他早期工作的这三条线索--证明、并发和ML--在米尔纳的图灵奖奖状中得到了强调。代表计算机最高荣誉的奖杯,不显眼地放在他厨房里的一个花瓶和一碗水果之间。

如果在这一点上停止叙述,将无法公正地描述他的遗产。除了对该领域做出自己的技术贡献之外,米尔纳还雄辩地阐述了计算机科学作为一项智力工作的愿景。他在爱丁堡大学计算机科学基础实验室的就职演说中问道:"计算是一门实验科学吗?"他认为计算的理论应该根据其对实践的影响来检验。

在1997年接受博洛尼亚大学的荣誉博士学位时,他思考了编程的力量

人类设计的每一个工具都是一个假肢装置,而每一个假肢装置都有一个控制的手段。许多工具是物理的,它们的控制是手动的。相比之下,计算机是有史以来最复杂的工具,它们是心灵的工具;控制手段几乎不是肌肉的--它主要是语言的。很简单,计算机的多功能性与我们规定其行为的语言的多功能性完全相等,而且这似乎是无限制的。

然后阐述了他对信息学的看法

计算不仅是关于计算机的内部行动;它是关于计算机作为一个更大系统的一部分的行为方式。规定计算机行为的术语必须与我们描述此类系统中信息流的方式相协调。因此,计算学扩展为信息学,即信息与通信的科学[......]它可以提供一种精确的世界观,这不是任何先前存在的科学的范畴。

他的技术工作继续以这种更广泛的视角进行。他与约阿希姆-帕罗和大卫-沃克合作,在1992年开发了π-微积分,其中标签作为数值传递,创建了一个交流系统的微积分,可以自然地表达具有变化结构的过程。关于Milner的权威论述,请看通信和移动系统。π-微积分[5]。

他越来越关注确保理论对实践的影响。 例如,他作为特邀专家为网络服务编排描述语言(WS-CDL)做出了贡献;这种业务流程描述语言的各个方面都受到π微积分的启发。

该微积分还导致了进一步的形式化计算,用于描述和推理其他系统,包括用于加密协议的spi微积分和用于细胞信号通路的随机π微积分。这种广泛不同的应用加强了米尔纳对信息学的看法,认为它是一门可以应用于许多领域的信息和互动的科学。"他说:"信息学,"是计算机科学的同义词。'信息'这个词有一个好处:它们表达了这样一种见解:信息学行为比计算机所做的事情或计算是什么更广泛。"

米尔纳于2001年退休,但他并没有停止。π-微积分已经被应用于他没有预料到的互动的新例子,但他现在看到了更多。例如,一个

"理解泛在计算需要一系列令人生畏的概念:数据出处、隐私、授权、信任(在代理之间)、自我意识、自我管理、重新配置、故障恢复、目标、信念......,这个清单还可以扩展得更远。"

他兴致勃勃地开始了进一步模型的开发,"一个旨在为移动交互系统提供理论基础的地形模型"。

这一雄心勃勃的事业导致了他在2009年的最后一本书《通信代理的空间和运动》[7]中报告的 "大图式 "模型。在这本书中,米尔纳试图解释具有位置性和连接性的代理,这些代理可以通过运动(放置)和互动(连接)进行重新配置。他的目标是建立 "不仅是人工代理之间的互动行为,而且还有与自然代理之间的互动。最终,我们的信息学建模应该与自然科学相融合,并丰富自然科学的内容"。

Bigraphs对移动通信代理的并发和互动行为进行建模。应用包括计算系统生物学,其中的代理包括基因和蛋白质,以及互联网,其中的代理包括人、计算机和程序。就像米尔纳早期的工作一样,这注定会在计算机科学内部和外部产生深远而深刻的意义。

他在去世前几周接受了 "本周极客 "的采访,并在谈到他在bigraphs方面的工作时说。

我很想把这种工作带到设计和体验的第一线去,但我觉得我的时间不够长。我正在通过倾听和与那些将在的人交谈来弥补!

罗宾的倾听和交谈激发了各种团体对大图编程语言的研究,以及对大图在自然系统中的应用。2010年3月20日,他因心脏病发作去世,就在他心爱的妻子露西的葬礼后几天,他又回到了爱丁堡的一个椅子上,仍然充满了对未来的计划和项目。

作者。迈克尔-福尔曼
分享到:  QQ好友和群QQ好友和群 QQ空间QQ空间 腾讯微博腾讯微博 腾讯朋友腾讯朋友
收藏收藏 分享分享 分享淘帖 顶 踩
您需要登录后才可以回帖 登录 | 立即注册

本版积分规则

QQ|小黑屋|手机版|网站地图|关于我们|ECO中文网 ( 京ICP备06039041号  

GMT+8, 2024-11-25 19:44 , Processed in 0.126752 second(s), 19 queries .

Powered by Discuz! X3.3

© 2001-2017 Comsenz Inc.

快速回复 返回顶部 返回列表