![[personal profile]](https://www.dreamwidth.org/img/silk/identity/user.png){kind=small}
xacidhttps://hal.inria.fr/hal-00996742v1/document
Negation is not involutive in the 𝜆𝒞 calculus because it does not distinguish captured stacks from continuations. We show that there is a formulae-as-types correspondence between the involutive negation in proof theory, and a notion of high-level access to the stacks studied by Felleisen and Clements.
We introduce polarised, untyped, calculi compatible with exten- sionality, for both of classical sequent calculus and classical natural deduction, with connectives for an involutive negation. The invol- ution is due to the l delimited control operator that we introduce, which allows us to implement the idea that captured stacks, unlike continuations, can be inspected. Delimiting control also gives a con- structive interpretation to falsity. We describe the isomorphism there is between 𝐴 and ¬¬𝐴, and thus between ¬∀ and ∃¬.
One way to provide constructive contents to classical proofs is by considering variants of the Gödel-Gentzen double-negation translations, such as Friedman’s [13]. We can translate classical proofs of ⊢ 𝑃 into intuitionistic proofs of ⊢ (𝑃′ → 𝑅) → 𝑅, where 𝑃′ is the translation of 𝑃 and where 𝑅 is chosen arbitrarily. When 𝑃 is purely positive, then 𝑃 ′ does not depend on 𝑅 and, furthermore, we have 𝑃′ = 𝑃. Therefore, in this special case we can take 𝑅 = 𝑃 and deduce an intuitionistic proof of ⊢ (𝑃 → 𝑃 ) → 𝑃 and, in turn, one of ⊢ 𝑃 . In the other cases, the translation describes in fact how the behaviour of classical proofs depends on the context in which classical axioms are invoked. Thus the interpretation does not contradict intuitionism: the latter assumes that the behaviour of proofs is referentially transparent, while here we do not make such an assump- tion. This is why proofs of ∀𝐴, 𝐴 ∨ ¬𝐴 do not provide a decision procedure for 𝐴 in general.
As we will see, the computational contents of the De Morgan law is as simple to understand as: 1) capturing the stack of the form 𝑛⋅𝜋 that appears during the head reduction of the argument; 2) decomposing it into head and tail, and return a pair (𝑛, 𝗄𝜋 ) where 𝗄𝜋 is the captured form of the tail. This contrasts with the proof in the 𝜆𝒞 cal- culus, which is convoluted because captured contexts are identified with continuations. By continuation we mean the functional abstrac- tion of the remainder of a computation. Thus, the contents of the captured context, which is represented by a functional value, cannot be accessed in an immediate way.
Negation is not involutive in the 𝜆𝒞 calculus because it does not distinguish captured stacks from continuations. We show that there is a formulae-as-types correspondence between the involutive negation in proof theory, and a notion of high-level access to the stacks studied by Felleisen and Clements.
We introduce polarised, untyped, calculi compatible with exten- sionality, for both of classical sequent calculus and classical natural deduction, with connectives for an involutive negation. The invol- ution is due to the l delimited control operator that we introduce, which allows us to implement the idea that captured stacks, unlike continuations, can be inspected. Delimiting control also gives a con- structive interpretation to falsity. We describe the isomorphism there is between 𝐴 and ¬¬𝐴, and thus between ¬∀ and ∃¬.
One way to provide constructive contents to classical proofs is by considering variants of the Gödel-Gentzen double-negation translations, such as Friedman’s [13]. We can translate classical proofs of ⊢ 𝑃 into intuitionistic proofs of ⊢ (𝑃′ → 𝑅) → 𝑅, where 𝑃′ is the translation of 𝑃 and where 𝑅 is chosen arbitrarily. When 𝑃 is purely positive, then 𝑃 ′ does not depend on 𝑅 and, furthermore, we have 𝑃′ = 𝑃. Therefore, in this special case we can take 𝑅 = 𝑃 and deduce an intuitionistic proof of ⊢ (𝑃 → 𝑃 ) → 𝑃 and, in turn, one of ⊢ 𝑃 . In the other cases, the translation describes in fact how the behaviour of classical proofs depends on the context in which classical axioms are invoked. Thus the interpretation does not contradict intuitionism: the latter assumes that the behaviour of proofs is referentially transparent, while here we do not make such an assump- tion. This is why proofs of ∀𝐴, 𝐴 ∨ ¬𝐴 do not provide a decision procedure for 𝐴 in general.
As we will see, the computational contents of the De Morgan law is as simple to understand as: 1) capturing the stack of the form 𝑛⋅𝜋 that appears during the head reduction of the argument; 2) decomposing it into head and tail, and return a pair (𝑛, 𝗄𝜋 ) where 𝗄𝜋 is the captured form of the tail. This contrasts with the proof in the 𝜆𝒞 cal- culus, which is convoluted because captured contexts are identified with continuations. By continuation we mean the functional abstrac- tion of the remainder of a computation. Thus, the contents of the captured context, which is represented by a functional value, cannot be accessed in an immediate way.
