Foundations of Simplicity

Combinator Completeness of Simplicity

Delving Into Simplicity

Combinator Completeness of Simplicity

Simplicity Types
Unit Type
Sum Type
Product Type
Core Simplicity Expressions
Two Basic Operations
Three Composition Combinators
Four More Combinators
The Nine Core Combinators
Simplicity and the Sequent Calculus
Values are not Expressions
Simplicity's Completeness Theorem
Conclusion

In this chapter we introduce the core Simplicity language and show that the language is complete, meaning that any finite computation can be expressed within it.

Simplicity Types

Simplicity supports three fundamental type constructors. The product type A × B represents parallel composition outputs, while the sum type A + B (tagged union) handles conditional composition inputs. The third type is the unit type.

Unit Type

The unit type, denoted 𝟙 or ONE, contains exactly one value: the empty tuple ⟨⟩ or (). This zero-bit data type carries no information.

Sum Type

A sum type A + B combines two types with tags indicating "left" or "right." Values are written as σᴸ(a) or inl(a) for left-tagged values and σᴿ(b) or inr(b) for right-tagged values. The tags remain distinct even when combining identical types.

Boolean Type

The type 𝟙 + 𝟙, denoted 𝟚 or TWO, represents a one-bit type with two values. By convention, σᴸ⟨⟩ represents false/zero, while σᴿ⟨⟩ represents true/one.

Product Type

Product types A × B contain value pairs written as ⟨a, b⟩ or (a, b). The type 𝟚 × 𝟚 has four values, distinct from the four values in 𝟚 + 𝟚.

Core Simplicity Expressions

Operations are denoted as f : A ⊢ B, meaning input type A and output type B. Simplicity is "first-order" — it lacks function types.

Two Basic Operations

The core language provides two basic operations:

Identity (iden). The identity operation passes its input through unchanged:

iden : A ⊢ A
⟦iden⟧(a) = a

Unit (unit). The unit operation discards its input and returns the empty tuple:

unit : A ⊢ 𝟙
⟦unit⟧(a) = ⟨⟩

These form families with one operation per type.

Three Composition Combinators

Sequential composition uses comp f g (written f ⨾ g or f >>> g):

If f : A ⊢ B and g : B ⊢ C, then
comp f g : A ⊢ C
⟦f ⨾ g⟧(a) = ⟦g⟧(⟦f⟧(a))

Parallel composition uses pair f g (written f ▵ g or f &&& g):

If f : A ⊢ B and g : A ⊢ C, then
pair f g : A ⊢ B × C
⟦f ▵ g⟧(a) = ⟨⟦f⟧(a), ⟦g⟧(a)⟩

Conditional composition uses case f g : (A + B) × C ⊢ D, providing branches access to shared environment C:

If f : A × C ⊢ D and g : B × C ⊢ D, then
case f g : (A + B) × C ⊢ D
⟦case f g⟧⟨σᴸ(a), c⟩ = ⟦f⟧⟨a, c⟩
⟦case f g⟧⟨σᴿ(b), c⟩ = ⟦g⟧⟨b, c⟩

Why does conditional composition take this shape — a sum paired with a shared environment C — rather than a simpler copair f g : A + B ⊢ C that merely picks a branch? Because a bare copair cannot express distribution: the function dist : (A + B) × C ⊢ A × C + B × C that pushes a shared input into whichever branch is taken. By building the environment C directly into case, Simplicity obtains conditional composition and distribution from a single combinator — one of the key design decisions that keeps the core language down to nine combinators.

Four More Combinators

Product consumption uses take and drop:

take extracts the left element:

If f : A ⊢ C, then
take f : A × B ⊢ C
⟦take f⟧⟨a, b⟩ = ⟦f⟧(a)

drop extracts the right element:

If f : B ⊢ C, then
drop f : A × B ⊢ C
⟦drop f⟧⟨a, b⟩ = ⟦f⟧(b)

Sum production uses injl and injr:

injl wraps with a left tag:

If f : A ⊢ B, then
injl f : A ⊢ B + C
⟦injl f⟧(a) = σᴸ(⟦f⟧(a))

injr wraps with a right tag:

If f : A ⊢ C, then
injr f : A ⊢ B + C
⟦injr f⟧(a) = σᴿ(⟦f⟧(a))

The Nine Core Combinators

In total, Simplicity has exactly nine core combinators:

Combinator	Purpose
`iden`	Pass input through
`unit`	Discard input
`comp`	Sequential composition
`pair`	Parallel composition
`case`	Conditional composition
`take`	Extract left from product
`drop`	Extract right from product
`injl`	Inject into left of sum
`injr`	Inject into right of sum

Simplicity and the Sequent Calculus

Simplicity's design derives from the conjunctive-disjunctive fragment of Gentzen's sequent calculus. More precisely, it is a variant of the functional interpretation of the sequent calculus, which is itself analogous to the Curry-Howard correspondence between natural deduction and the lambda calculus. The combinator rules exhibit "smaller types in premises than conclusions," enabling the Bit Machine — Simplicity's abstract stack machine interpreter — to minimize data copying during execution.

Values are not Expressions

Simplicity expressions denote operations, not values. The notation scribe b : A ⊢ B represents a unique expression always returning value b, serving as notational convenience rather than a combinator. This mirrors Bitcoin Script, where operations like OP_1 push values rather than express them directly.

Simplicity's Completeness Theorem

With all nine combinators in hand, how do we know we aren't missing something — that these nine really are enough? The Simplicity Completeness theorem answers this: for any function between (finite) Simplicity types, some Simplicity expression denotes it. The proof is constructive — it shows how to build the expression:

Decompose the input: Using nested case expressions, fully decompose any input of any type into its constituent bits
Build a lookup table: For each possible input, use scribe to produce the corresponding output
Assemble: The nested cases and scribes together form a giant lookup table that implements the function

This theorem is formally verified in the Rocq proof assistant (formerly Coq). The proof is part of the official Simplicity repository and has been machine-checked for correctness.

While the completeness theorem guarantees that Simplicity's nine combinators can express any function between (finite) Simplicity types, resulting expressions from the lookup-table construction are impractically large. A function on 256-bit inputs would require a lookup table with 2²⁵⁶ entries. This is why the next chapters focus on building efficient expressions that exploit the structure of computations, rather than brute-forcing everything through lookup tables.

Conclusion

Simplicity's core language includes a type system and combinators enabling any finite computation. While the Completeness theorem guarantees expressiveness, resulting expressions from the generic construction are impractically large. Practical Simplicity development involves exploiting computational structure for succinct expressions. The next chapters explore data structures, transaction interactions, and additional combinators.

Quiz

scr4032.2

1/5

The completeness proof builds any function by nesting case to decompose the input and scribe for each output. Why is it only a theoretical tool?