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

文章基本信息

  • 标题:Factorize Factorization
  • 本地全文:下载
  • 作者:Beniamino Accattoli ; Claudia Faggian ; Giulio Guerrieri
  • 期刊名称:LIPIcs : Leibniz International Proceedings in Informatics
  • 电子版ISSN:1868-8969
  • 出版年度:2021
  • 卷号:183
  • 页码:6:1-6:25
  • DOI:10.4230/LIPIcs.CSL.2021.6
  • 出版社:Schloss Dagstuhl -- Leibniz-Zentrum fuer Informatik
  • 摘要:We present a new technique for proving factorization theorems for compound rewriting systems in a modular way, which is inspired by the Hindley-Rosen technique for confluence. Specifically, our approach is well adapted to deal with extensions of the call-by-name and call-by-value λ-calculi. The technique is first developed abstractly. We isolate a sufficient condition (called linear swap) for lifting factorization from components to the compound system, and which is compatible with β-reduction. We then closely analyze some common factorization schemas for the λ-calculus. Concretely, we apply our technique to diverse extensions of the λ-calculus, among which de' Liguoro and Piperno’s non-deterministic λ-calculus and - for call-by-value - Carraro and Guerrieri’s shuffling calculus. For both calculi the literature contains factorization theorems. In both cases, we give a new proof which is neat, simpler than the original, and strikingly shorter.
  • 关键词:Lambda Calculus; Rewriting; Reduction Strategies; Factorization
国家哲学社会科学文献中心版权所有