The word problem for Smullyan's lark combinator is decidable

DOI10.1016/S0747-7171(89)80044-6MaRDI QIDQ1114668zbMATH OpenFDO

Authors Richard Statman

Publication date 1989

Published in Journal of Symbolic Computation (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/S0747-7171(89)80044-6

zbMATH Keywords

applicative combinatorsBWBlark combinatorparadoxical combinator

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40) Decidability (number-theoretic aspects) (11U05)

Review text

Smullyan's ``lark combinator L (Curry's BWB) is specified by the reduction rule Lxy\(\to x(yy)\). LL defines the paradoxical combinator Y. The author shows that several other interesting combinators can be defined in terms of L only. The main part of the paper involves showing that the problem of deciding whether two applicative combinators of L are equal is solvable.

Recommendations

• scientific article; zbMATH DE number 1615239
• A decidable word problem without equivalent canonical term rewriting system
• On a connection between the word problem and decidability of the equational theory
• Decidability, Recursive Enumerability and Kleene Hierarchy ForL-Subsets
• scientific article; zbMATH DE number 2208122
• scientific article; zbMATH DE number 149873
• scientific article; zbMATH DE number 7724207
• The decision problem for some logics for finite words on infinite alphabets
• A finitely axiomatizable undecidable equational theory with recursively solvable word problems
• scientific article; zbMATH DE number 176152

Cites work

• A foray into combinatory logic
• Combinatory logic. With two sections by William Craig.
• scientific article; zbMATH DE number 4037787 (Why is no real title available?)
• scientific article; zbMATH DE number 3713674 (Why is no real title available?)
• The lambda calculus, its syntax and semantics

Cited in

(10)

• Almost all one-rule Thue systems have decidable word problems
• How to decide the lark
• Displaying and deciding substructural logics. I: Logics with contraposition
• The combinator S
• scientific article; zbMATH DE number 1615239 (Why is no real title available?)
• On repetitive right application of \(B\)-terms
• The combinator M and the Mockingbird lattice
• On properties of \(B\)-terms
• Mockingbird lattices
• Algebra of self-replication

This page was built for publication: The word problem for Smullyan's lark combinator is decidable

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