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 $fabc$ 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 $fa$ 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 2 3 4 Hasegawa, Masahito (1995). Pitt, David; Rydeheard, David E.; Johnstone, Peter, eds. "Decomposing typed lambda calculus into a couple of categorical programming languages". Category Theory and Computer Science: 6th International Conference, CTCS '95 Cambridge, United Kingdom, August 7–11, 1995 Proceedings. Lecture Notes in Computer Science. Springer-Verlag Berlin Heidelberg. 953: 200–219. doi:10.1007/3-540-60164-3_28. ISBN 978-3-540-60164-7. ISSN 0302-9743. Lay summary – "Adam" answering "What are $\kappa$ -categories?" on MathOverflow (August 31, 2010).
↑ 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 0-444-87508-5.
↑ Lambek, Joachim (August 1, 1973). "Functional completeness of cartesian categories". Annals of Mathematical Logic. Amsterdam, North Holland: North-Holland Publishing Company (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 $\kappa$ -categories?" on MathOverflow (August 31, 2010).
↑ Hermida, Claudio; Jacobs, Bart (December 1995). "Fibrations with indeterminates: contextual and functional completeness for polymorphic lambda calculi". Mathematical Structures in Computer Science. Cambridge, England: Cambridge University Press. 5 (4): 501–531. doi:10.1017/S0960129500001213. ISSN 1469-8072.
↑ Power, John; Thielecke, Hayo (1999). Wiedermann, Jiří; van Emde Boas, Peter; Nielsen, Mogens, eds. "Closed Freyd- and $\kappa$ -Categories". Automata, Languages and Programming: 26th International Colloquium, ICALP’99 Prague, Czech Republic, July 11–15, 1999 Proceedings. Lecture Notes in Computer Science. Springer-Verlag Berlin Heidelberg. 1644: 625–634. doi:10.1007/3-540-48523-6_59. ISBN 978-3-540-66224-2. ISSN 0302-9743.

This article is issued from Wikipedia - version of the 6/2/2016. The text is available under the Creative Commons Attribution/Share Alike but additional terms may apply for the media files.