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.

DefinitionEdit

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

GrammarEdit

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

 
 

In other words,

  • 1 is a type
  • If   and   are types then   is a type.
  • Every variable is an expression
  • If τ is a type then   is an expression
  • If τ is a type then   is an expression
  • If τ is a type and e is an expression then   is an expression
  • If   and   are expressions then   is an expression
  • If x is a variable, τ is a type, and e is an expression, then   is an expression

The   and the subscripts of id, !, and   are sometimes omitted when they can be unambiguously determined from the context.

Juxtaposition is often used as an abbreviation for a combination of   and composition:

 

Typing rulesEdit

The presentation here uses sequents ( ) 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   is used to indicate that expression e has source type   and target type  .

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

  (Var)
  (Id)
  (Bang)
  (Comp)
  (Lift)
  (Kappa)

In other words,

  • Var: assuming   lets you conclude that  
  • Id: for any type τ,  
  • Bang: for any type τ,  
  • Comp: if the target type of   matches the source type of   they may be composed to form an expression   with the source type of   and target type of  
  • Lift: if  , then  
  • Kappa: if we can conclude that   under the assumption that  , then we may conclude without that assumption that  

EqualitiesEdit

Kappa calculus obeys the following equalities:

  • Neutrality: If   then   and  
  • Associativity: If  ,  , and  , then  .
  • Terminality: If   and   then  
  • Lift-Reduction:  
  • Kappa-Reduction:   if x is not free in h

The last two equalities are reduction rules for the calculus, rewriting from left to right.

PropertiesEdit

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   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   for some τ. This is the basic mechanism which ensures that all functions are first-order.

Categorical semanticsEdit

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

ExamplesEdit

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

 

If we define left-associative juxtaposition   as an abbreviation for  , then – assuming that  ,  , and   – we can apply this function:

 

Since the expression   has source type 1, it is a "ground value" and may be passed as an argument to another function. If  , then

 

Much like a curried function of type   in lambda calculus, partial application is possible:

 

However no higher types (i.e.  ) 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:

 

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   then the expression

j c

is well-typed as long as j has type

  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.

HistoryEdit

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.

VariantsEdit

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

ReferencesEdit

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