Unverified

Basis Decision for Proper Combinators

A proper combinator is a closed lambda term of the form $\lambda x_1\ldots x_n.M$ , where $M$ contains no abstraction and every free variable of $M$ belongs to $\{x_1,\ldots,x_n\}$ . A finite set $S$ of combinators is combinatorially complete if every closed lambda term is representable, up to the intended lambda-calculus equality, by an applicative term over $S$ . Is there an algorithm that, given a finite set of proper combinators, decides whether it is combinatorially complete?

Download

Abstract

Is combinatorial completeness decidable for finite sets of proper combinators? The unrestricted finite normal-combinator problem is undecidable, whereas the linear proper case is decidable.

Background and progress

Richard Statman submitted this decision problem in 1993. The source contrasts the open proper-combinator case with undecidability for finite sets of normal combinators that may be improper and with decidability for linear proper combinators. The status statements here follow the TLCA page's July 21, 2014 snapshot and have not been independently updated after that date [Statman, 1993]. The original open problem appears at https://tlca.di.unito.it/opltlca/opltlcasu13.html.

Reference papers

Basis Decision for Proper CombinatorsRichard StatmanTLCA Open Problem List · 1993 ↗

Basis Decision for Proper Combinators

Coming soon

Organizer