Relation To Non-constructive Logic
The Curry-Howard correspondence between proofs and programs relates call/cc to Peirce's law, which extends intuitionistic logic to non-constructive, classical logic: ((α → β) → α) → α. Here, ((α → β) → α) is the type of the function f, which can either return a value of type α directly or apply an argument to the continuation of type (α → β). Since the existing context is deleted when the continuation is applied, the type β is never used and may be taken to be ⊥.
The principle of double negative elimination ((α → ⊥) → ⊥) → α is comparable to a variant of call-cc which expects its argument f to always evaluate the current continuation without normally returning a value.
Embeddings of classical logic into intuitionistic logic are related to continuation passing style translation.
Read more about this topic: Call-with-current-continuation
Famous quotes containing the words relation to, relation and/or logic:
“The proper study of mankind is man in his relation to his deity.”
—D.H. (David Herbert)
“There is a certain standard of grace and beauty which consists in a certain relation between our nature, such as it is, weak or strong, and the thing which pleases us. Whatever is formed according to this standard pleases us, be it house, song, discourse, verse, prose, woman, birds, rivers, trees, room, dress, and so on. Whatever is not made according to this standard displeases those who have good taste.”
—Blaise Pascal (1623–1662)
“...some sort of false logic has crept into our schools, for the people whom I have seen doing housework or cooking know nothing of botany or chemistry, and the people who know botany and chemistry do not cook or sweep. The conclusion seems to be, if one knows chemistry she must not cook or do housework.”
—Ellen Henrietta Swallow Richards (1842–1911)