首页    期刊浏览 2024年11月25日 星期一
登录注册

文章基本信息

  • 标题:Evaluating functions as processes
  • 本地全文:下载
  • 作者:Beniamino Accattoli
  • 期刊名称:Electronic Proceedings in Theoretical Computer Science
  • 电子版ISSN:2075-2180
  • 出版年度:2013
  • 卷号:110
  • 页码:41-55
  • DOI:10.4204/EPTCS.110.6
  • 出版社:Open Publishing Association
  • 摘要:A famous result by Milner is that the lambda-calculus can be simulated inside the pi-calculus. This simulation, however, holds only modulo strong bisimilarity on processes, i.e. there is a slight mismatch between beta-reduction and how it is simulated in the pi-calculus. The idea is that evaluating a lambda-term in the pi-calculus is like running an environment-based abstract machine, rather than applying ordinary beta-reduction. In this paper we show that such an abstract-machine evaluation corresponds to linear weak head reduction, a strategy arising from the representation of lambda-terms as linear logic proof nets, and that the relation between the two is as tight as it can be. The study is also smoothly rephrased in the call-by-value case, introducing a call-by-value analogous of linear weak head reduction.
国家哲学社会科学文献中心版权所有