Call-with-current-continuation - Relation To Non-constructive Logic

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 see, I am alive, I am alive
    I stand in good relation to the earth
    I stand in good relation to the gods
    I stand in good relation to all that is beautiful
    I stand in good relation to the daughter of Tsen-tainte
    You see, I am alive, I am alive”
    —N. Scott Momaday (b. 1934)

    “The psychoanalysis of individual human beings, however, teaches us with quite special insistence that the god of each of them is formed in the likeness of his father, that his personal relation to God depends on his relation to his father in the flesh and oscillates and changes along with that relation, and that at bottom God is nothing other than an exalted father.”
    —Sigmund Freud (1856–1939)

    “There is no morality by instinct.... There is no social salvation—in the end—without taking thought; without mastery of logic and application of logic to human experience.”
    —Katharine Fullerton Gerould (1879–1944)