Com'è possibile implementare call/cc, ma la logica classica (intuizionistica + chiamata/cc) non è costruttiva?

Question

La logica intuizionista, essendo costruttiva, è la base per i sistemi di tipi nella programmazione funzionale. La logica classica non è costruttiva, in particolare la legge del centro escluso A ∨ ¬ A (o suoi equivalenti, come double negation elimination o Pierce's law).

Possiamo comunque attuare (costrutto) il call-with-current-continuation operatore (AKA chiamata/cc), per esempio come nel Scheme. Quindi, perché non è call/cc costruttivo?

Answer 1

Il problema è che con chiamata/cc il risultato dipende dall'ordine di valutazione. Considera il seguente esempio in Haskell. Supponendo abbiamo la chiamata/cc operatore

callcc :: ((a -> b) -> a) -> a 
callcc = undefined 

definiamo

example :: Int 
example = 
    callcc (\s -> 
     callcc (\t -> 
      s 3 + t 4 
     ) 
    ) 

Entrambe le funzioni sono puri, così il valore di example dovrebbero essere univocamente determinata. Tuttavia, dipende dall'ordine di valutazione. Se viene valutato prima s 3, il risultato è 3; se viene valutato prima t 4, il risultato è 4.

Ciò corrisponde a due esempi distinti monade di continuazione (che impone ordine):

-- the result is 3 
example1 :: (MonadCont m) => m Int 
example1 = 
    callCC (\s -> 
     callCC (\t -> do 
      x <- s 3 
      y <- t 4 
      return (x + y) 
     ) 
    ) 

-- the result is 4 
example2 :: (MonadCont m) => m Int 
example2 = 
    callCC (\s -> 
     callCC (\t -> do 
      y <- t 4 -- switched order 
      x <- s 3 
      return (x + y) 
     ) 
    ) 

Persino dipende se un termine viene valutata affatto o meno:

example' :: Int 
example' = callcc (\s -> const 1 (s 2)) 

Se s 2 viene valutato, il risultato è 2, altrimenti 1.

Ciò significa che il Church-Rosser theorem non detiene in presenza di chiamata/cc. In particolare, i termini non hanno più normal forms.

Forse una possibilità sarebbe di visualizzare chiamata/cc come operatore non deterministica (non costruttivo) che combina tutti i possibili risultati ottenuti da (non) valutare diverse sotto-termini vario ordine. Il risultato di un programma sarebbe quindi l'insieme di tutte le possibili forme normali. Tuttavia, l'implementazione standard call/cc selezionerà sempre solo uno di essi (in base al suo particolare ordine di valutazione).