Kappa Calculus

Origin. Masahito Hasegawa, "Decomposing typed lambda calculus into a couple of categorical programming languages" (CTCS 1995), which introduced κ as the first-order half of a decomposition; Power and Thielecke's κ-categories supply the categorical semantics. The point of the system is subtractive: what is the typed λ-calculus once function types are removed?

Models. The simply typed λ-calculus's power comes from the function type A → B being a type like any other, so functions are values and can be passed and returned. Remove that and something remains: contexts of one variable, composition, and the ability to lift a value into a context. That residue is the κ-calculus, and it is exactly the first-order fragment — it can express every first-order function and no higher-order one.

Formalism.

Types: τ ::= 1 | τ × τ | b No arrow. Function types are not types.

Judgment: Terms are typed relative to at most one free variable: x : a ⊢ t : b which is a morphism a → b, not a value of type a → b.

The two operators: κ (kappa): abstracts the single variable, forming a morphism. x : a ⊢ t : b gives κx. t : a → b as an arrow, not as a term of arrow type lift: injects a closed term into a context.

Composition: The calculus's only way to build: arrows compose, and κ binds the single variable. There is no application of a term to a term — only substitution into a context.

The decomposition (Hasegawa): Simply typed λ-calculus ≅ κ-calculus + ζ-calculus κ supplies the first-order structure (contextual completeness); ζ supplies the higher-order structure (currying). Together they are the λ-calculus; separately, κ is exactly what first-order means.

Categorical semantics: κ-calculus is the internal language of a category with finite products — no exponentials required. Adding exponentials is adding ζ, and gives a CCC. So the decomposition mirrors the categorical one: products, then closure.

Expressive power: Every first-order function on the base types is definable. No higher-order function is, and the restriction is a theorem, not a convention.

Symbols.

Symbol	Unicode	Name	Meaning
κ	U+03BA	Greek small letter kappa	Abstracts the single variable
ζ	U+03B6	Greek small letter zeta	The higher-order half of the decomposition
λ	U+03BB	Greek small letter lamda	Abstraction, in the calculus κ is a fragment of
τ	U+03C4	Greek small letter tau	Metavariable ranging over types
×	U+00D7	Multiplication sign	Product, the only type former besides base and 1
1	U+0031	Digit one	Terminal type
→	U+2192	Rightwards arrow	An arrow a → b, which here is a judgment and not a type
⊢	U+22A2	Right tack / Turnstile	Typing judgment, x : a ⊢ t : b
:	U+003A	Colon	Ascription of a type to a variable or a term
≅	U+2245	Approximately equal to	The decomposition, λ ≅ κ + ζ
lift	—	Injection	Closed term into a context
b	—	Base type	An unstructured type
::=	—	Grammar production	Defines the type syntax
CCC	—	Cartesian closed category	Finite products together with exponentials

Metatheory. Hasegawa's decomposition is the entry's content: the λ-calculus is not primitive but the join of two calculi, one contextual and one functional, and κ is precisely the fragment whose models are categories with finite products rather than cartesian closed ones. That makes "first-order" a structural notion instead of a syntactic restriction — the usual definition of the first-order fragment is λ-terms whose types have no nested arrows, which is a filter on a larger language, and κ is the language whose terms are all and only those, so the characterization is a theorem rather than a stipulation. Because κ-terms translate into the simply typed λ-calculus, confluence and strong normalization are inherited, and since no type contains an arrow, type checking is immediate. The categorical statement is the sharp one: κ is the internal language of finite products, ζ adds exponentials, and the two together are the CCC correspondence; Power and Thielecke's κ-categories (1999) axiomatize the first half directly.

Applies to. The first-order fragment of typed λ-calculus, characterized rather than filtered. Categorical semantics of products versus exponentials. Compilation, where first-order code needs no closures and the boundary matters. The decomposition of λ into its structural components.

Limitations. The absence of function types restricts not only what can be written but what can be said: an arrow a → b is a judgment rather than a type, so no term takes an arrow as an argument, returns one, or stores one, and in consequence there is no self-application, no fixed-point combinator, and no encoding of recursion — recursion must be added as a primitive. Currying is unavailable, so multi-argument functions have to go through products and the calculus cannot dispense with × the way a λ-calculus with exponentials can. The decomposition is not canonical: nothing establishes that κ and ζ are the only way to factor λ. And the calculus's interest is entirely in what it explains about λ, so there is no implementation and no independent motivation.