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".
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."
Grammar.
Kappa calculus consists of "types" and "expressions," given by the
grammar below:
In other words,
The formula_13 and the subscripts of , , and formula_14 are
sometimes omitted when they can be unambiguously determined from the
context.
Juxtaposition is often used as an abbreviation for a combination of
formula_14 and composition:
Typing rules.
"The presentation here uses sequents (formula_17) 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 formula_18 is used to indicate that expression e has source type formula_19 and target type formula_20.
Expressions in kappa calculus are assigned types according to the following rules:
In other words,
Equalities.
Kappa calculus obeys the following equalities:
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 formula_47 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 formula_47 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
If we define left-associative juxtaposition formula_50 as an abbreviation
for formula_51, then – assuming that
formula_52, formula_53, and
formula_54 – we can apply this function:
Since the expression formula_56 has source type , it is a "ground value" and may be passed as an argument to another function. If formula_57, then
Much like a curried function of type
formula_59 in lambda calculus, partial
application is possible:
However no higher types (i.e. formula_61) are involved. Note that because the source type of is not , 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
formula_54 then the expression
is well-typed as long as has type
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 the term
"functional completeness" in the context of combinatory algebra.
Kappa calculus arose out of efforts by Lambek to formulate an appropriate analogue of functional
completeness for arbitrary categories (see Hermida and Jacobs, section 1). Hasegawa later developed kappa
calculus into a usable (though simple) programming language including
arithmetic over natural numbers and primitive recursion. Connections to arrows
were later investigated 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 formula_7 expression. In such circumstances
the type operator is not a true cartesian product,
and is generally written to make this clear.