In mathematical logic, category theory, and computer science, kappa calculus is a formal system for defining first-order functions.
Contents
- Definition
- Grammar
- Typing rules
- Equalities
- Properties
- Categorical semantics
- Examples
- History
- Variants
- References
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".
Because its functions are not first-class objects, evaluation of kappa calculus expressions does not require closures.
Definition
The definition below has been adapted from the diagrams on pages 205 and 207 of Hasegawa.
Grammar
Kappa calculus consists of types and expressions, given by the grammar below:
In other words,
The
Juxtaposition is often used as an abbreviation for a combination of "
Typing rules
The presentation here uses sequents (
In kappa calculus an expression has two types: the type of its source and the type of its target. The notation
Expressions in kappa calculus are assigned types according to the following rules:
In other words,
Equalities
Kappa calculus obeys the following equalities:
The last two equalities are reduction rules for the calculus, rewriting from left to right.
Properties
The type 1 can be regarded as the unit type. Because of this, any two functions whose argument type is the same and whose result type is 1 should be equal – since there is only a single value of type 1 both functions must return that value for every argument (Terminality).
Expressions with type
Categorical semantics
Kappa calculus is intended to be the internal language of contextually complete categories.
Examples
Expressions with multiple arguments have source types which are "right-imbalanced" binary trees. For example, a function f with three arguments of types A, B, and C and result type D will have type
If we define left-associative juxtaposition (f c) as an abbreviation for
Since the expression
Much like a curried function of type
However no higher types (i.e.
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
is well-typed as long as j has type
History
Barendregt originally introduced the term "functional completeness" in the context of combinatory algebra. Kappa calculus arose out of efforts by Lambek to formulate an appropriate analogue of functional completeness for arbitrary categories (see Hermida and Jacobs, section 1). Hasegawa later developed kappa calculus into a usable (though simple) programming language including arithmetic over natural numbers and primitive recursion. Connections to arrows were later investigated by Power, Thielecke, and others.
Variants
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