Combinatory reduction systems: Introduction and survey (Q1314356): Difference between revisions

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.

0 references

zbMATH Keywords

lambda calculus

0 references

combinatory reduction systems

0 references

term rewriting systems

0 references

confluence

0 references

extension of the finite developments theorem

0 references

describes a project that uses

ETPS

0 references

Automath

0 references

MaRDI profile type

MaRDI publication profile

0 references

cites work

Q4726218

0 references

Pairing Without Conventional Restraints

0 references

The lambda calculus. Its syntax and semantics. Rev. ed.

0 references

0 references

0 references

0 references

0 references

0 references

0 references

0 references

0 references

0 references

0 references

The Equivalence of Complete Reductions

0 references

Standard and Normal Reductions

0 references

Q4722037

0 references

Q4692468

0 references

Q4001983

0 references

Unique normal forms for lambda calculus with surjective pairing

0 references

Sequential evaluation strategies for parallel-or and related reduction systems

0 references

On the longest perpetual reductions in orthogonal expression reduction systems

0 references

Q3918095

0 references

Q4023825

0 references

Q4101795

0 references

Modular properties of conditional term rewriting systems

0 references

A complete inference system for a class of regular behaviours

0 references

Confluence of the lambda calculus with left-linear algebraic rewriting

0 references

Q3880323

0 references

Q4281481

0 references

LCF considered as a programming language

0 references

Q5632554

0 references

Confluence and superdevelopments

0 references

Q3486543

0 references

Combinators, \(\lambda\)-terms and proof theory

0 references

Parallel reductions in \(\lambda\)-calculus

0 references

Q4281488

0 references

A theory of binding structures and applications to rewriting

0 references

Rewriting, and equational unification: the higher-order cases

0 references

The Clausal Theory of Types

0 references

Identifiers

zbMATH Open document ID

0796.03024

0 references

DOI

10.1016/0304-3975(93)90091-7

0 references

Mathematics Subject Classification ID

0 references

0 references

0 references

0 references

Sitelinks

Mathematics(1 entry)

mardi Publication:1314356

@@ Property / describes a project that uses @@
+ETPS
@@ Property / describes a project that uses: ETPS / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Automath
@@ Property / describes a project that uses: Automath / rank @@
+Normal rank
@@ Property / MaRDI profile type @@
+MaRDI publication profile
@@ Property / MaRDI profile type: MaRDI publication profile / rank @@
+Normal rank
@@ Property / OpenAlex ID @@
+W4212868911
@@ Property / OpenAlex ID: W4212868911 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4726218
@@ Property / cites work: Q4726218 / rank @@
+Normal rank
@@ Property / cites work @@
+Pairing Without Conventional Restraints
@@ Property / cites work: Pairing Without Conventional Restraints / rank @@
+Normal rank
@@ Property / cites work @@
+The lambda calculus. Its syntax and semantics. Rev. ed.
+Normal rank
@@ Property / cites work @@
+Q4385533
@@ Property / cites work: Q4385533 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4283231
@@ Property / cites work: Q4283231 / rank @@
+Normal rank
@@ Property / cites work @@
+Q3205213
@@ Property / cites work: Q3205213 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4205074
@@ Property / cites work: Q4205074 / rank @@
+Normal rank
@@ Property / cites work @@
+Q3235339
@@ Property / cites work: Q3235339 / rank @@
+Normal rank
@@ Property / cites work @@
+Q3785893
@@ Property / cites work: Q3785893 / rank @@
+Normal rank
@@ Property / cites work @@
+Q3899466
@@ Property / cites work: Q3899466 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4385532
@@ Property / cites work: Q4385532 / rank @@
+Normal rank
@@ Property / cites work @@
+Q3922646
@@ Property / cites work: Q3922646 / rank @@
+Normal rank
@@ Property / cites work @@
+Q3773876
@@ Property / cites work: Q3773876 / rank @@
+Normal rank
@@ Property / cites work @@
+The Equivalence of Complete Reductions
@@ Property / cites work: The Equivalence of Complete Reductions / rank @@
+Normal rank
@@ Property / cites work @@
+Standard and Normal Reductions
@@ Property / cites work: Standard and Normal Reductions / rank @@
+Normal rank
@@ Property / cites work @@
+Q4722037
@@ Property / cites work: Q4722037 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4692468
@@ Property / cites work: Q4692468 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4001983
@@ Property / cites work: Q4001983 / rank @@
+Normal rank
@@ Property / cites work @@
+Unique normal forms for lambda calculus with surjective pairing
+Normal rank
@@ Property / cites work @@
+Sequential evaluation strategies for parallel-or and related reduction systems
+Normal rank
@@ Property / cites work @@
+On the longest perpetual reductions in orthogonal expression reduction systems
+Normal rank
@@ Property / cites work @@
+Q3918095
@@ Property / cites work: Q3918095 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4023825
@@ Property / cites work: Q4023825 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4101795
@@ Property / cites work: Q4101795 / rank @@
+Normal rank
@@ Property / cites work @@
+Modular properties of conditional term rewriting systems
+Normal rank
@@ Property / cites work @@
+A complete inference system for a class of regular behaviours
+Normal rank
@@ Property / cites work @@
+Confluence of the lambda calculus with left-linear algebraic rewriting
+Normal rank
@@ Property / cites work @@
+Q3880323
@@ Property / cites work: Q3880323 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4281481
@@ Property / cites work: Q4281481 / rank @@
+Normal rank
@@ Property / cites work @@
+LCF considered as a programming language
@@ Property / cites work: LCF considered as a programming language / rank @@
+Normal rank
@@ Property / cites work @@
+Q5632554
@@ Property / cites work: Q5632554 / rank @@
+Normal rank
@@ Property / cites work @@
+Confluence and superdevelopments
@@ Property / cites work: Confluence and superdevelopments / rank @@
+Normal rank
@@ Property / cites work @@
+Q3486543
@@ Property / cites work: Q3486543 / rank @@
+Normal rank
@@ Property / cites work @@
+Combinators, \(\lambda\)-terms and proof theory
@@ Property / cites work: Combinators, \(\lambda\)-terms and proof theory / rank @@
+Normal rank
@@ Property / cites work @@
+Parallel reductions in \(\lambda\)-calculus
@@ Property / cites work: Parallel reductions in \(\lambda\)-calculus / rank @@
+Normal rank
@@ Property / cites work @@
+Q4281488
@@ Property / cites work: Q4281488 / rank @@
+Normal rank
@@ Property / cites work @@
+A theory of binding structures and applications to rewriting
+Normal rank
@@ Property / cites work @@
+Rewriting, and equational unification: the higher-order cases
+Normal rank
@@ Property / cites work @@
+The Clausal Theory of Types
@@ Property / cites work: The Clausal Theory of Types / rank @@
+Normal rank
@@ links / mardi / name / links / mardi / name @@
+Publication:1314356