Combinator Junk

Introduction

Combinator Junk (CJ) has a static type system where each term has a specific type known in advance. Instances of function application that violate the type system are simply invalid, as are terms containing them. The type system of CJ is based on that of simply typed lambda calculus. Each type is either $\mathbb {N}$, the type of the naturals, or of the form $A\to B$, where A and B stand for some types each, meaning a function type from type A to type B. Only the types arising from these rules are valid. To apply a term (say $f$) to another term (say $x$), the type of $f$ must be a function type from the type of $x$ to some type. Note that the types $A\to (B\to C)$ and $(A\to B)\to C$ are different and that $A\to B\to C$ refers to the former.

All CJ terms are created through application from a limited set of combinators. Though the number of combinators is technically infinite, most are duplicates, as in differently typed variants based on the same underlying idea. For example, one has both the combinator $K:\mathbb {N} \to (\mathbb {N} \to \mathbb {N} )\to \mathbb {N}$ and the combinator $K:\mathbb {N} \to \mathbb {N} \to \mathbb {N}$. In a system of punning, the same name may be used for two different combinators which differ in type but "act" the same, with the type signature disambiguating if necessary. When listing the combinators, using type names like A or B is used to mean that for all types A and B, one has such a combinator, with A and B replaced with the actual types.

Combinators

The K combinators have type $A\to (B\to A)$.

Kxy = x

The S combinators have type $(A\to (B\to C))\to (A\to B)\to A\to C$.

Sxyz = xz(yz)

The church combinators have type $\mathbb {N} \to (A\to A)\to A\to A$.

church zero f x = x

church (succ n) f x = f (church n f x)

• In other words, church n is the Church numeral corresponding to n, though always with a specific type.

The zero term (also described as a combinator on this page) has type $\mathbb {N}$.

• It represents the natural number 0.

The succ combinator has type $\mathbb {N} \to \mathbb {N}$.

• It represents the successor operator, which adds 1 to a natural number. However, we actually define addition in terms of succ and the other combinators.

Syntax used for examples

Various different syntaxes could be provided for CJ. The following syntax uses ASCII characters and is intended to be easily readable:

• Each combinator takes one line.
• Each combinator, aside from zero and succ, has its type written after it.
• This type is written as in (N -> N) -> N, with N for naturals, -> for function types, and brackets for disambiguation.
• The function type constructor is right-associative: N -> N -> N means N -> (N -> N), etc.
• To notate the application of one term to another, write after the first term, starting from an empty line, the second term with all of its lines indented by two extra spaces.

Example terms

Two

succ
  succ
    zero

Term reducing to succ

K : (N -> N) -> N -> (N -> N)
  succ
  zero

Term reducing to the succ of succ of zero

K : N -> N -> N
  succ
    succ
      zero
  zero

Addition (the function that calculates the sum of two naturals)

S : (N -> (N -> N) -> N -> N) -> (N -> N -> N) -> N -> N -> N
  church : N -> (N -> N) -> N -> N
  K : (N -> N) -> N -> N -> N
    succ

Computational features

• Combinator Junk is not Turing-complete. However, it is for this very reason that termination can be guaranteed.
• All terms of type $\mathbb {N}$ have a normal form that consists of repeatedly applying succ to zero.
• CJ can represent, to my understanding, all primitive recursive functions.
• CJ can also represent many functions that are not primitive recursive.
• Given a CJ term of type $\mathbb {N} \to \mathbb {N}$, it is undecidable whether applying it to any natural always yields zero.

Extensions

Potential IO methods

A pair of terms of types $\mathbb {N} \to \mathbb {N}$ and $\mathbb {N} \to \mathbb {N} \to \mathbb {N}$ could be used to represent a program that can interact with a user. Call the first term getOutput and the second term updateState. The program would keep track of the current state as a natural number, initially with the value zero. The program would perform the following on a loop: 1. "Call" getOutput with the current state, yielding a natural number to be displayed to the user in a base with a lot of digits, each represented using a different character. The idea is that this will look like text. 2. Wait for the user to give a response, written using the set of characters used for the base, and interpret it as a natural number. "Call" updateState with the previous state and the natural number gotten from the user, giving a new natural number which the current state will be set to.

Implementation

None yet! However, I intend to add one to this page by June 2026.