On the confluence of lambda-calculus with conditional rewriting
From MaRDI portal
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.
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)
Cites work
- scientific article; zbMATH DE number 1729952 (Why is no real title available?)
- scientific article; zbMATH DE number 4179332 (Why is no real title available?)
- scientific article; zbMATH DE number 4092755 (Why is no real title available?)
- scientific article; zbMATH DE number 3730111 (Why is no real title available?)
- scientific article; zbMATH DE number 3503199 (Why is no real title available?)
- scientific article; zbMATH DE number 4124996 (Why is no real title available?)
- scientific article; zbMATH DE number 1354162 (Why is no real title available?)
- scientific article; zbMATH DE number 512795 (Why is no real title available?)
- scientific article; zbMATH DE number 1142316 (Why is no real title available?)
- scientific article; zbMATH DE number 1499112 (Why is no real title available?)
- A rationale for conditional equational programming
- Adding algebraic rewriting to the untyped lambda calculus
- Combinatory reduction systems: Introduction and survey
- Conditional equational specifications of data types with partial operations for inductive theorem proving
- Conditional rewrite rules
- Conditional rewrite rules: Confluence and termination
- Confluence of the disjoint union of conditional term rewriting systems
- Confluence of the lambda calculus with left-linear algebraic rewriting
- Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems
- Definitions by rewriting in the Calculus of Constructions
- Foundations of Software Science and Computation Structures
- Higher order conditional rewriting and narrowing
- Modularity of strong normalization in the algebraic-λ-cube
- On termination and confluence properties of disjoint and constructor-sharing conditional rewrite systems
- On the Church-Rosser property for the direct sum of term rewriting systems
- Parallel reductions in \(\lambda\)-calculus
- Polymorphic rewriting conserves algebraic confluence
- Processes, Terms and Cycles: Steps on the Road to Infinity
- Pure patterns type systems
- The Clausal Theory of Types
- The lambda calculus. Its syntax and semantics. Rev. ed.
- Theorem proving modulo
Cited in
(7)- scientific article; zbMATH DE number 1390083 (Why is no real title available?)
- Foundations of Software Science and Computation Structures
- scientific article; zbMATH DE number 1303341 (Why is no real title available?)
- Confluence of the lambda calculus with left-linear algebraic rewriting
- scientific article; zbMATH DE number 7204433 (Why is no real title available?)
- Skew confluence and the lambda calculus with letrec
- On constructor rewrite systems and the lambda calculus
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)
