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 adolescent does not develop her identity and individuality by moving outside her family. She is not triggered by some magic unconscious dynamic whereby she rejects her family in favour of her peers or of a larger society.... She continues to develop in relation to her parents. Her mother continues to have more influence over her than either her father or her friends.”
—Terri Apter (20th century)
“Art should exhilarate, and throw down the walls of circumstance on every side, awakening in the beholder the same sense of universal relation and power which the work evinced in the artist, and its highest effect is to make new artists.”
—Ralph Waldo Emerson (1803–1882)
“The logic of worldly success rests on a fallacy: the strange error that our perfection depends on the thoughts and opinions and applause of other men! A weird life it is, indeed, to be living always in somebody else’s imagination, as if that were the only place in which one could at last become real!”
—Thomas Merton (1915–1968)