Combinatory reduction systems: Introduction and survey
type: Item
instance of: scholarly article
title: Combinatory reduction systems: Introduction and survey
zbMATH Open document ID: 0796.03024
DOI: 10.1016/0304-3975(93)90091-7
author: Jan Willem Klop
author: Vincent van Oostrom
author: Femke van Raamsdonk
published in: Theoretical Computer Science
publication date: 1994-09-26T00:00:00Z
full work available at URL: https://ir.cwi.nl/pub/5233
review text: This paper investigates combinatory reduction systems (CRSs), i.e. usual first-order term rewriting systems with the presence of bound variables. It introduces orthogonal CRSs (illustrated with many examples) and gives an outline of the proof of confluence. It also shows an extension of the finite development theorem.
Mathematics Subject Classification ID: 03B40
Mathematics Subject Classification ID: 68Q42
zbMATH DE Number: 501171
zbMATH Keywords: lambda calculus
zbMATH Keywords: combinatory reduction systems
zbMATH Keywords: term rewriting systems
zbMATH Keywords: confluence
zbMATH Keywords: extension of the finite developments theorem
describes a project that uses: ETPS
describes a project that uses: Automath
MaRDI profile type: Publication
OpenAlex ID: W4212868911
cites work: Q4726218
cites work: Pairing Without Conventional Restraints
cites work: The lambda calculus. Its syntax and semantics. Rev. ed.
cites work: Q4385533
cites work: Q4283231
cites work: Q3205213
cites work: Q4205074
cites work: Q3235339
cites work: Q3785893
cites work: Q3899466
cites work: Q4385532
cites work: Q3922646
cites work: Q3773876
cites work: The Equivalence of Complete Reductions
cites work: Standard and Normal Reductions
cites work: Q4722037
cites work: Q4692468
cites work: Q4001983
cites work: Unique normal forms for lambda calculus with surjective pairing
cites work: Sequential evaluation strategies for parallel-or and related reduction systems
cites work: On the longest perpetual reductions in orthogonal expression reduction systems
cites work: Q3918095
cites work: Q4023825
cites work: Q4101795
cites work: Modular properties of conditional term rewriting systems
cites work: A complete inference system for a class of regular behaviours
cites work: Confluence of the lambda calculus with left-linear algebraic rewriting
cites work: Q3880323
cites work: Q4281481
cites work: LCF considered as a programming language
cites work: Q5632554
cites work: Confluence and superdevelopments
cites work: Q3486543
cites work: Combinators, \(\lambda\)-terms and proof theory
cites work: Parallel reductions in \(\lambda\)-calculus
cites work: Q4281488
cites work: A theory of binding structures and applications to rewriting
cites work: Rewriting, and equational unification: the higher-order cases
cites work: The Clausal Theory of Types
description: scientific article; zbMATH DE number 501171