added reduction from MMA_HALTING to HaltLclosed without the L framewo…

…rk / MetaCoq

added MMA_computable to L_computable_closed without the L framework / MetaCoq
added MM_computable_to_MMA_computable
made HaltLclosed more prominent in reduction chains
generalized deterministic simulation to uniformly confluent simulation

theories/CounterMachines/Reductions/MM2_HALTING_to_CM1_HALT.v

@@ -16,7 +16,7 @@ Import ListNotations.
 
 Require Import Undecidability.MinskyMachines.MM2.
 Require Undecidability.CounterMachines.CM1.
-Require Undecidability.Shared.deterministic_simulation.
+Require Undecidability.Shared.simulation.
 Require Import Undecidability.CounterMachines.Util.CM1_facts.
 Require Import Undecidability.MinskyMachines.Util.MM2_facts.
 
@@ -359,7 +359,7 @@ Section MM2_CM1.
 
   Lemma MM2_HALTING_iff_terminates {a b} :
     MM2_HALTING (P, a, b) <->
-      deterministic_simulation.terminates (mm2_step P) (1, (a, b)).
+      simulation.terminates (mm2_step P) (1, (a, b)).
   Proof. done. Qed.
 
   Notation cm1_step := (fun x y => CM1.step M x = y /\ x <> y).
@@ -375,18 +375,18 @@ Section MM2_CM1.
     - by apply: rt_step.
   Qed.
 
-  Lemma cm1_halting_stuck x : CM1.halting M x -> deterministic_simulation.stuck cm1_step x.
+  Lemma cm1_halting_stuck x : CM1.halting M x -> simulation.stuck cm1_step x.
   Proof.
     rewrite /CM1.halting. move=> Hx y [Hxy H'xy]. congruence.
   Qed. 
 
   Lemma CM1_halting_iff_terminates {x} :
     (exists n, CM1.halting M (Nat.iter n (CM1.step M) x)) <->
-    deterministic_simulation.terminates cm1_step x.
+    simulation.terminates cm1_step x.
   Proof.
     split.
     - move=> [n].
-      have /(@deterministic_simulation.terminates_extend CM1.Config) := cm1_steps n x.
+      have /(@simulation.terminates_extend CM1.Config) := cm1_steps n x.
       move: (Nat.iter n (CM1.step M) x) => y H Hy. apply: H.
       exists y. by split; [apply: rt_refl|apply: cm1_halting_stuck].
     - move=> [y] [].
@@ -443,13 +443,13 @@ Section MM2_CM1.
     rewrite /CM1.CM1_HALT.
     apply /(terminating_reaches_iff init_M).
     apply /CM1_halting_iff_terminates.
-    move: H. apply: deterministic_simulation.terminates_transport.
+    move: H. apply: simulation.terminates_transport.
     - exact: P_to_M_step.
-    - rewrite /deterministic_simulation.stuck.
+    - rewrite /simulation.stuck.
       move=> x x' Hx Hxx'.
-      rewrite /deterministic_simulation.terminates.
+      rewrite /simulation.terminates.
       exists x'. split; [by apply: rt_refl|].
-      rewrite /deterministic_simulation.stuck.
+      rewrite /simulation.stuck.
       move=> y' [Hx'y' H'x'y'].
       move: Hx => /mm2_stop_index_iff.
       subst y'.
@@ -470,8 +470,8 @@ Section MM2_CM1.
   Proof.
     move=> /(terminating_reaches_iff init_M) /CM1_halting_iff_terminates H.
     apply /MM2_HALTING_iff_terminates.
-    move: H. apply: deterministic_simulation.terminates_reflection.
-    - by move=> > [<- _] [<- _].
+    move: H. apply: simulation.terminates_reflection.
+    - move=> > [<- _] [<- _]. by left.
     - exact: P_to_M_step.
     - by apply: mm2_exists_step_dec.
     - by split; [|exists 0].

theories/L/L.v

@@ -29,6 +29,11 @@ Inductive eval : term -> term -> Prop :=
 (* The L-halting problem  *)
 Definition HaltL (s : term) := exists t, eval s t.
 
+Definition closed s := forall n u, subst s n u = s.
+
+(* Halting problem for weak call-by-value lambda-calculus *)
+Definition HaltLclosed (s : {s : term | closed s}) := exists t, eval (proj1_sig s) t.
+
 (* Scott encoding of natural numbers  *)
 Fixpoint nat_enc (n : nat) := 
   match n with
@@ -45,8 +50,6 @@ Definition L_computable {k} (R : Vector.t nat k -> nat -> Prop) :=
       (forall m, R v m <-> L.eval (Vector.fold_left (fun s n => L.app s (nat_enc n)) s v) (nat_enc m)) /\
       (forall o, L.eval (Vector.fold_left (fun s n => L.app s (nat_enc n)) s v) o -> exists m, o = nat_enc m).
 
-Definition closed s := forall n u, subst s n u = s.
-
 Definition L_computable_closed {k} (R : Vector.t nat k -> nat -> Prop) := 
   exists s, closed s /\ forall v : Vector.t nat k, 
       (forall m, R v m <-> L.eval (Vector.fold_left (fun s n => L.app s (nat_enc n)) s v) (nat_enc m)) /\

theories/L/L_undec.v

@@ -1,18 +1,22 @@
 Require Import Undecidability.L.L.
 Require Import Undecidability.Synthetic.Undecidability.
