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

文章基本信息

  • 标题:Full Abstraction for the Resource Lambda Calculus with Tests, through Taylor Expansion
  • 本地全文:下载
  • 作者:Thomas Ehrhard ; Antonio Bucciarelli ; Alberto Carraro
  • 期刊名称:Logical Methods in Computer Science
  • 印刷版ISSN:1860-5974
  • 电子版ISSN:1860-5974
  • 出版年度:2012
  • 卷号:8
  • 期号:4
  • 页码:1
  • DOI:10.2168/LMCS-8(4:3)2012
  • 出版社:Technical University of Braunschweig
  • 摘要:We study the semantics of a resource-sensitive extension of the lambda calculus in a canonical reflexive object of a category of sets and relations, a relational version of Scott's original model of the pure lambda calculus. This calculus is related to Boudol's resource calculus and is derived from Ehrhard and Regnier's differential extension of Linear Logic and of the lambda calculus. We extend it with new constructions, to be understood as implementing a very simple exception mechanism, and with a "must" parallel composition. These new operations allow to associate a context of this calculus with any point of the model and to prove full abstraction for the finite sub-calculus where ordinary lambda calculus application is not allowed. The result is then extended to the full calculus by means of a Taylor Expansion formula. As an intermediate result we prove that the exception mechanism is not essential in the finite sub-calculus.
  • 其他关键词:Resource lambda calculus, relational semantics, full abstraction, differential linear logic
国家哲学社会科学文献中心版权所有