Combinatory reduction systems: Introduction and survey

DOI10.1016/0304-3975(93)90091-7zbMath0796.03024OpenAlexW4212868911MaRDI QIDQ1314356

Vincent van Oostrom, Femke van Raamsdonk, Jan Willem Klop

Publication date: 26 September 1994

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

Full work available at URL: https://ir.cwi.nl/pub/5233

zbMATH Keywords

confluenceterm rewriting systemslambda calculuscombinatory reduction systemsextension of the finite developments theorem

Mathematics Subject Classification ID

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

Related Items (57)

A modular construction of type theories ⋮ Higher-order interpretations and program complexity ⋮ Introducing \(\llparenthesis\lambda\rrparenthesis\), a \(\lambda \)-calculus for effectful computation ⋮ Logical foundations for hybrid type-logical grammars ⋮ Nominal rewriting ⋮ Harnessing First Order Termination Provers Using Higher Order Dependency Pairs ⋮ Combinatory reduction systems with explicit substitution that preserve strong normalisation ⋮ Combining algebraic rewriting, extensional lambda calculi, and fixpoints ⋮ Strong normalization from weak normalization in typed \(\lambda\)-calculi ⋮ Expressing combinatory reduction systems derivations in the rewriting calculus ⋮ On explicit substitution with names ⋮ Labelled reductions, runtime errors, and operational subsumption ⋮ Size-based termination of higher-order rewriting ⋮ Lambda calculus with explicit recursion ⋮ Higher-order rewrite systems and their confluence ⋮ Computing in unpredictable environments: semantics, reduction strategies, and program transformations ⋮ Developing developments ⋮ Termination of rewrite relations on \(\lambda\)-terms based on Girard's notion of reducibility ⋮ Counterexamples in infinitary rewriting with non-fully-extended rules ⋮ Strong normalisation in two Pure Pattern Type Systems ⋮ On Normalisation of Infinitary Combinatory Reduction Systems ⋮ A metamodel of access control for distributed environments: applications and properties ⋮ A prismoid framework for languages with resources ⋮ Theorem proving modulo ⋮ Capture-avoiding substitution as a nominal algebra ⋮ Intersection type assignment systems with higher-order algebraic rewriting ⋮ Expression reduction systems with patterns ⋮ Checking overlaps of nominal rewriting rules ⋮ The variable containment problem ⋮ Gödel's system \(\mathcal T\) revisited ⋮ Recursive Functions with Pattern Matching in Interaction Nets ⋮ Variable binding operators in transition system specifications ⋮ Unnamed Item ⋮ Infinitary combinatory reduction systems ⋮ Normalisation for higher-order calculi with explicit substitutions ⋮ Matching and alpha-equivalence check for nominal terms ⋮ Unnamed Item ⋮ On the confluence of lambda-calculus with conditional rewriting ⋮ Inductive-data-type systems ⋮ On the longest perpetual reductions in orthogonal expression reduction systems ⋮ A new connective in natural deduction, and its application to quantum computing ⋮ Nominal Confluence Tool ⋮ Axiomatizing permutation equivalence ⋮ Comparing Böhm-Like Trees ⋮ On the Relation between Sized-Types Based Termination and Semantic Labelling ⋮ Introducing a Calculus of Effects and Handlers for Natural Language Semantics ⋮ Order-sorted inductive types ⋮ Confluence of extensional and non-extensional \(\lambda\)-calculi with explicit substitutions ⋮ The algebra of recursive graph transformation language UnCAL: complete axiomatisation and iteration categorical semantics ⋮ Descendants and origins in term rewriting. ⋮ Perpetuality and uniform normalization in orthogonal rewrite systems ⋮ A Framework for Defining Logical Frameworks ⋮ From Functional Programs to Interaction Nets via the Rewriting Calculus ⋮ The Power of Closed Reduction Strategies ⋮ Complete Laziness: a Natural Semantics ⋮ Token-passing Nets for Functional Languages ⋮ Interaction nets and term rewriting systems (extended abstract)

Uses Software

• ETPS
• Automath

Cites Work

• A theory of binding structures and applications to rewriting
• Modular properties of conditional term rewriting systems
• The lambda calculus. Its syntax and semantics. Rev. ed.
• A complete inference system for a class of regular behaviours
• Unique normal forms for lambda calculus with surjective pairing
• Confluence of the lambda calculus with left-linear algebraic rewriting
• LCF considered as a programming language
• Sequential evaluation strategies for parallel-or and related reduction systems
• Combinators, \(\lambda\)-terms and proof theory
• Pairing Without Conventional Restraints
• The Equivalence of Complete Reductions
• Standard and Normal Reductions
• Rewriting, and equational unification: the higher-order cases
• Confluence and superdevelopments
• Parallel reductions in \(\lambda\)-calculus
• On the longest perpetual reductions in orthogonal expression reduction systems
• The Clausal Theory of Types
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Combinatory reduction systems: Introduction and survey