-From Undecidability.Synthetic Require Import
-  DecidabilityFacts EnumerabilityFacts.
-Require Import Undecidability.L.Enumerators.term_enum.
+From Undecidability.Synthetic Require Import DecidabilityFacts.
 
-Require Import Undecidability.TM.TM.
-Require Import Undecidability.TM.TM_undec.
-Require Import Undecidability.L.Reductions.TM_to_L.
+Require Import Undecidability.MinskyMachines.MMA2_undec.
+Require Undecidability.L.Reductions.MMA_HALTING_to_HaltLclosed.
 
-(** ** HaltL is undecidable *)
+(* The Halting problem for weak call-by-value lambda-calculus is undecidable *)
+Lemma HaltLclosed_undec :
+  undecidable (HaltLclosed).
+Proof.
+  apply (undecidability_from_reducibility MMA2_HALTING_undec).
+  eapply MMA_HALTING_to_HaltLclosed.reduction.
+Qed.
 
+(** ** HaltL is undecidable *)
 Lemma HaltL_undec :
   undecidable (HaltL).
 Proof.
-  apply (undecidability_from_reducibility HaltMTM_undec).
-  eapply HaltMTM_to_HaltL.
+  apply (undecidability_from_reducibility HaltLclosed_undec).
+  now exists (fun '(exist _ M _) => M).
 Qed.

theories/L/Prelim/ARS.v

@@ -20,7 +20,7 @@ Definition rcomp X Y Z (R : X -> Y -> Prop) (S : Y -> Z -> Prop)
 
 (* Power predicates *)
 
-Require Import Arith.
+Require Import Arith Relations.
 Definition pow X R n : X -> X -> Prop := it (rcomp R) n eq.
 
 Definition functional {X Y} (R: X -> Y -> Prop) := forall x y1 y2, R x y1 -> R x y2 -> y1 = y2.
@@ -90,6 +90,13 @@ Section FixX.
     intros A. erewrite star_pow. eauto.
   Qed.
 
+  Lemma star_clos_rt_iff R x y : star R x y <-> clos_refl_trans _ R x y.
+  Proof.
+    split.
+    - intros H; induction H; eauto using clos_refl_trans.
+    - intros H%clos_rt_rt1n_iff. induction H; eauto using star.
+  Qed.
+
   (* Equivalence closure *)
 
   Inductive ecl R : X -> X -> Prop :=

theories/L/Reductions/HaltMuRec_to_HaltL.v

@@ -415,7 +415,7 @@ Require Import Undecidability.L.Reductions.MuRec.MuRec_extract.
 Definition evalfun fuel c v := match eval fuel 0 c v with Some (inl x) => Some x | _ => None end.
 
 From Undecidability Require Import MuRec_computable LVector.
-From Undecidability.L.Util Require Import NaryApp ClosedLAdmissible.
+From Undecidability.L.Util Require Import NaryApp.
 
 Import L_Notations.
 
@@ -444,6 +444,12 @@ Proof.
   induction v; cbn; intros ? Hi. 1: inversion Hi. inv Hi. 1:Lproc. eapply IHv. eapply Eqdep_dec.inj_pair2_eq_dec in H2. 1:subst; eauto. eapply nat_eq_dec.
 Qed.
 
+Lemma equiv_R (s t t' : term):
+  t == t' -> s t == s t'.
+Proof.
+  now intros ->.
+Qed.
+
 Lemma cont_vec_correct k s (v : Vector.t nat k) :
   proc s ->
   many_app (cont_vec k s) (Vector.map enc v) == s (enc v).
@@ -557,20 +563,27 @@ Proof.
   now eapply erase_correct in H.
 Qed.
 
+Lemma many_app_eq_nat {k} (v : Vector.t nat k) s :  many_app s (Vector.map enc v) = Vector.fold_left (fun (s : term) n => s (nat_enc n)) s v.
+Proof.
+   induction v in s |- *.
+   * cbn. reflexivity.
+   * cbn. now rewrite IHv.
+Qed.
+
 Theorem computable_MuRec_to_L {k} (R : Vector.t nat k -> nat -> Prop) :
   MuRec_computable R -> L_computable R.
 Proof.
   intros [f Hf].
   exists (cont_vec k (lam (mu_option (lam (ext evalfun 0 (enc (erase f)) 1))))).
   intros v. rewrite <- many_app_eq_nat. split.
   - intros m. rewrite L_facts.eval_iff.
-    assert (lambda (encNatL m)) as [b Hb]. { change  (lambda (enc m)). Lproc. }
+    assert (lambda (nat_enc m)) as [b Hb]. { change  (lambda (enc m)). Lproc. }
     rewrite Hb. rewrite eproc_equiv. rewrite cont_vec_correct. 2: unfold mu_option; Lproc.
     assert (lam (mu_option (lam (ext evalfun 0 (enc (erase f)) 1))) (enc v) ==
           mu_option (lam (ext evalfun 0 (enc (erase f)) (enc v)))).
     {  unfold mu_option. now Lsimpl. }
     rewrite H. rewrite <- Hb.
-    change (encNatL m) with (enc m).
+    change (nat_enc m) with (enc m).
     rewrite mu_option_spec. 2:Lproc.
     2:{ intros []; cbv; congruence. }
     2:{ intros. eexists. rewrite !enc_vector_eq. Lsimpl. reflexivity. }