Adding algebraic rewriting to the untyped lambda calculus

DOI10.1016/0890-5401(92)90064-MzbMATH Open0769.68058MaRDI QIDQ1207945FDOQ1207945

Authors: Daniel J. Dougherty 

Publication date: 16 May 1993

Published in: Information and Computation (Search for Journal in Brave)

Recommendations

• Adding algebraic rewriting to the untyped lambda calculus (extended abstract)
• Combining algebraic rewriting, extensional lambda calculi, and fixpoints
• Applying universal algebra to lambda calculus
• scientific article; zbMATH DE number 1499090
• scientific article; zbMATH DE number 431764
• Confluence of the lambda calculus with left-linear algebraic rewriting
• A typed, algebraic, computational lambda-calculus
• scientific article; zbMATH DE number 2185664
• Semantics of a typed algebraic lambda-calculus
• Extending the lambda-calculus with unbind and rebind

zbMATH Keywords

confluenceterminationpolymorphic lambda calculusalgebraic rewritinguntyped lambda calculus

Mathematics Subject Classification ID

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

Cites Work

• The lambda calculus. Its syntax and semantics. Rev. ed.
• Termination of rewriting
• The calculus of constructions
• Title not available (Why is that?)
• Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems
• Title not available (Why is that?)
• Title not available (Why is that?)
• On the Church-Rosser property for the direct sum of term rewriting systems
• Title not available (Why is that?)
• On termination of the direct sum of term-rewriting systems
• Modular aspects of properties of term rewriting systems related to normal forms
• The Church-Rosser theorem for the typed lambda-calculus with pairing pairing
• Termination for the direct sum of left-linear term rewriting systems

Cited In (25)

• A domain model characterising strong normalisation
• The Computability Path Ordering: The End of a Quest
• Title not available (Why is that?)
• On the confluence of lambda-calculus with conditional rewriting
• Normal forms in combinatory logic
• A framework for defining logical frameworks
• On modular properties of higher order extensional lambda calculi
• Total unfolding: theory and applications
• Linear-algebraic λ-calculus: higher-order, encodings, and confluence.
• Confluence of the lambda calculus with left-linear algebraic rewriting
• Confluence via strong normalisation in an algebraic \(\lambda\)-calculus with rewriting
• Polymorphic rewriting conserves algebraic confluence
• Abstract data type systems
• Adding algebraic rewriting to the untyped lambda calculus (extended abstract)
• An insertion operator preserving infinite reduction sequences
• Adding algebraic rewriting to the calculus of constructions : Strong normalization preserved
• Termination of rewrite relations on \(\lambda\)-terms based on Girard's notion of reducibility
• Nominal rewriting
• Title not available (Why is that?)
• The algebraic lambda calculus
• A simplifier for untyped lambda expressions
• Title not available (Why is that?)
• Title not available (Why is that?)
• A combinatory logic approach to higher-order E-unification
• The vectorial \(\lambda\)-calculus

This page was built for publication: Adding algebraic rewriting to the untyped lambda calculus

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