In mathematical logic, category theory, and computer science, kappa calculus is a formal system for defining first-order functions.
Unlike lambda calculus, kappa calculus has no higher-order functions; its functions are not first class objects.
Kappa-calculus can be regarded as "a reformulation of the first-order fragment of typed lambda calculus".
[1] Because its functions are not first-class objects, evaluation of kappa calculus expressions does not require closures.
The definition below has been adapted from the diagrams on pages 205 and 207 of Hasegawa.
[1] Kappa calculus consists of types and expressions, given by the grammar below: In other words, The
are sometimes omitted when they can be unambiguously determined from the context.
) rather than hypothetical judgments in order to ease comparison with the simply typed lambda calculus.
Expressions in kappa calculus are assigned types according to the following rules: In other words, Kappa calculus obeys the following equalities: The last two equalities are reduction rules for the calculus, rewriting from left to right.
This is the basic mechanism which ensures that all functions are first-order.
Kappa calculus is intended to be the internal language of contextually complete categories.
Expressions with multiple arguments have source types which are "right-imbalanced" binary trees.
has source type 1, it is a "ground value" and may be passed as an argument to another function.
in lambda calculus, partial application is possible: However no higher types (i.e.
Note that because the source type of f a is not 1, the following expression cannot be well-typed under the assumptions mentioned so far: Because successive application is used for multiple arguments it is not necessary to know the arity of a function in order to determine its typing; for example, if we know that
then the expression is well-typed as long as j has type and β.
This property is important when calculating the principal type of an expression, something which can be difficult when attempting to exclude higher-order functions from typed lambda calculi by restricting the grammar of types.
Barendregt originally introduced[2] the term "functional completeness" in the context of combinatory algebra.
Kappa calculus arose out of efforts by Lambek[3] to formulate an appropriate analogue of functional completeness for arbitrary categories (see Hermida and Jacobs,[4] section 1).
Hasegawa later developed kappa calculus into a usable (though simple) programming language including arithmetic over natural numbers and primitive recursion.
[1] Connections to arrows were later investigated[5] by Power, Thielecke, and others.
It is possible to explore versions of kappa calculus with substructural types such as linear, affine, and ordered types.
These extensions require eliminating or restricting the
In such circumstances the × type operator is not a true cartesian product, and is generally written ⊗ to make this clear.