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; Barendregt's Handbook treatment and Power–Thielecke's work on 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.

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. The categorical statement is the sharp one: κ is the internal language of products, ζ adds exponentials, and the two together are the CCC correspondence.

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. Small literature and no implementation: κ is a way of seeing the λ-calculus, not a language anyone writes in. The single-variable restriction makes the syntax awkward — multi-argument functions go through products, which is fine categorically and painful notationally. And the decomposition's interest is entirely in what it explains about λ, so the calculus has no independent motivation.

© 2026 Lingenic LLC