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:

$\tau = 1 \mid \tau\times\tau \mid \ldots$

$e = x \mid id_\tau \mid !_\tau \mid \operatorname{lift}_\tau(e) \mid e \circ e \mid \kappa x:1{\to}\tau . e$

In other words,

• 1 is a type
• If $\tau_1$ and $\tau_2$ are types then $\tau_1\times\tau_2$ is a type.
• Every variable is an expression
• If $\tau$ is a type then $id_\tau$ is an expression
• If $\tau$ is a type then $!_\tau$ is an expression
• If $\tau$ is a type and e is an expression then $\operatorname{lift}_\tau(e)$ is an expression
• If $e_1$ and $e_2$ are expressions then $e_1\circ e_2$ is an expression
• If x is a variable, $\tau$ is a type, and e is an expression, then $\kappa x{:}1{\to}\tau\;.\;e$ is an expression

The $:1{\to}\tau$ and the subscripts of id, !, and $\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 "$\operatorname{lift}$" and composition:

$e_1 e_2 \overset{def}{=} e_1 \circ \operatorname{lift}(e_2)$

Typing rules

The presentation here uses sequents ($\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 $e:\tau_1{\to}\tau_2$ is used to indicate that expression e has source type ${\tau_1}$ and target type ${\tau_2}$.

Expressions in kappa calculus are assigned types according to the following rules:

${x{:}1{\to}\tau\;\in\;\Gamma}\over{\Gamma \vdash x : 1{\to}\tau }$ (Var)

${}\over{\vdash id_\tau\;:\;\tau\to\tau }$ (Id)

${}\over{\vdash !_\tau\;:\;\tau\to 1 }$ (Bang)

${\Gamma \vdash e_1{:}\tau_1{\to}\tau_2 \;\;\;\;\;\; \Gamma \vdash e_2{:}\tau_2{\to}\tau_3 }\over{\Gamma \vdash e_2\circ e_1 : \tau_1{\to}\tau_3 }$ (Comp)

${\Gamma \vdash e{:}1{\to}\tau_1} \over {\Gamma \vdash \operatorname{lift}_{\tau_2}(e)\;:\;\tau_2\to(\tau_1\times\tau_2) }$ (Lift)

${\Gamma,\;x{:}1{\to}\tau_1\;\vdash\;e:\tau_2{\to}\tau_3} \over {\Gamma \vdash \kappa x{:}1{\to}\tau_1\,.\,e\;:\;\tau_1\times\tau_2\to\tau_3 }$ (Kappa)

In other words,

• Var: assuming $x:1{\to}\tau$ lets you conclude that $x:1{\to}\tau$
• Id: for any type $\tau$, $id_\tau:\tau{\to}\tau$
• Bang: for any type $\tau$, $!_\tau:\tau{\to}1$
• Comp: if the target type of $e_1$ matches the source type of $e_2$ they may be composed to form an expression $e_2\circ e_1$ with the source type of $e_1$ and target type of $e_2$
• Lift: if $e:1{\to}\tau_1$, then $\operatorname{lift}_{\tau_2}(e):\tau_2{\to}(\tau_1\times\tau_2)$
• Kappa: if we can conclude that $e:\tau_2\to\tau_3$ under the assumption that $x:1{\to}\tau_1$, then we may conclude without that assumption that $\kappa x{:}1{\to}\tau_1\,.\,e\;:\;\tau_1\times\tau_2\to\tau_3$

Equalities

Kappa calculus obeys the following equalities:

• Neutrality: If $f:\tau_1{\to}\tau_2$ then $f{\circ}id_{\tau_1}=f$ and $f=id_{\tau_2}{\circ}f$
• Associativity: If $f:\tau_1{\to}\tau_2$, $g:\tau_2{\to}\tau_3$, and $h:\tau_3{\to}\tau_4$, then $(h{\circ}g){\circ}f = h{\circ}(g{\circ}f)$.
• Terminality: If $f{:}\tau{\to}1$ and $g{:}\tau{\to}1$ then $f=g$
• Lift-Reduction: $(\kappa x.f)\circ \operatorname{lift}_\tau(c) = f[c/x]$
• Kappa-Reduction: $\kappa x. (h\circ \operatorname{lift}_\tau(x)) = h$ if x is not free in h

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 $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 $1{\to}\tau$ for some $\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

$f : A\times (B\times (C\times 1)) \to D$

If we define left-associative juxtaposition (f c) as an abbreviation for $(f\circ \operatorname{lift}(c))$, then – assuming that $a:1{\to}A$, $b:1{\to}B$, and $c:1{\to}C$ – we can apply this function:

$f\;a\;b\;c\;:\;1 \to D$

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

$g\;(f\;a\;b\;c)\;:\;E \to F$

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

$f\;a\;:\;B\times (C\times 1) \to D$

However no higher types (i.e. $(\tau{\to}\tau){\to}\tau$) are involved. 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:

$h\;(f\;a)$

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 $c:1{\to}C$ then the expression

$j\;c$

is well-typed as long as j has type $(C\times\alpha){\to}\beta$ for some $\alpha$ and $\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 $!_\tau$ expression. In such circumstances the $\times$ type operator is not a true cartesian product, and is generally written $\otimes$ to make this clear.

References

1. Hasegawa, M. (1995). "Decomposing typed lambda calculus into a couple of categorical programming languages". Category Theory and Computer Science. Lecture Notes in Computer Science 953. p. 200. doi:10.1007/3-540-60164-3_28. ISBN 978-3-540-60164-7.
2. Barendregt, Hendrik Pieter (1984), The Lambda Calculus: Its Syntax and Semantics, Studies in Logic and the Foundations of Mathematics 103 (Revised ed.), North Holland, Amsterdam. Corrections, ISBN 0-444-87508-5 External link in |publisher= (help)
3. Lambek, J. (1974). "Functional completeness of cartesian categories". Annals of Mathematical Logic 6 (3–4): 259. doi:10.1016/0003-4843(74)90003-5.
4. Hermida, C.; Jacobs, B. (2009). "Fibrations with indeterminates: Contextual and functional completeness for polymorphic lambda calculi". Mathematical Structures in Computer Science 5 (4): 501. doi:10.1017/S0960129500001213.
5. Power, J.; Thielecke, H. (1999). "Closed Freyd- and κ-categories". Automata, Languages and Programming. Lecture Notes in Computer Science 1644. p. 625. doi:10.1007/3-540-48523-6_59. ISBN 978-3-540-66224-2.

• $\kappa$, MathOverflow question 37180.