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

文章基本信息

  • 标题:Head reduction and normalization in a call-by-value lambda-calculus
  • 本地全文:下载
  • 作者:Giulio Guerrieri
  • 期刊名称:OASIcs : OpenAccess Series in Informatics
  • 电子版ISSN:2190-6807
  • 出版年度:2015
  • 卷号:46
  • 页码:3-17
  • DOI:10.4230/OASIcs.WPTE.2015.3
  • 出版社:Schloss Dagstuhl -- Leibniz-Zentrum fuer Informatik
  • 摘要:Recently, a standardization theorem has been proven for a variant of Plotkin's call-by-value lambda-calculus extended by means of two commutation rules (sigma-reductions): this result was based on a partitioning between head and internal reductions. We study the head normalization for this call-by-value calculus with sigma-reductions and we relate it to the weak evaluation of original Plotkin's call-by-value lambda-calculus. We give also a (non-deterministic) normalization strategy for the call-by-value lambda-calculus with sigma-reductions.
  • 关键词:sequentialization; lambda-calculus; sigma-reduction; call-by-value; head reduction; internal reduction; (strong) normalization; evaluation; confluence
国家哲学社会科学文献中心版权所有