# Kappa calculus

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.

## Definition

The definition below has been adapted from the diagrams on pages 205 and 207 of Hasegawa.[1]

### Grammar

Kappa calculus consists of types and expressions, given by the grammar below:

In other words,

The ${\displaystyle :1{\to }\tau }$ and the subscripts of id, !, and ${\displaystyle \operatorname {lift} }$ are sometimes omitted when they can be unambiguously determined from the context.

Juxtaposition is often used as an abbreviation for a combination of "${\displaystyle \operatorname {lift} }$" and composition:

### Typing rules

The presentation here uses sequents (${\displaystyle \Gamma \vdash e:\tau }$) rather than hypothetical judgments in order to ease comparison with the simply typed lambda calculus. This requires the additional Var rule, which does not appear in Hasegawa[1]

In kappa calculus an expression has two types: the type of its source and the type of its target. The notation ${\displaystyle e:\tau _{1}{\to }\tau _{2}}$ is used to indicate that expression e has source type ${\displaystyle {\tau _{1}}}$ and target type ${\displaystyle {\tau _{2}}}$.

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 ${\displaystyle 1{\to }\tau }$ can be regarded as "constants" or values of "ground type"; this is because 1 is the unit type, and so a function from this type is necessarily a constant function. Note that the kappa rule allows abstractions only when the variable being abstracted has the type ${\displaystyle 1{\to }\tau }$ for some ${\displaystyle \tau }$. This is the basic mechanism which ensures that all functions are first-order.

## 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 ${\displaystyle (f\circ \operatorname {lift} (c))}$, then – assuming that ${\displaystyle a:1{\to }A}$, ${\displaystyle b:1{\to }B}$, and ${\displaystyle c:1{\to }C}$ – we can apply this function:

Since the expression ${\displaystyle fabc}$ has source type 1, it is a "ground value" and may be passed as an argument to another function. If ${\displaystyle g:(D\times E){\to }F}$, then

Much like a curried function of type ${\displaystyle A{\to }(B{\to }(C{\to }D))}$ in lambda calculus, partial application is possible:

However no higher types (i.e. ${\displaystyle (\tau {\to }\tau ){\to }\tau }$) are involved. Note that because the source type of ${\displaystyle fa}$ 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 ${\displaystyle c:1{\to }C}$ then the expression

is well-typed as long as j has type ${\displaystyle (C\times \alpha ){\to }\beta }$ for some ${\displaystyle \alpha }$ and ${\displaystyle \beta }$. 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.

## History

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.

## 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 ${\displaystyle !_{\tau }}$ expression. In such circumstances the ${\displaystyle \times }$ type operator is not a true cartesian product, and is generally written ${\displaystyle \otimes }$ to make this clear.

## References

1. Template:Cite doi
2. {{#invoke:citation/CS1|citation |CitationClass=citation }}
3. Template:Cite doi
4. Template:Cite doi
5. Template:Cite doi