The Coq mailing list

[AUGER Cédric <sedrikov AT gmail.com>]

Le Wed, 26 Dec 2012 07:45:42 +0100,
Daniel de Rauglaudre 
<daniel.de_rauglaudre AT inria.fr>
 a écrit :

> Hi,
> 
> Thanks for your explanations about decidability. Very interesting,
> made me think a lot, I think a true definition of decidability in
> Coq should be very complicated, since it implies that we define the
> notion of algorithm, and tutti quanti. I think Bruno Barras' thesis
> (Coq in Coq) contains this.
> 

Well, for decidability, in Coq, we often stick with:
Definition decidable {T:Type} (P:T->Prop) : Prop :=
        exists f:(T->bool), forall t, P t <-> f t = true.

Or simply we say that P is decidable if there exists a function f of
type "forall t, {P t}+{~P t}". For instance some (probably a lot) of us
use functions of type "forall a b, {a=b}+{a<>b}". It is an example for
which we can say that "forall a, equality to a is decidable".

Of course, it is a little "impure", as it covers cases involving
oracles, and with classical logic + axiom of choice, I think any
language is decidable.

For the complicateness of this notion involving Turing Machines, I
quickly did the following (92 loc).

I think it covers exactly the definition of decidability.

====================================================================
CoInductive TuringDemiBand : Set :=
  | More : bool -> TuringDemiBand -> TuringDemiBand
.
CoFixpoint demi_bk : TuringDemiBand :=
  More false demi_bk
.
Fixpoint demi_init (l : list bool) : TuringDemiBand :=
  match l with
  | nil => demi_bk
  | cons b l => More b (demi_init l)
  end
.
Record TuringBand : Set := TB
  { past : TuringDemiBand
  ; current : bool
  ; future : TuringDemiBand
  }
.
Definition init (l : list bool) : TuringBand := TB demi_bk false
(demi_init l) .
Fixpoint BoundedSet (n : nat) : Set :=
  match n with
  | O => Empty_set
  | S n => option (BoundedSet n)
  end
.
Inductive State (n : nat) : Set :=
  | Final : bool -> State n
  | Working : BoundedSet n -> State n
.
Record Transition (n : nat) : Set := Trans
  { new_state : State n (* None is for final state *)
  ; go_past : bool
  ; replace_current : bool
  }
.
(* I restrict to deterministic Turing Machines, as it does change theory
   of complexity but does not affect decidability *)
Definition TransSys (n : nat) := BoundedSet n -> bool -> Transition n
.
Record TuringMachine : Set := TM
  { states_cardinality : nat
  ; transitions : TransSys states_cardinality
  ; initial_state : BoundedSet states_cardinality
  }
.
Record WStatus (n : nat) : Set := WSt
  { state : BoundedSet n
  ; band : TuringBand
  }
.
Inductive Status (n : nat) : Set :=
  | Running : WStatus n -> Status n
  | Terminal : bool -> Status n
.
Definition app_trans (n : nat) (t : TransSys n) (s : WStatus n) :
Status n := let t := t (state n s) (current (band n s)) in
  match new_state n t with
  | Final b => Terminal n b
  | Working ns =>
    let b := if go_past n t
             then let (b, db) := past (band n s) in
                  TB db b (More (replace_current n t) (future (band n
s))) else let (b, db) := future (band n s) in
                  TB (More (replace_current n t) (past (band n s))) b db
    in Running n {| state := ns ; band := b |}
  end
.
Inductive EndsWith
 (*true parameters*) (n : nat) (t : TransSys n) (r : bool)
 (*false parameter*) (b : WStatus n) : Prop :=
 | Halt : app_trans n t b = Terminal n r -> EndsWith n t r b
 | Continue : forall ws, app_trans n t b = Running n ws ->
              EndsWith n t r ws -> EndsWith n t r b
.
(*****************************)
Record Encoding (T : Type) := Enc
  { encode : T -> list bool
  ; decode : list bool -> T
  ; code_spe : forall (t : T), decode (encode t) = t
  }
.
Definition Language (T : Type) := T -> Prop
.
Record Decidable (T : Type) (L : Language T) : Prop :=
  { decider : TuringMachine
  ; coder : Encoding T
  ; decision : forall t, (L t) <->
               EndsWith (states_cardinality decider) (transitions
decider) true (WSt _ (initial_state decider) (init (encode T coder t)))
  }
.