The search for a reduction in combinatory logic equivalent to λβ-reduction, Part II

详细信息    查看全文

• 作者：Jonathan P. Seldin ^{jonathan.seldin@uleth.ca}
• 关键词：λ-Calculus ; Combinatory logic ; β-Reduction ; βη-Reduction ; Abstraction ; Irreducible terms ; Normal form
• 刊名：Theoretical Computer Science
• 出版年：2017
• 出版时间：8 February 2017
• 年：2017
• 卷：663
• 期：Complete
• 页码：34-58
• 全文大小：504 K
• 卷排序：663

文摘

This second part of [13] takes up the showing in detail of the properties in [13, §3] for the proposed definitions of abstraction and combinatory β-reduction. The difficult cases are (R3) (the Church–Rosser Theorem) and (R6) on irreducible CL-terms.