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:
“We must get back into relation, vivid and nourishing relation to the cosmos and the universe. The way is through daily ritual, and is an affair of the individual and the household, a ritual of dawn and noon and sunset, the ritual of the kindling fire and pouring water, the ritual of the first breath, and the last.”
—D.H. (David Herbert)
“The foregoing generations beheld God and nature face to face; we, through their eyes. Why should not we also enjoy an original relation to the universe? Why should not we have a poetry and philosophy of insight and not of tradition, and a religion by revelation to us, and not the history of theirs?”
—Ralph Waldo Emerson (1803–1882)
“We want in every man a long logic; we cannot pardon the absence of it, but it must not be spoken. Logic is the procession or proportionate unfolding of the intuition; but its virtue is as silent method; the moment it would appear as propositions and have a separate value, it is worthless.”
—Ralph Waldo Emerson (1803–1882)