Kappa calculus

In mathematical logic, , 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. The definition below has been adapted from the diagrams on pages 205 and 207 of Hasegawa. 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: 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 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: {| cellpadding="9" style="text-align:center;" | || (Var) |- | || (Id) |- | || (Bang) |- | || (Comp) |- |