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

文章基本信息

  • 标题:A Theory of Explicit Substitutions with Safe and Full Composition
  • 本地全文:下载
  • 作者:Delia Kesner
  • 期刊名称:Logical Methods in Computer Science
  • 印刷版ISSN:1860-5974
  • 电子版ISSN:1860-5974
  • 出版年度:2009
  • 卷号:5
  • 期号:03
  • DOI:10.2168/LMCS-5(3:1)2009
  • 出版社:Technical University of Braunschweig
  • 摘要:

    Many different systems with explicit substitutions have been proposed to implement a large class of higher-order languages. Motivations and challenges that guided the development of such calculi in functional frameworks are surveyed in the first part of this paper. Then, very simple technology in named variable-style notation is used to establish a theory of explicit substitutions for the lambda-calculus which enjoys a whole set of useful properties such as full composition, simulation of one-step beta-reduction, preservation of beta-strong normalisation, strong normalisation of typed terms and confluence on metaterms. Normalisation of related calculi is also discussed.

国家哲学社会科学文献中心版权所有