Adding algebraic rewriting to the untyped lambda calculus (extended abstract)

DOI10.1007/3-540-53904-2_84zbMath1503.03023OpenAlexW1585482631MaRDI QIDQ5055747

Daniel J. Dougherty

Publication date: 9 December 2022

Published in: Rewriting Techniques and Applications (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/3-540-53904-2_84

zbMATH Keywords

normal formalgebraic reductionlambda calculusalgebraic termstable term

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42) Combinatory logic and lambda calculus (03B40)

Related Items (5)

More problems in rewriting ⋮ Problems in rewriting III ⋮ Higher-order rewrite systems and their confluence ⋮ Termination of rewrite relations on \(\lambda\)-terms based on Girard's notion of reducibility ⋮ Confluence of the lambda calculus with left-linear algebraic rewriting

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Termination of rewriting
• The calculus of constructions
• On termination of the direct sum of term-rewriting systems
• The lambda calculus, its syntax and semantics
• The Church-Rosser theorem for the typed lambda-calculus with pairing pairing
• Polymorphic rewriting conserves algebraic strong normalization
• Polymorphic rewriting conserves algebraic confluence
• Modular aspects of properties of term rewriting systems related to normal forms
• Termination for the direct sum of left-linear term rewriting systems
• On the Church-Rosser property for the direct sum of term rewriting systems
• Adding algebraic rewriting to the calculus of constructions : Strong normalization preserved

This page was built for publication: Adding algebraic rewriting to the untyped lambda calculus (extended abstract)