On the confluence of lambda-calculus with conditional rewriting

DOI10.1016/J.TCS.2009.07.058zbMATH Open1209.68104arXiv1109.4353OpenAlexW2117533875MaRDI QIDQ987976FDOQ987976

Claude Kirchner, Frédéric Blanqui, Colin Riba

Publication date: 24 August 2010

Published in: Theoretical Computer Science (Search for Journal in Brave)

Abstract: The confluence of untyped lambda-calculus with unconditional rewriting is now well un- derstood. In this paper, we investigate the confluence of lambda-calculus with conditional rewriting and provide general results in two directions. First, when conditional rules are algebraic. This extends results of M"uller and Dougherty for unconditional rewriting. Two cases are considered, whether �eta-reduction is allowed or not in the evaluation of conditions. Moreover, Dougherty's result is improved from the assumption of strongly normalizing �eta-reduction to weakly normalizing �eta-reduction. We also provide examples showing that outside these conditions, modularity of confluence is difficult to achieve. Second, we go beyond the algebraic framework and get new confluence results using a restricted notion of orthogonality that takes advantage of the conditional part of rewrite rules.

Full work available at URL: https://arxiv.org/abs/1109.4353

Recommendations

• Foundations of Software Science and Computation Structures
• scientific article; zbMATH DE number 512795
• Confluence of the lambda calculus with left-linear algebraic rewriting
• Conditional rewrite rules: Confluence and termination
• Adding algebraic rewriting to the untyped lambda calculus (extended abstract)

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42) Functional programming and lambda calculus (68N18)

Cites Work

• The lambda calculus. Its syntax and semantics. Rev. ed.
• Combinatory reduction systems: Introduction and survey
• Title not available (Why is that?)
• Theorem proving modulo
• Title not available (Why is that?)
• Conditional rewrite rules
• Conditional rewrite rules: Confluence and termination
• A rationale for conditional equational programming
• Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems
• Title not available (Why is that?)
• Title not available (Why is that?)
• The Clausal Theory of Types
• On termination and confluence properties of disjoint and constructor-sharing conditional rewrite systems
• Parallel reductions in \(\lambda\)-calculus
• Adding algebraic rewriting to the untyped lambda calculus
• On the Church-Rosser property for the direct sum of term rewriting systems
• Processes, Terms and Cycles: Steps on the Road to Infinity
• Title not available (Why is that?)
• Confluence of the disjoint union of conditional term rewriting systems
• Modularity of strong normalization in the algebraic-λ-cube
• Title not available (Why is that?)
• Pure patterns type systems
• Foundations of Software Science and Computation Structures
• Definitions by rewriting in the Calculus of Constructions
• Confluence of the lambda calculus with left-linear algebraic rewriting
• Polymorphic rewriting conserves algebraic confluence
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Conditional equational specifications of data types with partial operations for inductive theorem proving
• Higher order conditional rewriting and narrowing

Cited In (6)

• Foundations of Software Science and Computation Structures
• Title not available (Why is that?)
• Confluence of the lambda calculus with left-linear algebraic rewriting
• Skew confluence and the lambda calculus with letrec
• On constructor rewrite systems and the lambda calculus
• Title not available (Why is that?)

This page was built for publication: On the confluence of lambda-calculus with conditional rewriting

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q987976)