Concept

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) |- |

(Lift)
(Kappa)
}
In other words,
Var: assuming lets you conclude that
Id: for any type τ,
Bang: for any type τ,
Comp: if the target type of matches the source type of they may be composed to form an expression with the source type of and target type of
Lift: if , then
Kappa: if we can conclude that under the assumption that , then we may conclude without that assumption that
Kappa calculus obeys the following equalities:
Neutrality: If then and
Associativity: If , , and , then .
À propos de ce résultat
Cette page est générée automatiquement et peut contenir des informations qui ne sont pas correctes, complètes, à jour ou pertinentes par rapport à votre recherche. Il en va de même pour toutes les autres pages de ce site. Veillez à vérifier les informations auprès des sources officielles de l'EPFL.

Graph Chatbot

Chattez avec Graph Search

Posez n’importe quelle question sur les cours, conférences, exercices, recherches, actualités, etc. de l’EPFL ou essayez les exemples de questions ci-dessous.

AVERTISSEMENT : Le chatbot Graph n'est pas programmé pour fournir des réponses explicites ou catégoriques à vos questions. Il transforme plutôt vos questions en demandes API qui sont distribuées aux différents services informatiques officiellement administrés par l'EPFL. Son but est uniquement de collecter et de recommander des références pertinentes à des contenus que vous pouvez explorer pour vous aider à répondre à vos questions.