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:

${\displaystyle \tau =1\mid \tau \times \tau \mid \ldots }$

${\displaystyle 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 ${\displaystyle \tau _{1}}$ and ${\displaystyle \tau _{2}}$ are types then ${\displaystyle \tau _{1}\times \tau _{2}}$ is a type.
• Every variable is an expression
• If τ is a type then ${\displaystyle id_{\tau }}$ is an expression
• If τ is a type then ${\displaystyle !_{\tau }}$ is an expression
• If τ is a type and e is an expression then ${\displaystyle \operatorname {lift} _{\tau }(e)}$ is an expression
• If ${\displaystyle e_{1}}$ and ${\displaystyle e_{2}}$ are expressions then ${\displaystyle e_{1}\circ e_{2}}$ is an expression
• If x is a variable, τ is a type, and e is an expression, then ${\displaystyle \kappa x{:}1{\to }\tau \;.\;e}$ is an expression

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:

${\displaystyle e_{1}e_{2}\ {\overset {\operatorname {def} }{=}}\ e_{1}\circ \operatorname {lift} (e_{2})}$

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:

${\displaystyle {x{:}1{\to }\tau \;\in \;\Gamma } \over {\Gamma \vdash x:1{\to }\tau }}$	(Var)
${\displaystyle {} \over {\vdash id_{\tau }\;:\;\tau \to \tau }}$	(Id)
${\displaystyle {} \over {\vdash !_{\tau }\;:\;\tau \to 1}}$	(Bang)
${\displaystyle {\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)
${\displaystyle {\Gamma \vdash e{:}1{\to }\tau _{1}} \over {\Gamma \vdash \operatorname {lift} _{\tau _{2}}(e)\;:\;\tau _{2}\to (\tau _{1}\times \tau _{2})}}$	(Lift)
${\displaystyle {\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 ${\displaystyle x:1{\to }\tau }$ lets you conclude that ${\displaystyle x:1{\to }\tau }$
• Id: for any type τ, ${\displaystyle id_{\tau }:\tau {\to }\tau }$
• Bang: for any type τ, ${\displaystyle !_{\tau }:\tau {\to }1}$
• Comp: if the target type of ${\displaystyle e_{1}}$ matches the source type of ${\displaystyle e_{2}}$ they may be composed to form an expression ${\displaystyle e_{2}\circ e_{1}}$ with the source type of ${\displaystyle e_{1}}$ and target type of ${\displaystyle e_{2}}$
• Lift: if ${\displaystyle e:1{\to }\tau _{1}}$, then ${\displaystyle \operatorname {lift} _{\tau _{2}}(e):\tau _{2}{\to }(\tau _{1}\times \tau _{2})}$
• Kappa: if we can conclude that ${\displaystyle e:\tau _{2}\to \tau _{3}}$ under the assumption that ${\displaystyle x:1{\to }\tau _{1}}$, then we may conclude without that assumption that ${\displaystyle \kappa x{:}1{\to }\tau _{1}\,.\,e\;:\;\tau _{1}\times \tau _{2}\to \tau _{3}}$

Equalities

Kappa calculus obeys the following equalities:

• Neutrality: If ${\displaystyle f:\tau _{1}{\to }\tau _{2}}$ then ${\displaystyle f{\circ }id_{\tau _{1}}=f}$ and ${\displaystyle f=id_{\tau _{2}}{\circ }f}$
• Associativity: If ${\displaystyle f:\tau _{1}{\to }\tau _{2}}$, ${\displaystyle g:\tau _{2}{\to }\tau _{3}}$, and ${\displaystyle h:\tau _{3}{\to }\tau _{4}}$, then ${\displaystyle (h{\circ }g){\circ }f=h{\circ }(g{\circ }f)}$.
• Terminality: If ${\displaystyle f{:}\tau {\to }1}$ and ${\displaystyle g{:}\tau {\to }1}$ then ${\displaystyle f=g}$
• Lift-Reduction: ${\displaystyle (\kappa x.f)\circ \operatorname {lift} _{\tau }(c)=f[c/x]}$
• Kappa-Reduction: ${\displaystyle \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 ${\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 τ. 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

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

If we define left-associative juxtaposition ${\displaystyle 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:

${\displaystyle f\;a\;b\;c\;:\;1\to D}$

Since the expression ${\displaystyle f\;a\;b\;c}$ 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

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

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

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

However no higher types (i.e. ${\displaystyle (\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:

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

j c

is well-typed as long as j has type

${\displaystyle (C\times \alpha ){\to }\beta }$ for some α

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.

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 × type operator is not a true cartesian product, and is generally written ⊗ to make this clear.

References

1. Hasegawa, Masahito (1995). "Decomposing typed lambda calculus into a couple of categorical programming languages". In Pitt, David; Rydeheard, David E.; Johnstone, Peter (eds.). Category Theory and Computer Science. Category Theory and Computer Science: 6th International Conference, CTCS '95 Cambridge, United Kingdom, August 7–11, 1995 Proceedings. Lecture Notes in Computer Science. 953. Springer-Verlag Berlin Heidelberg. pp. 200–219. CiteSeerX 10.1.1.53.715. doi:10.1007/3-540-60164-3_28. ISBN 978-3-540-60164-7. ISSN 0302-9743. Lay summary – "Adam" answering "What are κ-categories?" on MathOverflow (August 31, 2010).
2. Barendregt, Hendrik Pieter, ed. (October 1, 1984). The Lambda Calculus: Its Syntax and Semantics. Studies in Logic and the Foundations of Mathematics. 103 (Revised ed.). Amsterdam, North Holland: Elsevier Science. ISBN 978-0-444-87508-2.
3. Lambek, Joachim (August 1, 1973). "Functional completeness of cartesian categories". Annals of Mathematical Logic (published March 1974). 6 (3–4): 259–292. doi:10.1016/0003-4843(74)90003-5. ISSN 0003-4843. Lay summary – "Adam" answering "What are κ-categories?" on MathOverflow (August 31, 2010).
4. Hermida, Claudio; Jacobs, Bart (December 1995). "Fibrations with indeterminates: contextual and functional completeness for polymorphic lambda calculi". Mathematical Structures in Computer Science. 5 (4): 501–531. doi:10.1017/S0960129500001213. ISSN 1469-8072.
5. Power, John; Thielecke, Hayo (1999). Wiedermann, Jiří; van Emde Boas, Peter; Nielsen, Mogens (eds.). Closed Freyd- and κ-Categories. Automata, Languages and Programming: 26th International Colloquium, ICALP'99 Prague, Czech Republic, July 11–15, 1999 Proceedings. Lecture Notes in Computer Science. 1644. Springer-Verlag Berlin Heidelberg. pp. 625–634. CiteSeerX 10.1.1.42.2151. doi:10.1007/3-540-48523-6_59. ISBN 978-3-540-66224-2. ISSN 0302-9743.