Kappa calculus

From Wikipedia, the free encyclopedia
Jump to: navigation, search

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[edit]

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

Grammar[edit]

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


\tau = 1 | \tau\times\tau | \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[edit]

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[edit]

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[edit]

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[edit]

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

Examples[edit]

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[edit]

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[edit]

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[edit]

  1. ^ a b c d 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.  edit
  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 
  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.  edit
  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.  edit
  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.  edit