Perché i collegamenti logici e i booleani sono separati in Coq?

Question

Vengo da una programmazione sfondo JavaScript/Ruby e sono abituato a questo essere come vero/falso opere (in JS):

!true 
// false 
!false 
// true 

quindi è possibile utilizzare quei veri falsi valori/con && come

var a = true, b = false; 
a && !b; 

Quindi e e non (e altri operatori logici/booleani) fanno parte di un unico sistema; sembra che il sistema "logico" e il sistema "booleano" siano la stessa cosa.

Tuttavia, in Coq, le logiche e i booleani sono due cose separate. Perchè è questo? La citazione/link sottostante dimostra come è necessario un teorema per metterli in relazione.

Abbiamo già visto diversi luoghi in cui strutture analoghe possono essere trovate nei mondi computazionale (Tipo) e logico (Prop) di Coq. Eccone un'altra: gli operatori booleani andb e orb sono chiaramente analoghi ai connettivi logici ∧ e ∨. Questa analogia può essere resa più precisa dai seguenti teoremi, che mostrano come tradurre la conoscenza dei comportamenti di andb e orb su determinati input in fatti proposizionali su quegli input.

Theorem andb_prop : ∀b c, 
    andb b c = true → b = true ∧ c = true. 

http://www.seas.upenn.edu/~cis500/current/sf/Logic.html#lab211

Answer 1

Essenzialmente, Coq ha sia perché sono utili per cose diverse: booleani corrispondono a fatti verificabili meccanicamente (ad esempio, con un algoritmo), considerando che le proposizioni possono esprimere più concetti.

In senso stretto, i mondi logici e booleani non sono separati in Coq: il mondo booleano è un sottoinsieme del mondo logico. In altre parole, ogni affermazione che puoi esprimere come un calcolo booleano può essere vista come una proposizione logica (ad esempio, qualcosa di tipo Prop): se b : bool rappresenta una dichiarazione, possiamo affermare che questa affermazione è vera dicendo b = true, che è di tipo Prop.

Il motivo c'è di più in Coq alla logica di un semplice booleani è che l'inverso della dichiarazione precedente non regge: non tutti i fatti logici possono essere visti come i calcoli booleani. In altri termini, non è il caso che i booleani nei normali linguaggi di programmazione come Ruby e JavaScript sommano sia bool e Prop in Coq, perché i valori Prop possono esprimere cose che i valori booleani in queste lingue non possono.

Per illustrare questo, si consideri il seguente Coq predicato:

Definition commutative {T} (op : T -> T -> T) : Prop := 
    forall x y, op x y = op y x. 

Come suggerisce il nome, questo predicato afferma che un operatore op è commutativa. Molti operatori nei linguaggi di programmazione sono commutativi: ad esempio, moltiplicano e aggiungono gli interi. Infatti, in Coq possiamo provare le seguenti affermazioni (e credo che questi sono esempi nel libro Software Foundation):

Lemma plus_comm : commutative plus. Proof. (* ... *) Qed. 
Lemma mult_comm : commutative mult. Proof. (* ... *) Qed. 

Ora, provate a pensare come si potrebbe tradurre un predicato come commutative in un linguaggio più convenzionale.Se questo sembra difficile, non è un caso: è possibile dimostrare che non possiamo scrivere un programma che restituisca un booleano in queste lingue per verificare se un'operazione è commutativa o meno. Si può certamente scrivere unit test per verificare se questo fatto è vero per particolari input, ad esempio:

2 + 3 == 3 + 2 
4 * 5 == 5 * 4 

Tuttavia, se il vostro operatore lavora con un numero infinito di ingressi, questi test di unità in grado di coprire solo una frazione di tutti i casi possibili Pertanto, il test è sempre necessariamente più debole di una prova formale completa.

Ci si potrebbe chiedere perché ci preoccupiamo di avere booleani in Coq se Prop s può esprimere tutto ciò che i booleani possono. Il motivo è che Coq è una logica costruttiva , che è ciò a cui allude Vinz nel suo commento. La conseguenza più noto di questo fatto è che in Coq non possiamo dimostrare il seguente principio intuitivo:

Definition excluded_middle := 
    forall P : Prop, P \/ ~ P. 

che sostanzialmente dice che ogni proposizione è vera o falsa. "Come potrebbe fallire questo?", Potresti chiedertelo. In parole povere, nelle logiche costruttive (e in particolare in Coq), ogni prova corrisponde a un algoritmo che possiamo eseguire. In particolare, quando si dimostra una dichiarazione del modulo A \/ B in una logica costruttiva, è possibile estrarre un algoritmo (sempre terminante) da quella prova che risponde se A o B contiene. Quindi, se fossimo in grado di dimostrare il principio di cui sopra, avremmo un algoritmo che, data una certa proposizione, ci dice se quella proposizione è valida o meno. La teoria della computabilità mostra, tuttavia, che ciò non è possibile in generale a causa della indecidibilità: se prendiamo P per indicare "programma p fermate sull'ingresso x", il centro escluso produrrebbe un decisore per lo halting problem, che non può esistere.

Ora, ciò che è interessante dei booleani in Coq è che per costruzione consentono l'uso del centro escluso, perché do corrispondono a un algoritmo che possiamo eseguire. Specificamente, si può dimostrare la seguente:

Lemma excluded_middle_bool : 
    forall b : bool, b = true \/ negb b = true. 
Proof. intros b; destruct b; simpl; auto. Qed. 

Così, in Coq è utile considerare booleani come un caso speciale di proposizioni perché consentono forme di ragionamento che altre proposizioni Non, cioè, analisi del caso.

Naturalmente, si può pensare che richiedere che ogni prova corrisponda ad un algoritmo sia sciocco, e in effetti la maggior parte delle logiche consente il principio del centro escluso. Esempi di dimostrativi che seguono questo approccio di default includono Isabelle/HOL e il sistema Mizar. In questi sistemi, non dobbiamo avere una distinzione tra booleani e proposizioni, e sono trattati come la stessa cosa. Isabelle, ad esempio, ha solo bool e non Prop. Coq consente inoltre di sfumare la distinzione tra booleani e proposizioni, assumendo assiomi che consentono di eseguire analisi del caso su proposizioni generali. D'altra parte, in tale impostazione, quando si scrive una funzione che restituisce un valore booleano, è possibile che non si ottenga qualcosa che è possibile eseguire come algoritmo, mentre questo è sempre il caso per impostazione predefinita in Coq.