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

文章基本信息

  • 标题:Linear Logic and Strong Normalization
  • 本地全文:下载
  • 作者:Beniamino Accattoli
  • 期刊名称:LIPIcs : Leibniz International Proceedings in Informatics
  • 电子版ISSN:1868-8969
  • 出版年度:2013
  • 卷号:21
  • 页码:39-54
  • DOI:10.4230/LIPIcs.RTA.2013.39
  • 出版社:Schloss Dagstuhl -- Leibniz-Zentrum fuer Informatik
  • 摘要:Strong normalization for linear logic requires elaborated rewriting techniques. In this paper we give a new presentation of MELL proof nets, without any commutative cut-elimination rule. We show how this feature induces a compact and simple proof of strong normalization, via reducibility candidates. It is the first proof of strong normalization for MELL which does not rely on any form of confluence, and so it smoothly scales up to full linear logic. Moreover, it is an axiomatic proof, as more generally it holds for every set of rewriting rules satisfying three very natural requirements with respect to substitution, commutation with promotion, full composition, and Kesner's IE property. The insight indeed comes from the theory of explicit substitutions, and from looking at the exponentials as a substitution device.
  • 关键词:linear logic; proof nets; strong normalization; explicit substitutions
国家哲学社会科学文献中心版权所有