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:
“A theory of the middle class: that it is not to be determined by its financial situation but rather by its relation to government. That is, one could shade down from an actual ruling or governing class to a class hopelessly out of relation to government, thinking of gov’t as beyond its control, of itself as wholly controlled by gov’t. Somewhere in between and in gradations is the group that has the sense that gov’t exists for it, and shapes its consciousness accordingly.”
—Lionel Trilling (1905–1975)
“You must realize that I was suffering from love and I knew him as intimately as I knew my own image in a mirror. In other words, I knew him only in relation to myself.”
—Angela Carter (1940–1992)
“Logic is not a body of doctrine, but a mirror-image of the world. Logic is transcendental.”
—Ludwig Wittgenstein (1889–1951)