Proofbinator

Proofbinator

Designed by	User:namotanu
Appeared in	2026
Dimensions	1
Computational class	Total
Reference implementation	Unimplemented
Influenced by	Lazy K

Overview

${\text{Proofbinator}}$ is an extreme, variable-free (Point-free) esoteric programming language based on a Pure Type System (similar to the Calculus of Constructions). In ${\text{Proofbinator}}$, there are no variables, no traditional lambda abstractions in user code, and no built-in data types (such as integers or booleans). Programs and types are unified and constructed entirely through combinators using Polish notation. Because it operates as a Pure Type System where types are terms, type checking and evaluation are deeply intertwined.

Syntax

${\text{Proofbinator}}$ uses prefix Polish notation with a single explicit application operator, represented by the backtick (`).

• ` a b represents the application of term $a$ to $b$. Due to prefix notation, nested applications are written as ` ` f a b (meaning $(f(a))(b)$).
• Variables: None. All expressions are composed of combinators and sorts/kinds.

Combinators and Types

The system features both term-level combinators (lowercase) and type/kind-level combinators (uppercase), operating under a Pure Type System framework.

Term-Level Combinators

• s: λT:*.λU:*.λV:*.λx:(T→U→V).λy:(T→U).λz:T.xz(yz)

 * Type: ΠT:*.ΠU:*.ΠV:*.(T→U→V)→(T→U)→T→V

• k: λT:*.λU:*.λx:T.λy:U.x

 * Type: ΠT:*.ΠU:*.T→U→T

• i: λT:*.λx:T.x

 * Type: ΠT:*.T→T

Type and Kind-Level Combinators

• S: λT:*.λU:*.λf:(T→U→*).λg:(T→U).Πx:T.fx(gx)

 * Type: ΠT:*.ΠU:*.(T→U→*)→(T→U)→*

• K: λT:*.λU:*.Πx:T.U

 * Type: *→*→*

• I: λT:*.Πx:T.x

 * Type: *→*

Evaluation and Type System

${\text{Proofbinator}}$ is built on a Pure Type System (PTS) framework: 1. Types as Terms: Types are terms and are reduced normally during evaluation (CoC-style evaluation). 2. No Built-in Types: Primitive data structures like integers, booleans, and arrays do not exist natively; programmers must encode and define them from scratch using combinators. 3. Evaluation Rules: Standard combinator reductions apply, where type arguments and proofs are reduced seamlessly alongside computation steps.

Examples

Since all data types (Booleans, Naturals) and proofs must be constructed from raw combinators under strict type constraints, writing even a basic program requires profound logical encoding.

User-Defined Types

Because types such as Int or Bool are not built-in, users construct them via Church-style or System F-style encodings using pure combinator expressions.