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:
τ = 1 ∣ τ × τ ∣ … {\displaystyle \tau =1\mid \tau \times \tau \mid \ldots }
e = x ∣ i d τ ∣ ! τ ∣ lift τ ( e ) ∣ e ∘ e ∣ κ x : 1 → τ . e {\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 τ 1 {\displaystyle \tau _{1}} and τ 2 {\displaystyle \tau _{2}} are types then τ 1 × τ 2 {\displaystyle \tau _{1}\times \tau _{2}} is a type. Every variable is an expression If τ is a type then i d τ {\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 lift τ ( e ) {\displaystyle \operatorname {lift} _{\tau }(e)} is an expression If e 1 {\displaystyle e_{1}} and e 2 {\displaystyle e_{2}} are expressions then e 1 ∘ e 2 {\displaystyle e_{1}\circ e_{2}} is an expression If x is a variable, τ is a type, and e is an expression, then κ x : 1 → τ . e {\displaystyle \kappa x{:}1{\to }\tau \;.\;e} is an expression The : 1 → τ {\displaystyle :1{\to }\tau } and the subscripts of id, !, and lift {\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
lift {\displaystyle \operatorname {lift} } and composition:
e 1 e 2 = def e 1 ∘ lift ( e 2 ) {\displaystyle e_{1}e_{2}\ {\overset {\operatorname {def} }{=}}\ e_{1}\circ \operatorname {lift} (e_{2})}
Typing rules The presentation here uses sequents ( Γ ⊢ e : τ {\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 In kappa calculus an expression has two types: the type of its source and the type of its target. The notation e : τ 1 → τ 2 {\displaystyle e:\tau _{1}{\to }\tau _{2}} is used to indicate that expression e has source type τ 1 {\displaystyle {\tau _{1}}} and target type τ 2 {\displaystyle {\tau _{2}}} . Expressions in kappa calculus are assigned types according to the following rules:
In other words,
Var: assuming x : 1 → τ {\displaystyle x:1{\to }\tau } lets you conclude that x : 1 → τ {\displaystyle x:1{\to }\tau }
Id: for any type τ, i d τ : τ → τ {\displaystyle id_{\tau }:\tau {\to }\tau }
Bang: for any type τ, ! τ : τ → 1 {\displaystyle !_{\tau }:\tau {\to }1}
… excerpt ends here. Continue reading the full article.
