Kappa calculus

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

${\displaystyle \tau =1\mid \tau \times \tau \mid \ldots }$

${\displaystyle 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 ${\displaystyle \tau _{1}}$ and ${\displaystyle \tau _{2}}$ are types then ${\displaystyle \tau _{1}\times \tau _{2}}$ is a type.
• Every variable is an expression
• If τ is a type then ${\displaystyle id_{\tau }}$ is an expression
• If τ is a type then ${\displaystyle !_{\tau }}$ is an expression
• If τ is a type and e is an expression then ${\displaystyle \operatorname {lift} _{\tau }(e)}$ is an expression
• If ${\displaystyle e_{1}}$ and ${\displaystyle e_{2}}$ are expressions then ${\displaystyle e_{1}\circ e_{2}}$ is an expression
• If x is a variable, τ is a type, and e is an expression, then ${\displaystyle \kappa x{:}1{\to }\tau \;.\;e}$ is an expression

The ${\displaystyle :1{\to }\tau }$ and the subscripts of id, !, and ${\displaystyle \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 ${\displaystyle \operatorname {lift} }$ and composition:

${\displaystyle e_{1}e_{2}\ {\overset {\operatorname {def} }{=}}\ e_{1}\circ \operatorname {lift} (e_{2})}$

The presentation here uses sequents (${\displaystyle \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 ${\displaystyle e:\tau _{1}{\to }\tau _{2}}$ is used to indicate that expression e has source type ${\displaystyle {\tau _{1}}}$ and target type ${\displaystyle {\tau _{2}}}$.

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

${\displaystyle {x{:}1{\to }\tau \;\in \;\Gamma } \over {\Gamma \vdash x:1{\to }\tau }}$	(Var)
${\displaystyle {} \over {\vdash id_{\tau }\;:\;\tau \to \tau }}$	(Id)
${\displaystyle {} \over {\vdash !_{\tau }\;:\;\tau \to 1}}$	(Bang)
${\displaystyle {\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)
${\displaystyle {\Gamma \vdash e{:}1{\to }\tau _{1}} \over {\Gamma \vdash \operatorname {lift} _{\tau _{2}}(e)\;:\;\tau _{2}\to (\tau _{1}\times \tau _{2})}}$	(Lift)
${\displaystyle {\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 ${\displaystyle x:1{\to }\tau }$ lets you conclude that ${\displaystyle x:1{\to }\tau }$
• Id: for any type τ, ${\displaystyle id_{\tau }:\tau {\to }\tau }$
• Bang: for any type τ, ${\displaystyle !_{\tau }:\tau {\to }1}$
• Comp: if the target type of ${\displaystyle e_{1}}$ matches the source type of ${\displaystyle e_{2}}$ they may be composed to form an expression ${\displaystyle e_{2}\circ e_{1}}$ with the source type of ${\displaystyle e_{1}}$ and target type of ${\displaystyle e_{2}}$
• Lift: if ${\displaystyle e:1{\to }\tau _{1}}$, then ${\displaystyle \operatorname {lift} _{\tau _{2}}(e):\tau _{2}{\to }(\tau _{1}\times \tau _{2})}$
• Kappa: if we can conclude that ${\displaystyle e:\tau _{2}\to \tau _{3}}$ under the assumption that ${\displaystyle x:1{\to }\tau _{1}}$, then we may conclude without that assumption that ${\displaystyle \kappa x{:}1{\to }\tau _{1}\,.\,e\;:\;\tau _{1}\times \tau _{2}\to \tau _{3}}$

Kappa calculus obeys the following equalities:

• Neutrality: If ${\displaystyle f:\tau _{1}{\to }\tau _{2}}$ then ${\displaystyle f{\circ }id_{\tau _{1}}=f}$ and ${\displaystyle f=id_{\tau _{2}}{\circ }f}$
• Associativity: If ${\displaystyle f:\tau _{1}{\to }\tau _{2}}$, ${\displaystyle g:\tau _{2}{\to }\tau _{3}}$, and ${\displaystyle h:\tau _{3}{\to }\tau _{4}}$, then ${\displaystyle (h{\circ }g){\circ }f=h{\circ }(g{\circ }f)}$.
• Terminality: If ${\displaystyle f{:}\tau {\to }1}$ and ${\displaystyle g{:}\tau {\to }1}$ then ${\displaystyle f=g}$
• Lift-Reduction: ${\displaystyle (\kappa x.f)\circ \operatorname {lift} _{\tau }(c)=f[c/x]}$
• Kappa-Reduction: ${\displaystyle \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.