Skip to content

Abstracts.2018.ClassicalProofsAsPrograms

Jump to bottom
Fabian edited this page Feb 3, 2020 · 7 revisions

Classical proofs as programs

by Ayberk Tosun

Abstract

The insight that Felleisen et al's control operator C has the typing ¬¬A → A is due to Griffin [1]. The sense of this correspondence, however, was made precise through the work of Chetan Murthy who noticed that Harvey Friedman's method for transforming classical proofs of Π⁰₂ sentences to constructive ones is exactly what is needed to understand the typing of C. In my talk, I will give a self-contained introduction to the typing of C and its computational sense through Friedman's method. More specifically, I will follow the presentation of [2] that addresses three main questions:

  • How does Friedman's method work?
  • What is the computational reading of the extract obtained from the translated proof?
  • Why is this restricted to Π⁰₂ sentences?

References

  1. Griffin, Timothy G. "A formulae-as-type notion of control." Proceedings of the 17th ACM SIGPLAN-SIGACT symposium on Principles of programming languages. ACM, 1989.

  2. Murthy, Chetan R. "Classical proofs as programs: How, what and why." Constructivity in Computer Science. Springer, Berlin, Heidelberg, 1992. 71-88.

  3. Friedman, Harvey. "Classically and intuitionistically provably recursive functions." Proceedings of Higher Set Theory, Oberwolfach. Springer, Berlin, Heidelberg, 1978. 21-28.

Other Reading

There are also lecture notes on the same topic written by Robert Constable.

An Example in Agda (cf. Constable's lecture notes, pp. 25-27)

module TopLevel where

open import Relation.Binary.PropositionalEquality as Eq

open        Eq               using (_≡_; refl)
open import Data.Sum         using (_⊎_; inj₁; inj₂)
open import Relation.Nullary using (¬_)
open import Data.Nat         using (ℕ; _<_; _≤_)
open import Data.Product     using (∃-syntax; _,_; proj₁)

module Top {A} (ψ : A → Set) where

   -- φ := ∃[ x ](ψ x)
  ¬φ_ : Set → Set
  ¬φ ϑ = ϑ → ∃[ x ](ψ x)

  top : ¬φ ∃[ x ](¬φ ¬φ (ψ x))
  top (n , imp) = imp (λ x → n , x)

module Example where

  open Top (λ x → 0 < x)

  -- A := ⊥ checks out.
  thm₀ : ¬ ¬ ∃[ x ](¬ ¬ (0 < x))
  thm₀ = λ ne → ne (0 , λ nz → ne (1 , λ x → x (_≤_.s≤s _≤_.z≤n)))

  -- But thm₀ works for ⊥ replaced with _any_ A.
  -- Notice that the proof term is unchanged.
  thm₁ : ∀ (A : Set) → ((∃[ x ](((0 < x) → A) → A)) → A) → A
  thm₁ _ = λ ne → ne (0 , λ nz → ne (1 , λ x → x (_≤_.s≤s _≤_.z≤n)))

  -- We reconstruct the constructive proof from the translation as follows.
  thm : ∃[ x ](0 < x)
  thm = thm₁ (∃[ x ](0 < x)) top

  _ : proj₁ thm ≡ 1
  _ = refl
Clone this wiki locally