Kappa calculus explained

In mathematical logic, category theory, andcomputer science, kappa calculus is aformal system for defining first-orderfunctions.

Unlike lambda calculus, kappa calculus has nohigher-order functions; its functions arenot first class objects. Kappa-calculus can beregarded as "a reformulation of the first-order fragment of typedlambda calculus".

Because its functions are not first-class objects, evaluation of kappacalculus expressions does not requireclosures.

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 thegrammar below:

\tau = 1 \mid \tau x \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 x \tau} _{2} is a type.

• Every variable is an expression
• If is a type then

id _{\tau} is an expression

• If is a type then

! _{\tau} is an expression

• If 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, 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,, and \operatorname{lift} aresometimes omitted when they can be unambiguously determined from thecontext.

Juxtaposition is often used as an abbreviation for a combination of

\operatorname{lift} and composition:e _{1} e _{2 \overset\operatorname{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

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 x \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 x \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,

id _{\tau:\tau{\to}\tau}

• Bang: for any type,

! _{\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 x \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 x \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 can be regarded as the unit type. Because of this, any two functions whose argument type is the same and whose result type is should be equal – since there is only a single value of type 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 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 . This is the basic mechanism which ensures that all functions are first-order.

Categorical semantics

Kappa calculus is intended to be the internal language ofcontextually complete categories.

Examples

Expressions with multiple arguments have source types which are"right-imbalanced" binary trees. For example, a function f with threearguments of types A, B, and C and result type D will have type

f : A x (B x (C x 1 )) \to D

If we define left-associative juxtaposition

f c as an abbreviationfor (f\circ \operatorname{lift}(c)) , then – assuming thata: 1 {\to}A , b: 1 {\to}B , andc: 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, it is a "ground value" and may be passed as an argument to another function. If g:(D x E){\to}F , theng (f a b c) : E \to F

Much like a curried function of type

A{\to}(B{\to}(C{\to}D)) in lambda calculus, partialapplication is possible:f a : B x (C x 1 ) \to D

However no higher types (i.e.

(\tau{\to}\tau){\to}\tau ) are involved. Note that because the source type of is not, the following expression cannot be well-typed under the assumptions mentioned so far:h (f a)

Because successive application is used for multiplearguments it is not necessary to know the arity of a function inorder to determine its typing; for example, if we know that

c: 1 {\to}C then the expression

is well-typed as long as has type

(C x \alpha){\to}\beta for some and . This property is important when calculatingthe principal type of an expression, somethingwhich can be difficult when attempting to exclude higher-orderfunctions from typed lambda calculi by restricting the grammar of types.

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 functionalcompleteness for arbitrary categories (see Hermida and Jacobs, section 1). Hasegawa later developed kappacalculus into a usable (though simple) programming language includingarithmetic over natural numbers and primitive recursion. Connections to arrowswere later investigated by Power, Thielecke, and others.

Variants

It is possible to explore versions of kappa calculus withsubstructural types such as linear, affine,and ordered types. These extensions require eliminating orrestricting the

! _{\tau} expression. In such circumstancesthe type operator is not a true cartesian product,and is generally written to make this clear.

References

^{[1] [2] [3] [4] [5]}

Notes and References

1. Lambek . Joachim . Joachim Lambek . August 1, 1973 . Functional completeness of cartesian categories . Annals of Mathematical Logic . March 1974 . 6 . 3–4 . 259–292 . 10.1016/0003-4843(74)90003-5 . 0003-4843.
   • Web site: Adam . August 31, 2010 . What are κappa-categories? . MathOverflow .
2. 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 . 10.1017/S0960129500001213 . 3428512 . 1469-8072.
3. Book: October 1, 1984 . Barendregt . Hendrik Pieter . The Lambda Calculus: Its Syntax and Semantics . Studies in Logic and the Foundations of Mathematics . Revised . Amsterdam, North Holland . Elsevier Science . 103 . 978-0-444-87508-2.
4. Book: Hasegawa . Masahito . Category Theory and Computer Science . Decomposing typed lambda calculus into a couple of categorical programming languages . 1995 . Pitt . David . Rydeheard . David E. . Johnstone . Peter . Peter Johnstone (mathematician) . Lecture Notes in Computer Science . Springer-Verlag Berlin Heidelberg . 953 . 200–219 . 10.1007/3-540-60164-3_28 . 978-3-540-60164-7 . 0302-9743. 10.1.1.53.715 .
   • Web site: Adam . August 31, 2010 . What are κappa-categories? . MathOverflow .
5. Book: Power . John . Thielecke . Hayo . Automata, Languages and Programming . Closed Freyd- and κ-categories . 1999 . Wiedermann . Jiří . van Emde Boas . Peter . Peter van Emde Boas . Nielsen . Mogens . Lecture Notes in Computer Science . Springer-Verlag Berlin Heidelberg . 1644 . 625–634 . 10.1007/3-540-48523-6_59 . 978-3-540-66224-2 . 0302-9743. 10.1.1.42.2151 .