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:
“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)
“In relation to God, we are like a thief who has burgled the house of a kindly householder and been allowed to keep some of the gold. From the point of view of the lawful owner this gold is a gift; From the point of view of the burglar it is a theft. He must go and give it back. It is the same with our existence. We have stolen a little of God’s being to make it ours. God has made us a gift of it. But we have stolen it. We must return it.”
—Simone Weil (1909–1943)
“Neither Aristotelian nor Russellian rules give the exact logic of any expression of ordinary language; for ordinary language has no exact logic.”
—Sir Peter Frederick Strawson (b. 1919)