Kappa calculus

Last updated September 05, 2023

In mathematical logic, category theory, and computer science, kappa calculus is a formal system for defining first-order functions.

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 $τ$ 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 $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 {\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^[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 $τ$ , $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}\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 $τ$ . 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 $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

α

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^[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.

Related Research Articles

In mathematics, an associative algebraA is an algebraic structure with compatible operations of addition, multiplication, and a scalar multiplication by elements in some field K. The addition and multiplication operations together give A the structure of a ring; the addition and scalar multiplication operations together give A the structure of a vector space over K. In this article we will also use the term K-algebra to mean an associative algebra over the field K. A standard first example of a K-algebra is a ring of square matrices over a field K, with the usual matrix multiplication.

In mathematics and computer science in general, a fixed point of a function is a value that is mapped to itself by the function.

In type theory, a typing rule is an inference rule that describes how a type system assigns a type to a syntactic construction. These rules may be applied by the type system to determine if a program is well-typed and what type expressions have. A prototypical example of the use of typing rules is in defining type inference in the simply typed lambda calculus, which is the internal language of Cartesian closed categories.

Variational Bayesian methods are a family of techniques for approximating intractable integrals arising in Bayesian inference and machine learning. They are typically used in complex statistical models consisting of observed variables as well as unknown parameters and latent variables, with various sorts of relationships among the three types of random variables, as might be described by a graphical model. As typical in Bayesian inference, the parameters and latent variables are grouped together as "unobserved variables". Variational Bayesian methods are primarily used for two purposes:

To provide an analytical approximation to the posterior probability of the unobserved variables, in order to do statistical inference over these variables.
To derive a lower bound for the marginal likelihood of the observed data. This is typically used for performing model selection, the general idea being that a higher marginal likelihood for a given model indicates a better fit of the data by that model and hence a greater probability that the model in question was the one that generated the data.

In differential geometry, a tensor density or relative tensor is a generalization of the tensor field concept. A tensor density transforms as a tensor field when passing from one coordinate system to another, except that it is additionally multiplied or weighted by a power W of the Jacobian determinant of the coordinate transition function or its absolute value. A tensor density with a single index is called a vector density. A distinction is made among (authentic) tensor densities, pseudotensor densities, even tensor densities and odd tensor densities. Sometimes tensor densities with a negative weight W are called tensor capacity. A tensor density can also be regarded as a section of the tensor product of a tensor bundle with a density bundle.

The simply typed lambda calculus, a form of type theory, is a typed interpretation of the lambda calculus with only one type constructor that builds function types. It is the canonical and simplest example of a typed lambda calculus. The simply typed lambda calculus was originally introduced by Alonzo Church in 1940 as an attempt to avoid paradoxical use of the untyped lambda calculus.

Lambda lifting is a meta-process that restructures a computer program so that functions are defined independently of each other in a global scope. An individual "lift" transforms a local function into a global function. It is a two step process, consisting of;

This is a glossary of properties and concepts in category theory in mathematics.

In mathematics, Church encoding is a means of representing data and operators in the lambda calculus. The Church numerals are a representation of the natural numbers using lambda notation. The method is named for Alonzo Church, who first encoded data in the lambda calculus this way.

In mathematics, the theta representation is a particular representation of the Heisenberg group of quantum mechanics. It gains its name from the fact that the Jacobi theta function is invariant under the action of a discrete subgroup of the Heisenberg group. The representation was popularized by David Mumford.

<span class="mw-page-title-main">Corner detection</span>

Corner detection is an approach used within computer vision systems to extract certain kinds of features and infer the contents of an image. Corner detection is frequently used in motion detection, image registration, video tracking, image mosaicing, panorama stitching, 3D reconstruction and object recognition. Corner detection overlaps with the topic of interest point detection.

The Newman–Penrose (NP) formalism is a set of notation developed by Ezra T. Newman and Roger Penrose for general relativity (GR). Their notation is an effort to treat general relativity in terms of spinor notation, which introduces complex forms of the usual variables used in GR. The NP formalism is itself a special case of the tetrad formalism, where the tensors of the theory are projected onto a complete vector basis at each point in spacetime. Usually this vector basis is chosen to reflect some symmetry of the spacetime, leading to simplified expressions for physical observables. In the case of the NP formalism, the vector basis chosen is a null tetrad: a set of four null vectors—two real, and a complex-conjugate pair. The two real members often asymptotically point radially inward and radially outward, and the formalism is well adapted to treatment of the propagation of radiation in curved spacetime. The Weyl scalars, derived from the Weyl tensor, are often used. In particular, it can be shown that one of these scalars— $in the appropriate frame—encodes the outgoing gravitational radiation of an asymptotically flat system.$

In probability and statistics, the Tweedie distributions are a family of probability distributions which include the purely continuous normal, gamma and inverse Gaussian distributions, the purely discrete scaled Poisson distribution, and the class of compound Poisson–gamma distributions which have positive mass at zero, but are otherwise continuous. Tweedie distributions are a special case of exponential dispersion models and are often used as distributions for generalized linear models.

In mathematics, a Lamé function, or ellipsoidal harmonic function, is a solution of Lamé's equation, a second-order ordinary differential equation. It was introduced in the paper. Lamé's equation appears in the method of separation of variables applied to the Laplace equation in elliptic coordinates. In some special cases solutions can be expressed in terms of polynomials called Lamé polynomials.

In mathematics, the modular lambda function λ(τ) is a highly symmetric Holomorphic function on the complex upper half-plane. It is invariant under the fractional linear action of the congruence group Γ(2), and generates the function field of the corresponding quotient, i.e., it is a Hauptmodul for the modular curve X(2). Over any point τ, its value can be described as a cross ratio of the branch points of a ramified double cover of the projective line by the elliptic curve $, where the map is defined as the quotient by the [-1] involution.$

A Hindley–Milner (HM) type system is a classical type system for the lambda calculus with parametric polymorphism. It is also known as Damas–Milner or Damas–Hindley–Milner. It was first described by J. Roger Hindley and later rediscovered by Robin Milner. Luis Damas contributed a close formal analysis and proof of the method in his PhD thesis.

Deductive lambda calculus considers what happens when lambda terms are regarded as mathematical expressions. One interpretation of the untyped lambda calculus is as a programming language where evaluation proceeds by performing reductions on an expression until it is in normal form. In this interpretation, if the expression never reduces to normal form then the program never terminates, and the value is undefined. Considered as a mathematical deductive system, each reduction would not alter the value of the expression. The expression would equal the reduction of the expression.

In mathematics, convenient vector spaces are locally convex vector spaces satisfying a very mild completeness condition.

In mathematics, a polyadic space is a topological space that is the image under a continuous function of a topological power of an Alexandroff one-point compactification of a discrete space.

In algebraic topology, given a fibration p:E→B, the change of fiber is a map between the fibers induced by paths in B.

References

1 2 3 4
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. Lecture Notes in Computer Science. Vol. 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.
- Adam (August 31, 2010). "What are κappa-categories?". MathOverflow.
↑ Barendregt, Hendrik Pieter, ed. (October 1, 1984). The Lambda Calculus: Its Syntax and Semantics. Studies in Logic and the Foundations of Mathematics. Vol. 103 (Revised ed.). Amsterdam, North Holland: Elsevier Science. ISBN 978-0-444-87508-2.
↑
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.
- Adam (August 31, 2010). "What are κappa-categories?". MathOverflow.
↑ 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. S2CID 3428512.
↑ Power, John; Thielecke, Hayo (1999). "Closed Freyd- and κ-categories". In Wiedermann, Jiří; van Emde Boas, Peter; Nielsen, Mogens (eds.). Automata, Languages and Programming. Lecture Notes in Computer Science. Vol. 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.

This page is based on this Wikipedia article
Text is available under the CC BY-SA 4.0 license; additional terms may apply.
Images, videos and audio are available under their respective licenses.

[Hasegawa-1] 1 2 3 4 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. Lecture Notes in Computer Science. Vol. 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.
Adam (August 31, 2010). "What are κappa-categories?". MathOverflow.

[mwARw] Adam (August 31, 2010). "What are κappa-categories?". MathOverflow.

[Barendregt-2] Barendregt, Hendrik Pieter, ed. (October 1, 1984). The Lambda Calculus: Its Syntax and Semantics. Studies in Logic and the Foundations of Mathematics. Vol. 103 (Revised ed.). Amsterdam, North Holland: Elsevier Science. ISBN 978-0-444-87508-2.

[Lambek-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.
Adam (August 31, 2010). "What are κappa-categories?". MathOverflow.

[mwATo] Adam (August 31, 2010). "What are κappa-categories?". MathOverflow.

[HermidaJacobs-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. S2CID 3428512.

[closed-5] Power, John; Thielecke, Hayo (1999). "Closed Freyd- and κ-categories". In Wiedermann, Jiří; van Emde Boas, Peter; Nielsen, Mogens (eds.). Automata, Languages and Programming. Lecture Notes in Computer Science. Vol. 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.

[1]

[2]

[3]

[4]

[5]