From e20bc04a731dbdac4822f8ba63cd25da3f6ec133 Mon Sep 17 00:00:00 2001 From: Andrej Dudenhefner Date: Tue, 1 Oct 2024 13:50:47 +0200 Subject: [PATCH] added reduction from MMA_HALTING to HaltLclosed without the L framework / 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 --- .../Reductions/MM2_HALTING_to_CM1_HALT.v | 22 +- theories/L/L.v | 7 +- theories/L/L_undec.v | 22 +- theories/L/Prelim/ARS.v | 9 +- theories/L/Reductions/HaltL_to_HaltLclosed.v | 18 - theories/L/Reductions/HaltMuRec_to_HaltL.v | 19 +- .../L/Reductions/MMA_HALTING_to_HaltLclosed.v | 748 ++++++++++++++++++ .../MMA_computable_to_L_computable_closed.v | 251 ++++++ theories/L/Util/NaryApp.v | 8 +- theories/L/Util/term_facts.v | 221 ++++++ theories/LambdaCalculus/Krivine_undec.v | 4 +- theories/LambdaCalculus/Lambda_undec.v | 4 +- .../Reductions/HaltLclosed_to_wCBNclosed.v | 10 +- .../KrivineMclosed_HALT_to_SNclosed.v | 9 +- .../L_computable_to_MMA_computable.v | 28 - .../MM2_HALTING_to_MM2_ZERO_HALTING.v | 6 +- .../MMA_computable_to_MMA_mon_computable.v | 59 +- .../MM_computable_to_MMA_computable.v | 190 +++++ theories/MinskyMachines/Util/MMA_facts.v | 75 ++ theories/MinskyMachines/Util/MM_computable.v | 34 +- ...eterministic_simulation.v => simulation.v} | 40 +- theories/Synthetic/Models_Equivalent.v | 20 +- ...o_HaltTM_5.v => HaltLclosed_to_HaltTM_5.v} | 4 +- .../L_computable_to_TM_computable.v | 15 - .../MMA_mon_computable_to_TM_computable.v | 14 +- theories/_CoqProject | 41 +- 26 files changed, 1655 insertions(+), 223 deletions(-) delete mode 100644 theories/L/Reductions/HaltL_to_HaltLclosed.v create mode 100644 theories/L/Reductions/MMA_HALTING_to_HaltLclosed.v create mode 100644 theories/L/Reductions/MMA_computable_to_L_computable_closed.v create mode 100644 theories/L/Util/term_facts.v delete mode 100644 theories/MinskyMachines/Reductions/L_computable_to_MMA_computable.v create mode 100644 theories/MinskyMachines/Reductions/MM_computable_to_MMA_computable.v create mode 100644 theories/MinskyMachines/Util/MMA_facts.v rename theories/Shared/{deterministic_simulation.v => simulation.v} (75%) rename theories/TM/Reductions/{HaltL_to_HaltTM_5.v => HaltLclosed_to_HaltTM_5.v} (82%) delete mode 100644 theories/TM/Reductions/L_computable_to_TM_computable.v diff --git a/theories/CounterMachines/Reductions/MM2_HALTING_to_CM1_HALT.v b/theories/CounterMachines/Reductions/MM2_HALTING_to_CM1_HALT.v index 3e796e226..3a1221eae 100644 --- a/theories/CounterMachines/Reductions/MM2_HALTING_to_CM1_HALT.v +++ b/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]. diff --git a/theories/L/L.v b/theories/L/L.v index 368fb76a6..fc5549568 100644 --- a/theories/L/L.v +++ b/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)) /\ diff --git a/theories/L/L_undec.v b/theories/L/L_undec.v index 5933bf9de..110c77522 100644 --- a/theories/L/L_undec.v +++ b/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. diff --git a/theories/L/Prelim/ARS.v b/theories/L/Prelim/ARS.v index 3770c88b6..54797e765 100644 --- a/theories/L/Prelim/ARS.v +++ b/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 := diff --git a/theories/L/Reductions/HaltL_to_HaltLclosed.v b/theories/L/Reductions/HaltL_to_HaltLclosed.v deleted file mode 100644 index 692b76e61..000000000 --- a/theories/L/Reductions/HaltL_to_HaltLclosed.v +++ /dev/null @@ -1,18 +0,0 @@ - -Require Import Undecidability.Synthetic.Definitions. -From Undecidability.L Require Import L Functions.Eval Util.L_facts. -Import L_Notations. - -(* Halting problem for weak call-by-value lambda-calculus *) -Definition HaltLclosed (s : {s : term | closed s}) := exists t, eval (proj1_sig s) t. - -Lemma reduction : HaltL ⪯ HaltLclosed. -Proof. - unshelve eexists. - - intros s. exists (Eval (enc s)). unfold Eval. Lproc. - - cbn. intros s. unfold HaltL. split; intros (t & Ht). - + eapply eval_converges. edestruct Eval_converges. eapply H. - eapply eval_iff in Ht. eauto. - + setoid_rewrite eval_iff. eapply eval_converges. - eapply Eval_converges. eapply Seval.eval_converges. eauto. -Qed. diff --git a/theories/L/Reductions/HaltMuRec_to_HaltL.v b/theories/L/Reductions/HaltMuRec_to_HaltL.v index 95849774e..d6ed06fc9 100644 --- a/theories/L/Reductions/HaltMuRec_to_HaltL.v +++ b/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,6 +563,13 @@ 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. @@ -564,13 +577,13 @@ Proof. 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. } diff --git a/theories/L/Reductions/MMA_HALTING_to_HaltLclosed.v b/theories/L/Reductions/MMA_HALTING_to_HaltLclosed.v new file mode 100644 index 000000000..73076b5f7 --- /dev/null +++ b/theories/L/Reductions/MMA_HALTING_to_HaltLclosed.v @@ -0,0 +1,748 @@ +(* + Author(s): + Andrej Dudenhefner (1) + Affiliation(s): + (1) TU Dortmund University, Dortmund, Germany +*) + +(* + Reduction from: + Alternate Minsky Machine with n Registers Halting (MMA_HALTING n) + to: + Halting Problem for Weak Call-by-value lambda-Calculus (HaltLclosed) +*) + +Require Import List PeanoNat Lia Relations Transitive_Closure. +Import ListNotations. + +From Undecidability.MinskyMachines Require Import MMA Util.MMA_facts mma_defs. + +From Undecidability.L Require Import L Util.term_facts. +From Undecidability.L Require Util.L_facts Prelim.ARS. +Import L_facts (step). + +From Undecidability.Shared Require Import Libs.DLW.Code.sss simulation. + +Require Import ssreflect. + +Unset Implicit Arguments. + +Set Default Goal Selector "!". + +(* general facts *) + +Lemma vec_pos_nth {X : Type} {n} {v : Vector.t X n} {i} : + vec.vec_pos v i = Vector.nth v i. +Proof. + elim: v i; first by apply: Fin.case0. + move=> ?? v IH i. + pattern i. by apply: (Fin.caseS' i). +Qed. + +Lemma vec_change_replace {X : Type} {n} (v : Vector.t X n) i x : + vec.vec_change v i x = Vector.replace v i x. +Proof. + elim: v i; first by apply: Fin.case0. + move=> ?? v IH i. + pattern i. apply: (Fin.caseS' i); first done. + move=> ?. by congr Vector.cons. +Qed. + +Lemma nth_order_map : forall (X Y : Type) (f : X -> Y) (n : nat) (v : Vector.t X n) (i : nat) (H : i < n), + Vector.nth_order (Vector.map f v) H = f (Vector.nth_order v H). +Proof. + move=> X Y f n. elim; first by lia. + move=> x {}n v IH [|i] H /=; first done. + by apply: IH. +Qed. + +Lemma nth_order_nth {X : Type} {n} (v : Vector.t X n) i {k} (H : k < n) : + proj1_sig (Fin.to_nat i) = k -> Vector.nth_order v H = VectorDef.nth v i. +Proof. + elim: v k i H. + - move=> ?. by apply: Fin.case0. + - move=> x {}n v IH [|k] i /=. + + pattern i; apply: (Fin.caseS' i); first done. + move=> i' /=. case: (Fin.to_nat i')=> /=. lia. + + move=> ?. pattern i; apply: (Fin.caseS' i); first done. + move=> i' /=. move E: (Fin.to_nat i') => [m Hm] /= [?]. + apply: IH. by rewrite E. +Qed. + +Lemma vec_In_nil {X : Type} {x} : Vector.In x (Vector.nil X) -> False. +Proof. + intros H. by inversion H. +Qed. + +Lemma vec_In_replace {X : Type} {n} {v : Vector.t X n} {i x y} : + Vector.In y (Vector.replace v i x) -> y = x \/ Vector.In y v. +Proof. + elim: v i x. + - by apply: Fin.case0. + - move=> x {}n v IH /= i x'. + pattern i. apply: (Fin.caseS' i). + + move=> /= /Vector.In_cons_iff [<-|?]; first by left. + right. by constructor. + + move=> /= j /Vector.In_cons_iff [<-|/IH [?|?]]. + * right. by constructor. + * by left. + * right. by constructor. +Qed. + +Lemma vec_In_map {X Y : Type} {n} {f : X -> Y} {v : Vector.t X n} {y} : + Vector.In y (Vector.map f v) -> exists x, y = f x /\ Vector.In x v. +Proof. + elim: v. + - by move=> /vec_In_nil. + - move=> x {}n v IH /= /Vector.In_cons_iff [<-|/IH]. + + eexists. split; first done. by constructor. + + move=> [? [-> ?]]. + eexists. split; first done. by constructor. +Qed. + +Lemma clos_t_rt_t {A : Type} {R : relation A} (x y z : A) : + clos_trans A R x y -> clos_refl_trans A R y z -> clos_trans A R x z. +Proof. + move=> H /clos_rt_rtn1_iff H'. elim: H' H; by eauto using clos_trans. +Qed. + +Lemma map_nth' {X Y : Type} {f : X -> Y} {l i} {d} d' : i < length l -> nth i (map f l) d = f (nth i l d'). +Proof. + move=> H. rewrite (nth_indep _ _ (f d')); first by rewrite length_map. + by apply: map_nth. +Qed. + +Lemma combine_map_l {A B C} (f : A -> B) (l : list A) (r : list C) : + combine (map f l) r = map (fun '(x, y) => (f x, y)) (combine l r). +Proof. + elim: l r; first done. + move=> > IH [|? r]; first done. + move=> /=. by rewrite IH. +Qed. + +Lemma clos_trans_flip {X : Type} {R : X -> X -> Prop} {x y} : clos_trans _ R x y -> + clos_trans _ (fun y x => R x y) y x. +Proof. by elim; eauto using clos_trans. Qed. + +#[local] Notation lams k M := (Nat.iter k lam M). +#[local] Notation apps M Ns := (fold_left app Ns M). + +Section MMA_HALTING_to_HaltLclosed. + +Opaque Nat.add Nat.sub. + +Context {num_regs : nat}. (* number of registers - 1 *) +Notation N := (S num_regs). +Context (P : list (MM.mm_instr (Fin.t N))). (* program *) + +#[local] Hint Rewrite subst_apps : subst. + +Lemma eval_lams_S n s : eval (lams (S n) s) (lams (S n) s). +Proof. + by constructor. +Qed. + +#[local] Hint Resolve eval_lams_S : core. + +Opaque Nat.iter. + +(* remap machine addresses to 0 .. n (n + 1 => 0) *) +Definition addr i := + match i - length P with + | 0 => i + | S i => 0 + end. + +Lemma addr_spec_in_code {l instr r} : + P = l ++ instr :: r -> + addr (S (length l)) = S (length l). +Proof. + rewrite /addr=> ->. rewrite length_app /=. + by have ->: S (length l) - (length l + S (length r)) = 0 by lia. +Qed. + +Lemma addr_spec_out_code {i} : i < 1 \/ S (length P) <= i -> addr i = 0. +Proof. + rewrite /addr => - [?|?]. + - have ->: i = 0 by lia. + by case: (length P). + - by have ->: i - length P = S (i - length P - 1) by lia. +Qed. + +Definition pi i := lams (S (length P)) (var i). + +Lemma eval_pi i : eval (pi i) (pi i). +Proof. + by rewrite /pi. +Qed. + +Lemma pi_addr_closed i : closed (pi (addr i)). +Proof. + move=> k u. rewrite /pi subst_lams /=. + have /Nat.eqb_neq ->: addr i <> S (length P + k); last done. + rewrite /addr. + case E: (i - length P) => [|]; lia. +Qed. + +#[local] Hint Resolve eval_pi : core. +#[local] Hint Rewrite pi_addr_closed : subst. + +Lemma apps_pi_spec {i} ts t : + Forall (fun t' => eval t' t') ts -> + Forall closed ts -> + length ts = S (length P) -> + eval (nth i (rev ts) (var 0)) t -> + eval (apps (pi i) ts) t. +Proof. + move=> ?? Hts Ht. rewrite /pi -Hts. + apply: eval_apps_lams; [done..|]. + rewrite /= (nth_indep _ _ (var 0)); last done. + suff : i >= length (rev ts) -> False by lia. + move=> ?. rewrite nth_overflow in Ht; first done. + by inversion Ht. +Qed. + +Opaque addr pi. + +Lemma nat_enc_closed n : closed (nat_enc n). +Proof. + elim: n; first done. + move=> n IH u k /=. by rewrite IH. +Qed. + +Lemma eval_nat_enc n : eval (nat_enc n) (nat_enc n). +Proof. + by case: n; constructor. +Qed. + +#[local] Hint Resolve eval_nat_enc : core. +#[local] Hint Rewrite nat_enc_closed : subst. + +Lemma nat_enc_inj n m : nat_enc n = nat_enc m -> n = m. +Proof. + elim: n m. + - by case. + - move=> n IH [|m] /=; first done. + by move=> [/IH] <-. +Qed. + +(* encode register values *) +(* \f.f c1 ... cN *) +Definition enc_regs (regs : Vector.t nat N) := lam (apps (var 0) (Vector.to_list (Vector.map nat_enc regs))). + +Lemma eval_enc_regs ts : eval (enc_regs ts) (enc_regs ts). +Proof. + by constructor. +Qed. + +Lemma enc_regs_closed v : closed (enc_regs v). +Proof. + rewrite /enc_regs. move=> k u. + rewrite /= subst_apps /=. + rewrite Vector.to_list_map map_map. + congr lam. congr fold_left. + apply: map_ext=> ?. by rewrite nat_enc_closed. +Qed. + +#[local] Hint Resolve eval_enc_regs : core. +#[local] Hint Rewrite enc_regs_closed : subst. + +Lemma enc_regs_spec v s t : + eval (substs 0 (rev (Vector.to_list (Vector.map nat_enc v))) s) t -> + eval (app (enc_regs v) (lams N s)) t. +Proof. + move=> H. econstructor; [constructor|done|]. + rewrite subst_apps /=. apply: eval_apps_lams. + - by rewrite length_map Vector.length_to_list. + - apply /Forall_map. apply /Vector.to_list_Forall. + apply /Vector.Forall_map. + apply /Vector.Forall_nth=> y. rewrite nat_enc_closed. + by apply: eval_nat_enc. + - apply /Forall_map. apply /Vector.to_list_Forall. + apply /Vector.Forall_map. + apply /Vector.Forall_nth=> y. rewrite nat_enc_closed. + by apply: nat_enc_closed. + - move: H. congr eval. congr substs. congr rev. + rewrite -Vector.to_list_map Vector.map_map. + congr Vector.to_list. apply: Vector.map_ext. + move=> c. by rewrite nat_enc_closed. +Qed. + +Opaque enc_regs. + +Definition nat_succ := lam (lam (lam (app (var 0) (var 2)))). + +Lemma nat_succ_closed : closed nat_succ. +Proof. + done. +Qed. + +#[local] Hint Rewrite nat_succ_closed : subst. + +Lemma nat_succ_spec t c : eval t (nat_enc c) -> eval (app nat_succ t) (nat_enc (S c)). +Proof. + rewrite /nat_succ. move=> H. + econstructor; [constructor|eassumption|]. + rewrite /=. by constructor. +Qed. + +Opaque nat_succ. + +(* just use of_list seq ? *) +Fixpoint rev_vec_seq n : Vector.t nat n := + match n with + | 0 => Vector.nil _ + | S n => Vector.cons _ n _ (rev_vec_seq n) + end. + +Lemma rev_vec_seq_S n : rev_vec_seq (S n) = Vector.cons _ n _ (rev_vec_seq n). +Proof. + done. +Qed. + +Lemma vec_In_rev_seq n i : Vector.In i (rev_vec_seq n) -> i < n. +Proof. + elim: n. + - by move=> /vec_In_nil. + - move=> n IH. rewrite rev_vec_seq_S. + move=> /Vector.In_cons_iff [->|/IH]; lia. +Qed. + +Opaque rev_vec_seq. + +Lemma vec_nth_rev_seq n i : VectorDef.nth (rev_vec_seq n) i = n - 1 - proj1_sig (Fin.to_nat i). +Proof. + elim: n i. + - by apply: Fin.case0. + - move=> n IH i. + pattern i. apply: (Fin.caseS' i). + + rewrite rev_vec_seq_S /=. lia. + + move=> {}i /=. rewrite rev_vec_seq_S /= IH. + move: (Fin.to_nat i) => [m Hm] /=. lia. +Qed. + +(* get nth vector element *) +Definition enc_nth (x : Fin.t N) : term := + (* \c1 .. cN.cx *) + lams N (var (N - 1 - proj1_sig (Fin.to_nat x))). + +Lemma enc_nth_closed x : closed (enc_nth x). +Proof. + move=> k u. rewrite /= subst_lams /=. + by have /Nat.eqb_neq ->: N - 1 - proj1_sig (Fin.to_nat x) <> N + k by lia. +Qed. + +Lemma enc_nth_spec x v : eval (app (enc_regs v) (enc_nth x)) (nat_enc (Vector.nth v x)). +Proof. + apply: enc_regs_spec. + move Ex: (Fin.to_nat x) => [n Hn] /=. + rewrite /= rev_nth Vector.length_to_list; first lia. + rewrite -Vector.to_list_nth_order; [|lia]. + move=> Hm. rewrite nth_order_map. + rewrite -(Fin.of_nat_to_nat_inv x) Ex /=. + rewrite (@nth_order_nth _ _ _ (Fin.of_nat_lt Hn)) ?Fin.to_nat_of_nat /=; first lia. + by apply: eval_nat_enc. +Qed. + +#[local] Hint Resolve enc_nth_spec : core. +#[local] Hint Rewrite enc_nth_closed : subst. +Opaque enc_nth. + +(* set nth vector element *) +Definition enc_replace (x : Fin.t N) : term := + (* \c.\c1 .. cN.\f.f c1 .. c .. cN *) + lam (lams N (lam (apps (var 0) (map var (Vector.to_list (Vector.replace (Vector.map S (rev_vec_seq N)) x (N + 1))))))). + +Lemma enc_replace_closed x : closed (enc_replace x). +Proof. + move=> k u. rewrite /= subst_lams /= subst_apps /=. + rewrite /enc_replace. + rewrite map_map -!Vector.to_list_map. + congr lam. congr Nat.iter. congr lam. congr fold_left. + congr Vector.to_list. apply: Vector.map_ext_in => n /= /vec_In_replace H. + have /Nat.eqb_neq ->: n <> S (S (num_regs + S k)); last done. + move: H => [->|]; first by lia. + move=> /vec_In_map [?] [->] /vec_In_rev_seq. lia. +Qed. + +Lemma enc_replace_spec x v c t : + eval t (nat_enc c) -> + eval (app (enc_regs v) (app (enc_replace x) t)) (enc_regs (Vector.replace v x c)). +Proof. + move=> Hc. apply: rt_steps_eval_eval. + - apply: rt_steps_app_l. apply: eval_rt_steps_subst. by eassumption. + - rewrite subst_lams. + apply: enc_regs_spec. + rewrite /= subst_apps substs_apps. apply: eval_lam. + rewrite /=. congr lam. congr fold_left. + rewrite !map_map. + rewrite -!Vector.to_list_map. + congr Vector.to_list. + apply /Vector.eq_nth_iff=> i ? <-. + rewrite !(Vector.nth_map _ _ _ _ eq_refl) /=. + have [?|?] := Fin.eq_dec i x. + + subst i. rewrite !Vector.nth_replace_eq. + have /Nat.eqb_eq ->: S (num_regs + 1) = S (S (num_regs + 0)) by lia. + rewrite substs_closed; last done. + by apply: nat_enc_closed. + + rewrite !Vector.nth_replace_neq; [done..|]. + rewrite (Vector.nth_map _ _ _ _ eq_refl). + rewrite vec_nth_rev_seq /=. + have /Nat.eqb_neq -> /=: N - 1 - proj1_sig (Fin.to_nat i) <> S (num_regs + 0) by lia. + move Ei: (Fin.to_nat i) => [n Hn] /=. + rewrite rev_nth Vector.length_to_list; first lia. + rewrite -Vector.to_list_nth_order; [|lia]. + move=> ?. rewrite nth_order_map. congr nat_enc. + apply: nth_order_nth. rewrite Ei /=. lia. +Qed. + +#[local] Hint Resolve enc_replace_spec : core. +#[local] Hint Rewrite enc_replace_closed : subst. +Opaque enc_replace. + +Definition enc_instr '(i, instr) : term := + match instr with + | MM.mm_inc x => + (* \cs.(\cs'.\f.f (pi (S i)) cs') (inc x cs) *) + lam (app (lam (lam (apps (var 0) [pi (addr (S i)); var 1]))) (app (var 0) (app (enc_replace x) (app nat_succ (app (var 0) (enc_nth x)))))) + | MM.mm_dec x j => + (* \cs.(nth x cs) (\f. f (pi (S i)) cs) (\c.(\c'.\f. f (pi j) c') (replace x cs c)) *) + lam (apps (var 0) [enc_nth x; + lam (apps (var 0) [pi (addr (S i)); var 1]); + lam (app (lam (lam (apps (var 0) [pi (addr j); var 1]))) (app (var 1) (app (enc_replace x) (var 0))))]) + end. + +Lemma enc_instr_closed o : closed (enc_instr o). +Proof. + move=> k u. case: o=> i [instr|instr x] /=; by autorewrite with subst. +Qed. + +Lemma eval_enc_instr o : eval (enc_instr o) (enc_instr o). +Proof. + move: o => [] ? []; by constructor. +Qed. + +#[local] Hint Resolve eval_enc_instr : core. +#[local] Hint Rewrite enc_instr_closed : subst. + +Definition enc_recurse := + (* \i.\cs.\run.run i cs run *) + lam (lam (lam (apps (var 0) [var 2; var 1; var 0]))). + +Lemma enc_recurse_closed : closed enc_recurse. +Proof. + done. +Qed. + +Lemma eval_enc_recurse : eval enc_recurse enc_recurse. +Proof. + by constructor. +Qed. + +#[local] Hint Resolve eval_enc_recurse : core. +#[local] Hint Rewrite enc_recurse_closed : subst. + +(* \cs.\f.\run.cs *) +Definition enc_halt := lam (lam (lam (var 2))). +(* \i.i (halt :: P) *) +Definition enc_step := lam (apps (var 0) (rev (enc_halt :: map enc_instr (combine (seq 1 (length P)) P)))). + +Lemma enc_halt_closed : closed enc_halt. +Proof. + done. +Qed. + +Lemma eval_enc_halt : eval enc_halt enc_halt. +Proof. + by constructor. +Qed. + +Lemma enc_halt_spec cs : + clos_refl_trans _ step + (apps enc_halt [enc_regs cs; enc_recurse; lam (lam (apps enc_step [var 1; var 0; enc_recurse]))]) + (enc_regs cs). +Proof. + rewrite /enc_halt /=. + apply: rt_trans. + { do 2 apply: rt_steps_app_r. by apply: eval_rt_steps_subst. } + apply: rt_trans. + { apply: rt_steps_app_r. rewrite /=. by apply: eval_rt_steps_subst. } + apply: rt_trans. + { rewrite /=. apply: eval_rt_steps_subst. by constructor. } + autorewrite with subst. by apply: rt_refl. +Qed. + +#[local] Hint Resolve eval_enc_halt : core. +#[local] Hint Rewrite enc_halt_closed : subst. + +Lemma map_subst_map_enc_instr k t l : map (fun u => subst u k t) (map enc_instr l) = map enc_instr l. +Proof. + rewrite map_map. apply: map_ext=> ?. by rewrite enc_instr_closed. +Qed. + +Lemma enc_step_closed : closed enc_step. +Proof. + rewrite /enc_step. move=> k u /=. rewrite subst_apps /=. + rewrite map_app map_rev map_subst_map_enc_instr /=. + by autorewrite with subst. +Qed. + +Lemma enc_step_spec l instr r cs : + P = l ++ instr :: r -> + clos_refl_trans term step + (apps enc_step [pi (addr (S (length l))); enc_regs cs]) + (app (enc_instr (S (length l), instr)) (enc_regs cs)). +Proof. + move=> HP. + apply: rt_trans. + { rewrite /= /enc_step. apply: rt_steps_app_r. by apply: eval_rt_steps_subst. } + apply: rt_trans. + { rewrite /= subst_apps /=. apply: rt_steps_app_r. + autorewrite with subst. + rewrite map_app map_rev map_subst_map_enc_instr /=. + apply: eval_rt_steps. apply: apps_pi_spec. + - apply /Forall_app. split. + + by apply /Forall_rev /Forall_map /Forall_forall=> *. + + constructor; by autorewrite with subst. + - apply /Forall_app. split. + + apply /Forall_rev /Forall_map /Forall_forall=> * ??. by autorewrite with subst. + + constructor; by autorewrite with subst. + - rewrite length_app length_rev length_map length_combine length_seq /=. lia. + - rewrite rev_app_distr rev_involutive (addr_spec_in_code HP) /=. + rewrite (map_nth' (0, MM.mm_inc Fin.F1)). + { rewrite length_combine length_seq HP length_app /=. lia. } + rewrite combine_nth; first by rewrite length_seq. + rewrite seq_nth. + { rewrite HP length_app /=. lia. } + have ->: nth (length l) P (INCₐ Fin.F1) = instr; last done. + { by rewrite HP app_nth2 ?Nat.sub_diag. } } + by apply: rt_refl. +Qed. + +Lemma enc_step_0_spec : + clos_refl_trans term step (app enc_step (pi 0)) enc_halt. +Proof. + rewrite /enc_step. + apply: rt_trans. + { by apply: eval_rt_steps_subst. } + apply: rt_trans. + { rewrite /= subst_apps map_app map_rev map_subst_map_enc_instr /=. + apply: eval_rt_steps. apply: apps_pi_spec. + - apply /Forall_app. split. + + by apply /Forall_rev /Forall_map /Forall_forall=> *. + + constructor; by autorewrite with subst. + - apply /Forall_app. split. + + apply /Forall_rev /Forall_map /Forall_forall=> * ??. by autorewrite with subst. + + constructor; by autorewrite with subst. + - rewrite length_app length_rev length_map length_combine length_seq /=. lia. + - by rewrite rev_app_distr rev_involutive /=. } + by apply: rt_refl. +Qed. + +#[local] Hint Rewrite enc_step_closed : subst. +Opaque enc_recurse enc_halt enc_step. + +Lemma mma_step_sim (instr : MM.mm_instr (Fin.t N)) (p q : mm_state N) : + mma_sss instr p q -> + clos_refl_trans _ step + (apps (enc_instr (fst p, instr)) [enc_regs (snd p); enc_recurse]) + (apps enc_recurse [pi (addr (fst q)); enc_regs (snd q)]). +Proof. + case. + - (* INC *) + move=> i x v /=. rewrite vec_change_replace vec_pos_nth. + apply: rt_trans. + { apply: rt_steps_app_r. by apply: eval_rt_steps_subst. } + apply: rt_trans. + { apply: rt_steps_app_r. rewrite /=. apply: rt_steps_app_l. + autorewrite with subst. apply: eval_rt_steps. + apply: enc_replace_spec. apply: nat_succ_spec. by apply: enc_nth_spec. } + apply: rt_trans. + { apply: rt_steps_app_r. autorewrite with subst. by apply: eval_rt_steps_subst. } + apply: rt_trans. + { rewrite /=. by apply: eval_rt_steps_subst. } + rewrite /=. autorewrite with subst. by apply: rt_refl. + - (* DEC *) + move=> i x j v. rewrite vec_pos_nth /==> Hx. + apply: rt_trans. + { apply: rt_steps_app_r. + apply: rt_trans. + { by apply: eval_rt_steps_subst. } + apply: rt_trans. + { rewrite /=. autorewrite with subst. do 2 apply: rt_steps_app_r. by apply: eval_rt_steps. } + rewrite Hx /=. apply: rt_trans. + { apply: rt_steps_app_r. apply: rt_step. by constructor. } + apply: rt_step. rewrite /=. by constructor. } + apply: rt_trans. + { rewrite /=. autorewrite with subst. by apply: eval_rt_steps_subst. } + rewrite /=. autorewrite with subst. by apply: rt_refl. + - (* JUMP *) + move=> i x j v c. rewrite vec_pos_nth vec_change_replace /==> Hx. + apply: rt_trans. + { apply: rt_steps_app_r. + apply: rt_trans. + { by apply: eval_rt_steps_subst. } + apply: rt_trans. + { rewrite /=. autorewrite with subst. do 2 apply: rt_steps_app_r. by apply: eval_rt_steps. } + rewrite Hx /=. apply: rt_trans. + { apply: rt_steps_app_r. apply: rt_step. by constructor. } + apply: rt_step. rewrite /=. by constructor. } + apply: rt_trans. + { rewrite /=. autorewrite with subst. apply: rt_steps_app_r. by apply: eval_rt_steps_subst. } + apply: rt_trans. + { rewrite /=. autorewrite with subst. apply: rt_steps_app_r. apply: rt_steps_app_l. + apply: eval_rt_steps. by apply: enc_replace_spec. } + apply: rt_trans. + { apply: rt_steps_app_r. by apply: eval_rt_steps_subst. } + apply: rt_trans. + { rewrite /=. autorewrite with subst. by apply: eval_rt_steps_subst. } + rewrite /=. autorewrite with subst. by apply: rt_refl. +Qed. + +(* \i.\cs.step i cs recurse *) +Definition enc_run := lam (lam (apps enc_step [var 1; var 0; enc_recurse])). + +Lemma enc_run_closed : closed enc_run. +Proof. + rewrite /enc_run. move=> k u /=. by autorewrite with subst. +Qed. + +Lemma eval_enc_run : eval enc_run enc_run. +Proof. + by constructor. +Qed. + +#[local] Hint Rewrite enc_run_closed : subst. +#[local] Hint Resolve eval_enc_run : core. + +Lemma enc_recurse_spec p : + clos_refl_trans term step + (apps enc_recurse [pi (addr (fst p)); enc_regs (snd p); enc_run]) + (apps enc_run [pi (addr (fst p)); enc_regs (snd p); enc_run]). +Proof. + apply: rt_trans. + { apply: rt_steps_app_r. apply: rt_steps_app_r. apply: rt_step. by apply: step_app'. } + apply: rt_trans. + { apply: rt_steps_app_r. apply: rt_step. rewrite /=. by apply: step_app'. } + apply: rt_trans. + { apply: rt_step. rewrite /=. by apply: step_app'. } + rewrite /=. autorewrite with subst. by apply: rt_refl. +Qed. + +Opaque enc_recurse. + +Lemma t_steps_enc_run_enc_step i cs : + clos_trans term step + (apps enc_run [pi (addr i); enc_regs cs]) + (apps enc_step [pi (addr i); enc_regs cs; lam (lam (lam (apps (var 0) [var 2; var 1; var 0])))]). +Proof. + apply: t_trans. + { apply: t_steps_app_r. apply: t_step. apply: step_app'. by apply: eval_pi. } + apply: clos_t_rt_t. + { rewrite /=. apply: t_step. by apply: step_app'. } + rewrite /=. autorewrite with subst. by apply: rt_refl. +Qed. + +Opaque enc_instr. + +Lemma enc_run_spec (p q : mm_state N) : @sss_step _ _ (@mma_sss N) (1, P) p q -> + clos_trans term step + (apps enc_run [pi (addr (fst p)); enc_regs (snd p); enc_run]) + (apps enc_run [pi (addr (fst q)); enc_regs (snd q); enc_run]). +Proof. + move=> [k [l [instr [r [cs]]]]]. + move=> [[??]] [?]. subst k p. + move=> /mma_step_sim Hpq. apply: clos_t_rt_t. + { rewrite /=. apply: t_steps_app_r. by apply: t_steps_enc_run_enc_step. } + apply: rt_trans. + { apply: rt_steps_app_r. apply: rt_steps_app_r. rewrite /=. + apply: enc_step_spec. by eassumption. } + apply: rt_trans. + { apply: rt_steps_app_r. by eassumption. } + by apply: enc_recurse_spec. +Qed. + +Lemma enc_run_spec_out_code (p : mm_state N) : fst p < 1 \/ S (length P) <= fst p -> + clos_refl_trans _ step (apps enc_run [pi (addr (fst p)); enc_regs (snd p); enc_run]) (enc_regs (snd p)). +Proof. + move=> Hp. rewrite /enc_run. + apply: rt_trans. + { apply: rt_steps_app_r. apply: rt_steps_app_r. by apply: eval_rt_steps_subst. } + apply: rt_trans. + { apply: rt_steps_app_r. rewrite /=. by apply: eval_rt_steps_subst. } + apply: rt_trans. + { apply: rt_steps_app_r. rewrite /=. autorewrite with subst. + rewrite (addr_spec_out_code Hp). do 2 apply: rt_steps_app_r. by apply: enc_step_0_spec. } + by apply: enc_halt_spec. +Qed. + +Definition sync p t := t = apps enc_run [pi (addr (fst p)); enc_regs (snd p); enc_run]. + +Lemma sss_step_transport p q s : + sss_step (@mma_sss N) (1, P) p q -> + sync p s -> + exists t, clos_trans term step s t /\ sync q t. +Proof. + move=> /enc_run_spec H ->. + by exists (apps enc_run [pi (addr (fst q)); enc_regs (snd q); enc_run]). +Qed. + +Lemma stuck_sss_step_transport p s : + stuck (sss_step (@mma_sss N) (1, P)) p -> + sync p s -> terminates step s. +Proof. + move=> /(out_code_iff (@mma_sss_total_ni _)) Hp ->. + exists (enc_regs (snd p)). split. + - by apply: enc_run_spec_out_code. + - move=> t. intros H. by inversion H. +Qed. + +Opaque enc_run. + +Lemma closed_apps_enc_run i cs : closed (apps enc_run [pi (addr i); enc_regs cs; enc_run]). +Proof. + move=> k u. rewrite subst_apps /=. by autorewrite with subst. +Qed. + +End MMA_HALTING_to_HaltLclosed. + +Require Import Undecidability.Synthetic.Definitions. + +Theorem reduction n : @MMA_HALTING n ⪯ HaltLclosed. +Proof. + destruct n as [|n]. + { unshelve eexists. + - intros _. now exists (lam (var 0)). + - intros [[|??] st]. + + split. + * intros _. exists (lam (var 0)). by constructor. + * intros _. unfold MMA_HALTING, sss_terminates. exists (1, st). + unfold sss_output, sss_compute. split. + ** exists 0. now apply in_sss_steps_0. + ** now right. + + now destruct m as [x|x ?]; pattern x; apply Fin.case0. } + unshelve eexists. + - intros [P v]. exists (apps (enc_run P) [pi P (addr P 1); enc_regs v; enc_run P]). + apply closed_apps_enc_run. + - intros [P v]. split. + + intros ?%(sss_terminates_iff (@mma_sss_total_ni _)). + destruct (@terminates_transport _ _ + (sss_step (@mma_sss (S n)) (1, P)) + L_facts.step + (sync P) + (@sss_step_transport _ P) + (@stuck_sss_step_transport _ P) + (1, v) _ eq_refl H) as [t [H1t H2t]]. + exists t. cbn. eapply steps_stuck_eval; [|assumption..]. + apply closed_apps_enc_run. + + intros [t Ht%eval_steps_stuck]. cbn in Ht. + apply (sss_terminates_iff (@mma_sss_total_ni _)). + apply (@terminates_reflection _ _ + (sss_step (@mma_sss (S n)) (1, P)) + L_facts.step + (sync P) + L_facts.uniform_confluence + (@sss_step_transport _ P) + (fun p => sss_step_or_stuck (@mma_sss_total_ni _) p 1 P) + (1, v) _ eq_refl Ht). +Qed. diff --git a/theories/L/Reductions/MMA_computable_to_L_computable_closed.v b/theories/L/Reductions/MMA_computable_to_L_computable_closed.v new file mode 100644 index 000000000..1f27174d0 --- /dev/null +++ b/theories/L/Reductions/MMA_computable_to_L_computable_closed.v @@ -0,0 +1,251 @@ +(* + Author(s): + Andrej Dudenhefner (1) + Affiliation(s): + (1) TU Dortmund University, Dortmund, Germany +*) + +(* + Minsky Machine combinability (MMA_computable) implies L computability (L_computable_closed) +*) + +Require Import List PeanoNat Lia Relations Transitive_Closure. +Import ListNotations. + +From Undecidability.MinskyMachines Require Import MMA Util.MMA_facts mma_defs. + +From Undecidability.L Require Import L Util.term_facts. +From Undecidability.L Require Util.L_facts Prelim.ARS. +Import L_facts (step). + +From Undecidability.Shared Require Import Libs.DLW.Code.sss simulation. + +Require Import Undecidability.L.Reductions.MMA_HALTING_to_HaltLclosed. + +Require Import ssreflect. + +Unset Implicit Arguments. + +Set Default Goal Selector "!". + +#[local] Notation lams k M := (Nat.iter k lam M). +#[local] Notation apps M Ns := (fold_left app Ns M). + +Fixpoint fin_seq n : list (Fin.t n) := + match n with + | 0 => [] + | S n => Fin.F1 :: map Fin.FS (fin_seq n) + end. + +Opaque Vector.to_list Fin.L. + +(* apps (enc_regs (Vector.const 0 (1 + k + n))) (Vector.to_list (Vector.map (fun x => enc_replace (Fin.L n (Fin.FS x))) (rev_vec_seq k)))*) +Definition enc_set_state k n : term := + apps (enc_regs (Vector.const 0 (1 + k + n))) + (map (fun '(x, i) => app (enc_replace (Fin.FS (Fin.L n x))) (var i)) (combine (fin_seq k) (rev (seq 0 k)))). + +Opaque enc_replace Vector.to_list. + +Lemma substs_enc_set_state k n (v : Vector.t nat k) : + clos_refl_trans _ step + (substs 0 (rev (map nat_enc (VectorDef.to_list v))) (enc_set_state k n)) + (enc_regs (Vector.append (Vector.cons nat 0 k v) (Vector.const 0 n))) . +Proof. + have : clos_refl_trans _ step + (substs 0 (rev (map nat_enc (VectorDef.to_list v))) (enc_set_state k n)) + (enc_regs (fold_left (fun w '(x, c) => Vector.replace w (Fin.FS (Fin.L n x)) c) (combine (fin_seq k) (Vector.to_list v)) (Vector.const 0 (1 + k + n)))). + { rewrite /enc_set_state. + move: (Vector.const 0 (1 + k + n))=> cs. + rewrite substs_apps substs_closed; first by apply: enc_regs_closed. + have ->: forall xs, map (substs 0 (rev (map nat_enc (VectorDef.to_list v)))) + (map (fun '(x, i) => app (enc_replace (Fin.L n (Fin.FS x))) (var i)) + (combine xs (rev (seq 0 k)))) = + map (fun '(x, c) => app (enc_replace (Fin.L n (Fin.FS x))) (nat_enc c)) + (combine xs (Vector.to_list v)). + { elim: v; first by move=> ? [|??]. + move=> c k' v IH ? [|x xs]; first done. + have ->: seq 0 (S k') = seq 0 (k' + 1). + { congr seq. lia. } + rewrite seq_app rev_app_distr Vector.to_list_cons /=. congr cons. + - rewrite substs_closed; first by apply: enc_replace_closed. + congr app. rewrite app_nth2 length_rev length_map Vector.length_to_list; first done. + by rewrite Nat.sub_diag. + - rewrite -IH. apply: map_ext_in=> s /in_map_iff [[y j]] [<-]. + move=> /(@in_combine_r (Fin.t _) nat) /in_rev. + rewrite rev_involutive=> /in_seq ? /=. + rewrite !substs_closed; [by apply: enc_replace_closed..|]. + congr app. rewrite app_nth1; last done. + rewrite length_rev length_map Vector.length_to_list. lia. } + + move: (fin_seq k)=> xs. + move: (Vector.to_list v)=> c's. + elim: xs c's cs {v}. + - move=> *. by apply: rt_refl. + - move=> x xs IH [|c' c's]. + + move=> *. by apply: rt_refl. + + move=> cs /=. apply: rt_trans. + { apply: rt_steps_apps_r. apply: eval_rt_steps. apply: enc_replace_spec. by apply: eval_nat_enc. } + by apply: IH. } + congr clos_refl_trans. congr enc_regs. + rewrite [RHS](@Vector.eta _ (k + n)) [LHS](@Vector.eta _ (k + n)). + congr (@Vector.cons _ _ (k + n)); rewrite /=. + - elim: (fin_seq k) (Vector.to_list v) (Vector.const 0 (k + n)); first done. + by move=> ?? IH [|??] ?; [|apply: IH]. + - apply /Vector.eq_nth_iff=> x ? <-. + pattern x. apply: Fin.case_L_R'=> {}x. + + rewrite Vector.nth_append_L. + have : forall x c, In (x, c) (combine (fin_seq k) (Vector.to_list v)) -> Vector.nth v x = c. + { elim: v; first done. + move=> > IH {}x c /=. rewrite Vector.to_list_cons /=. + move=> [[??]|]; first by subst. + rewrite combine_map_l. + move=> /in_map_iff [[??]] [[??]] /IH ?. by subst. } + have : In (x, Vector.nth v x) (combine (fin_seq k) (Vector.to_list v)). + { elim: v x; first by apply: Fin.case0. + move=> > IH x. + pattern x. apply: Fin.caseS'; first by left. + move=> {}x. rewrite Vector.to_list_cons /=. right. + rewrite combine_map_l. apply /in_map_iff. by eexists (_, _). } + rewrite -Vector.append_const. + move: (VectorDef.const 0 k). + elim /rev_ind: (combine (fin_seq k) (Vector.to_list v)); first done. + move=> [y j] ? IH ? /in_app_iff H'. + move=> H. rewrite fold_left_app /=. + rewrite [fold_left _ _ _](@Vector.eta _ (k + n)) /=. + have [?|?] := Fin.eq_dec x y. + * subst. rewrite Vector.nth_replace_eq. + rewrite (H y j); last done. + apply /in_app_iff. right. by left. + * rewrite Vector.nth_replace_neq; first by move=> /Fin.L_inj. + apply: IH=> *. + ** by move: H' => [|[[/(@eq_sym (Fin.t k))]|]]. + ** apply: H. apply /in_app_iff. by left. + + rewrite Vector.nth_append_R Vector.const_nth -Vector.append_const. + elim: (fin_seq k) (Vector.to_list v) (VectorDef.const 0 k). + * move=> /= *. by rewrite Vector.nth_append_R Vector.const_nth. + * move=> ?? IH [|??] ? /=; first by rewrite Vector.nth_append_R Vector.const_nth. + by rewrite Vector.replace_append_L IH. +Qed. + +Lemma subst_enc_set_state k n m u : subst (enc_set_state k n) (k + m) u = enc_set_state k n. +Proof. + rewrite /enc_set_state subst_apps enc_regs_closed. + congr fold_left. rewrite map_map. + apply: map_ext_in=> - [x i]. + rewrite /= enc_replace_closed. + move=> /(@in_combine_r (Fin.t k) nat) /in_rev. + rewrite rev_involutive. + move=> /in_seq ?. + by have /Nat.eqb_neq -> : i <> k + m by lia. +Qed. + +Opaque enc_run pi enc_set_state enc_nth. + +Lemma enc_init_spec {k n} (P : list (MM.mm_instr (Fin.t (1 + k + n)))) (v : Vector.t nat k) : + clos_refl_trans _ step + (Vector.fold_left (fun (s : term) c => app s (nat_enc c)) + (lams k (apps (enc_run P) [pi P (addr P 1); enc_set_state k n; enc_run P; enc_nth (@Fin.F1 (k + n))])) v) + (apps (enc_run P) [pi P (addr P 1); enc_regs (Vector.append (Vector.cons nat 0 k v) (Vector.const 0 n)); enc_run P; enc_nth (@Fin.F1 (k + n))]). +Proof. + rewrite Vector.to_list_fold_left. + have ->: forall cs t, fold_left (fun s c => app s (nat_enc c)) cs t = apps t (map nat_enc cs). + { elim; first done. + move=> > IH ? /=. by rewrite IH. } + apply: rt_trans. + { apply: steps_apps_lams. + - by rewrite length_map Vector.length_to_list. + - apply /Forall_map /Forall_forall=> *. by apply: eval_nat_enc. + - apply /Forall_map /Forall_forall=> *. by apply: nat_enc_closed. } + rewrite substs_apps /=. + apply: rt_trans. + { do 2 apply: rt_steps_app_r. apply: rt_steps_app_l. + by apply: substs_enc_set_state. } + rewrite !substs_closed; [by auto using enc_run_closed, pi_addr_closed, enc_nth_closed..|]. + by apply: rt_refl. +Qed. + +Theorem MMA_computable_to_L_computable_closed {k} (R : Vector.t nat k -> nat -> Prop) : + MMA_computable R -> L_computable_closed R. +Proof. + unfold MMA_computable, L_computable_closed. + move=> [n [P HP]]. + (* \c1...\ck. run pi_1 ((0...0) (set 1 c1) .. (set k ck)) run (\c'1...\c'n.c'1) *) + exists (lams k (apps (enc_run P) [pi P (addr P 1); enc_set_state k n; enc_run P; enc_nth (@Fin.F1 (k + n))])). + split. + - intros u ?. + rewrite subst_lams subst_apps !map_cons subst_enc_set_state. + by rewrite !enc_run_closed pi_addr_closed enc_nth_closed. + - move=> v. split. + + move=> m. rewrite HP. split. + * intros [c [v' [H1 H2]]]. + apply /L_facts.eval_iff. split; last by (case: (m); eexists). + apply /ARS.star_clos_rt_iff. apply: rt_trans. + { by apply: enc_init_spec. } + move=> /sss_compute_iff in H1. + have := @clos_refl_trans_transport _ _ + (sss_step (@mma_sss ((1 + k + n))) (1, P)) + L_facts.step + (sync P) + (@sss_step_transport _ P) + (1, Vector.append (Vector.cons nat 0 k v) (Vector.const 0 n)) + _ (c, Vector.cons nat m (k + n) v') eq_refl H1. + move=> [t [-> Ht]]. + apply: rt_trans. + { apply: rt_steps_app_r. by eassumption. } + apply: rt_trans. + { apply: rt_steps_app_r. by apply: enc_run_spec_out_code. } + apply: eval_rt_steps. by apply: enc_nth_spec. + * move=> /eval_rt_steps_eval => /(_ _ (enc_init_spec _ _)). + move: (Vector.append _ _)=> {}v /[dup] /eval_steps_stuck H'. + have /(@Acc_clos_trans term) := @terminating_Acc _ _ L_facts.uniform_confluence _ H'. + have [i Hi] : exists i, 1 = i by eexists. + rewrite [in addr P 1]Hi [in (1, v)]Hi. + move E: (apps _ _) => t H. + elim: H i v E {H' Hi}. + move=> {}t IH1 IH2 i v ?. subst t. + have [[[j w]]|] := sss_step_or_stuck (@mma_sss_total_ni _) (i, v) 1 P. + ** move=> /[dup] Hvw /enc_run_spec /=. + move=> /(@t_steps_app_r _ _ (enc_nth (@Fin.F1 (k + n)))). + move=> /[dup] /(@clos_trans_clos_refl_trans term) /eval_rt_steps_eval H' + /H'. + move=> /clos_trans_flip /IH2 /(_ _ _ eq_refl) /[apply]. + move=> [c] [v'] [??]. exists c, v'. split; last done. + apply: sss_compute_trans; last by eassumption. + apply /sss_compute_iff. + by apply: rt_step. + ** move=> /[dup] /(out_code_iff (@mma_sss_total_ni _)) /enc_run_spec_out_code H. + move=> /[dup] /(out_code_iff (@mma_sss_total_ni _)) H''. + move=> /stuck_sss_step_transport => /(_ _ eq_refl) [t] H'. + move: H=> /(rt_steps_app_r _ _ (enc_nth (@Fin.F1 (k + n)))). + move=> /eval_rt_steps_eval /[apply]. + have /L_facts.eval_iff [+ [??]] := enc_nth_spec (@Fin.F1 (k + n)) v. + move=> /ARS.star_clos_rt_iff /eval_rt_steps_eval /[apply]. + have := eval_nat_enc (Vector.nth v Fin.F1). + move=> /L_facts.eval_iff /L_facts.eval_unique + /L_facts.eval_iff => /[apply]. + move=> /nat_enc_inj <-. + exists i, (snd (@Vector.splitat _ 1 (k + n) v)). + split; last done. + apply /sss_compute_iff. + rewrite (Vector.eta v). + by apply: rt_refl. + + move=> o /eval_rt_steps_eval => /(_ _ (enc_init_spec _ _)). + move: (Vector.append _ _)=> {}v /[dup] /eval_steps_stuck H'. + have /(@Acc_clos_trans term) := @terminating_Acc _ _ L_facts.uniform_confluence _ H'. + move: (1) => i. + move E: (apps _ _) => t H. + elim: H i v E {H'}. + move=> {}t IH1 IH2 i v ?. subst t. + have [[[j w]]|] := sss_step_or_stuck (@mma_sss_total_ni _) (i, v) 1 P. + * move=> /enc_run_spec /=. + move=> /(@t_steps_app_r _ _ (enc_nth (@Fin.F1 (k + n)))). + move=> /[dup] /(@clos_trans_clos_refl_trans term) /eval_rt_steps_eval H' + /H'. + by move=> /clos_trans_flip /IH2 /(_ _ _ eq_refl) /[apply]. + * move=> /[dup] /(out_code_iff (@mma_sss_total_ni _)) /enc_run_spec_out_code H. + move=> /stuck_sss_step_transport => /(_ _ eq_refl) [t] H'. + move: H=> /(rt_steps_app_r _ _ (enc_nth (@Fin.F1 (k + n)))). + move=> /eval_rt_steps_eval /[apply]. + have /L_facts.eval_iff [+ [??]] := enc_nth_spec (@Fin.F1 (k + n)) v. + move=> /ARS.star_clos_rt_iff /eval_rt_steps_eval /[apply]. + have := eval_nat_enc (Vector.nth v Fin.F1). + move=> /L_facts.eval_iff /L_facts.eval_unique + /L_facts.eval_iff => /[apply] <-. + by eexists. +Qed. diff --git a/theories/L/Util/NaryApp.v b/theories/L/Util/NaryApp.v index 24a68aeae..040428e4e 100644 --- a/theories/L/Util/NaryApp.v +++ b/theories/L/Util/NaryApp.v @@ -1,4 +1,4 @@ -From Undecidability.L Require Import LTactics. +Require Import Undecidability.L.L Undecidability.L.Util.L_facts. Require Import Undecidability.Shared.Libs.PSL.Vectors.Vectors. Require Import Vector List. Import ListNotations. @@ -17,8 +17,8 @@ Qed. Fixpoint many_app k s (v : Vector.t term k) := match v with - | Vector.nil => s - | Vector.cons x _ v => many_app (L.app s x) v + | Vector.nil _ => s + | Vector.cons _ x _ v => many_app (L.app s x) v end. Lemma subst_many_app k (v : Vector.t term k) n u s : @@ -63,7 +63,7 @@ Qed. Fixpoint many_subst {k} s n (v : Vector.t term k) := match v with | [] => s - | Vector.cons u k v => many_subst (subst s (n + k) u) n v + | Vector.cons _ u k v => many_subst (subst s (n + k) u) n v end. Lemma beta_red s t t' : lambda t -> t' == subst s 0 t -> (lam s) t == t'. diff --git a/theories/L/Util/term_facts.v b/theories/L/Util/term_facts.v new file mode 100644 index 000000000..acc85f67f --- /dev/null +++ b/theories/L/Util/term_facts.v @@ -0,0 +1,221 @@ +Require Import List PeanoNat Lia Relations. +Import ListNotations. + +From Undecidability.L Require Import L. + +From Undecidability.L Require Util.L_facts Prelim.ARS. +Import L_facts (step). +Require Import Undecidability.Shared.simulation. + +Require Import ssreflect. + +Unset Implicit Arguments. + +Set Default Goal Selector "!". + +#[local] Notation lams k M := (Nat.iter k lam M). +#[local] Notation apps M Ns := (fold_left app Ns M). + +Lemma subst_apps s k t ts : subst (apps t ts) k s = apps (subst t k s) (map (fun u => subst u k s) ts). +Proof. + elim: ts t; first done. + move=> t' ts IH t /=. by rewrite IH. +Qed. + +Lemma subst_lams n s k t : subst (lams n s) k t = lams n (subst s (n + k) t). +Proof. + elim: n k; first done. + move=> n IH k /=. by rewrite IH Nat.add_succ_r. +Qed. + +Fixpoint substs k ts t := + match t with + | var x => nth x (map var (seq 0 k) ++ ts) (var x) + | app s t => app (substs k ts s) (substs k ts t) + | lam s => lam (substs (S k) ts s) + end. + +Lemma substs_apps k ts s ss : substs k ts (apps s ss) = apps (substs k ts s) (map (substs k ts) ss). +Proof. + elim: ss s; first done. + move=> s' ss IH s /=. by rewrite IH. +Qed. + +Lemma substs_nil k t : substs k [] t = t. +Proof. + elim: t k. + - move=> x k /=. rewrite app_nil_r map_nth. + have [?|?] : x < k \/ x >= k by lia. + + by rewrite seq_nth. + + by rewrite nth_overflow ?length_seq. + - move=> ? IH1 ? IH2 ? /=. by rewrite IH1 IH2. + - move=> ? IH ? /=. by rewrite IH. +Qed. + +Lemma substs_closed k ts t : closed t -> substs k ts t = t. +Proof. + move=> /L_facts.closed_dcl. + have : 0 <= k by lia. + move: (0)=> n + H. elim: H k. + - move=> > ? > ? /=. rewrite app_nth1. + + rewrite length_map length_seq. lia. + + by rewrite map_nth seq_nth; [lia|]. + - move=> > ? IH1 ? IH2 * /=. + by rewrite IH1 ?IH2. + - move=> > ? IH * /=. by rewrite IH; [lia|]. +Qed. + +Lemma substs_subst k t ts s : closed t -> Forall closed ts -> + substs k ts (subst s (k + length ts) t) = substs k (ts ++ [t]) s. +Proof. + move=> Ht Hts. elim: s k. + - move=> x k /=. + move E: (Nat.eqb x (k + length ts)) => [|]. + + move=> /Nat.eqb_eq in E. subst. + rewrite app_assoc app_nth2 !length_app !length_map !length_seq; [lia|]. + rewrite Nat.sub_diag /=. by apply: substs_closed. + + move=> /Nat.eqb_neq in E. + rewrite /= !app_assoc. + have [?|?] : x < k + length ts \/ x > k + length ts by lia. + * rewrite (app_nth1 _ [t]); last done. + by rewrite length_app length_map length_seq. + * rewrite !nth_overflow; last done. + all: rewrite !length_app length_map length_seq /=; lia. + - move=> ? IH1 ? IH2 ? /=. by rewrite IH1 IH2. + - move=> ? IH ? /=. by rewrite IH. +Qed. + +Lemma eval_lam s t : lam s = t -> eval (lam s) t. +Proof. + move=> <-. by constructor. +Qed. + +Lemma t_steps_app_l s t1 t2 : clos_trans term step t1 t2 -> clos_trans term step (app s t1) (app s t2). +Proof. + elim. + - move=> > ?. apply: t_step. by apply: L_facts.stepAppR. + - move=> *. apply: t_trans; by eassumption. +Qed. + +Lemma t_steps_app_r s1 s2 t : clos_trans term step s1 s2 -> clos_trans term step (app s1 t) (app s2 t). +Proof. + elim. + - move=> > ?. apply: t_step. by apply: L_facts.stepAppL. + - move=> *. apply: t_trans; by eassumption. +Qed. + +Lemma rt_steps_app_l s t1 t2 : clos_refl_trans term step t1 t2 -> clos_refl_trans term step (app s t1) (app s t2). +Proof. + elim. + - move=> > ?. apply: rt_step. by apply: L_facts.stepAppR. + - move=> *. by apply: rt_refl. + - move=> *. apply: rt_trans; by eassumption. +Qed. + +Lemma rt_steps_app_r s1 s2 t : clos_refl_trans term step s1 s2 -> clos_refl_trans term step (app s1 t) (app s2 t). +Proof. + elim. + - move=> > ?. apply: rt_step. by apply: L_facts.stepAppL. + - move=> *. by apply: rt_refl. + - move=> *. apply: rt_trans; by eassumption. +Qed. + +Lemma rt_steps_apps_r s ts t : + clos_refl_trans _ step s t -> clos_refl_trans _ step (apps s ts) (apps t ts). +Proof. + elim: ts s t; first done. + move=> ?? IH ??? /=. apply: IH. + by apply: rt_steps_app_r. +Qed. + +Lemma step_app' s t : eval t t -> step (app (lam s) t) (subst s 0 t). +Proof. + move=> /L_facts.eval_iff [_] [?] ->. by constructor. +Qed. + +Lemma steps_apps_lams n (ts : list term) s : + n = length ts -> + Forall (fun t' => eval t' t') ts -> + Forall closed ts -> + clos_refl_trans _ step (apps (lams n s) ts) (substs 0 (rev ts) s). +Proof. + move=> -> H. elim: H s. + - move=> ? /= *. rewrite substs_nil. by apply: rt_refl. + - move=> t' {}ts H1t' Hts IH s /Forall_cons_iff [H2t'] /[dup] ? /IH {}IH. + move: H1t' => /L_facts.eval_iff [_] [t'' ?]. subst. + rewrite /=. apply: rt_trans. + + apply: rt_steps_apps_r. apply: rt_trans. + { apply: rt_step. by constructor. } + rewrite subst_lams. by apply: rt_refl. + + apply: rt_trans; first by apply IH. + rewrite Nat.add_0_r -length_rev. + rewrite substs_subst; [done|by apply: Forall_rev|]. + by apply: rt_refl. +Qed. + +Lemma eval_rt_steps_subst s t1 t2 : eval t1 t2 -> clos_refl_trans _ step (app (lam s) t1) (subst s 0 t2). +Proof. + move=> /L_facts.eval_iff [/ARS.star_clos_rt_iff ?] [?] ?. subst. + apply: rt_trans. + - apply: rt_steps_app_l. by eassumption. + - apply: rt_step. by constructor. +Qed. + +Lemma eval_rt_steps s t : eval s t -> clos_refl_trans term step s t. +Proof. + move=> /L_facts.eval_iff [?] [?] ?. subst. + by apply /ARS.star_clos_rt_iff. +Qed. + +Lemma eval_rt_steps_eval s t u : eval s t -> clos_refl_trans _ step s u -> eval u t. +Proof. + move=> /L_facts.eval_iff [+] [s'] ?. subst. + move=> + /ARS.star_clos_rt_iff. + move=> /L_facts.confluence /[apply] - [?] [H1 H2]. + apply /L_facts.eval_iff. + have Hs' : L_facts.lambda (lam s') by eexists. + split. + - have := L_facts.lam_terminal Hs'. + move: H1 H2 => []; first done. + by move=> > + _ _ H => /H. + - by eexists. +Qed. + +Lemma rt_steps_eval_eval s t u : clos_refl_trans _ step s u -> eval u t -> eval s t. +Proof. + move=> ? /L_facts.eval_iff [/ARS.star_clos_rt_iff ??]. + apply /L_facts.eval_iff. split; last done. + apply /ARS.star_clos_rt_iff /rt_trans; by eassumption. +Qed. + +Lemma eval_apps_lams n (ts : list term) s t : + n = length ts -> + Forall (fun t' => eval t' t') ts -> + Forall closed ts -> + eval (substs 0 (rev ts) s) t -> + eval (apps (lams n s) ts) t. +Proof. + move=> /steps_apps_lams /[apply] /[apply] H. + apply: rt_steps_eval_eval. by apply: H. +Qed. + +Lemma closed_rt_step {s t} : clos_refl_trans term step s t -> closed s -> closed t. +Proof. + elim; by eauto using L_facts.closed_step. +Qed. + +Lemma steps_stuck_eval s t : closed s -> clos_refl_trans term step s t -> stuck step t -> eval s t. +Proof. + move=> /closed_rt_step Hs /[dup] /Hs H't Hst Ht. + apply /L_facts.eval_iff. split. + - by apply /ARS.star_clos_rt_iff. + - by move: H't => /L_facts.comb_proc_red [[]|[? /Ht]]. +Qed. + +Lemma eval_steps_stuck s t : eval s t -> terminates step s. +Proof. + move=> /L_facts.eval_iff [?] [?] ?. subst. + eexists. split. + - apply /ARS.star_clos_rt_iff. by eassumption. + - move=> ? H. by inversion H. +Qed. diff --git a/theories/LambdaCalculus/Krivine_undec.v b/theories/LambdaCalculus/Krivine_undec.v index d3f88bf82..d416ed7e0 100644 --- a/theories/LambdaCalculus/Krivine_undec.v +++ b/theories/LambdaCalculus/Krivine_undec.v @@ -17,15 +17,13 @@ Require Import Undecidability.LambdaCalculus.Krivine. From Undecidability.LambdaCalculus.Reductions Require wCBNclosed_to_KrivineMclosed_HALT HaltLclosed_to_wCBNclosed. -Require Undecidability.L.Reductions.HaltL_to_HaltLclosed. Require Import Undecidability.L.L_undec. (* Undecidability of Krivine machine halting for closed terms *) Theorem KrivineMclosed_HALT_undec : undecidable KrivineMclosed_HALT. Proof. - apply (undecidability_from_reducibility HaltL_undec). - apply (reduces_transitive HaltL_to_HaltLclosed.reduction). + apply (undecidability_from_reducibility HaltLclosed_undec). apply (reduces_transitive HaltLclosed_to_wCBNclosed.reduction). exact wCBNclosed_to_KrivineMclosed_HALT.reduction. Qed. diff --git a/theories/LambdaCalculus/Lambda_undec.v b/theories/LambdaCalculus/Lambda_undec.v index fe4c51e7d..47b51e5e9 100644 --- a/theories/LambdaCalculus/Lambda_undec.v +++ b/theories/LambdaCalculus/Lambda_undec.v @@ -17,7 +17,6 @@ Require Import Undecidability.LambdaCalculus.Lambda. From Undecidability.LambdaCalculus.Reductions Require HaltLclosed_to_wCBNclosed KrivineMclosed_HALT_to_SNclosed. -Require Undecidability.L.Reductions.HaltL_to_HaltLclosed. Require Import Undecidability.L.L_undec. Require Import Undecidability.LambdaCalculus.Krivine_undec. @@ -25,8 +24,7 @@ Require Import Undecidability.LambdaCalculus.Krivine_undec. (* Undecidability of weak call-by-name leftmost outermost normalization for given closed terms *) Theorem wCBNclosed_undec : undecidable wCBNclosed. Proof. - apply (undecidability_from_reducibility HaltL_undec). - apply (reduces_transitive HaltL_to_HaltLclosed.reduction). + apply (undecidability_from_reducibility HaltLclosed_undec). exact HaltLclosed_to_wCBNclosed.reduction. Qed. diff --git a/theories/LambdaCalculus/Reductions/HaltLclosed_to_wCBNclosed.v b/theories/LambdaCalculus/Reductions/HaltLclosed_to_wCBNclosed.v index 4c02fc8a3..a0d123274 100644 --- a/theories/LambdaCalculus/Reductions/HaltLclosed_to_wCBNclosed.v +++ b/theories/LambdaCalculus/Reductions/HaltLclosed_to_wCBNclosed.v @@ -341,21 +341,19 @@ Qed. End Argument. Require Import Undecidability.Synthetic.Definitions. -Require Undecidability.L.Reductions.HaltL_to_HaltLclosed. -Import HaltL_to_HaltLclosed (HaltLclosed). #[local] Unset Asymmetric Patterns. (* reduction from L halting to weak call-by-name leftmost outermost normalization *) -(* note: currently HaltLclosed is defined in HaltL_to_HaltLclosed *) Theorem reduction : HaltLclosed ⪯ wCBNclosed. Proof. exists (fun '(exist _ s Hs) => exist _ (Argument.colon s (lam (var 0))) (Argument.closed_colon Hs)). move=> [s Hs]. split. - - move=> [t] /= /[dup] [[_ []]] t' ->. - move=> /eval_iff /= /Argument.simulation. + - move=> [t] /= /[dup] /eval_iff [_ []] t' ->. + move=> /= /Argument.simulation. move=> /(_ Hs (lam (var 0))) ?. exists (Argument.cbv_cbn t'). apply: rt_trans; first by eassumption. apply: rt_step. by apply: wCBN_stepSubst. - - move=> [t] /Argument.inverse_simulation. by apply. + - move=> [t] /Argument.inverse_simulation /(_ Hs) [{}t] /eval_iff ?. + by exists t. Qed. diff --git a/theories/LambdaCalculus/Reductions/KrivineMclosed_HALT_to_SNclosed.v b/theories/LambdaCalculus/Reductions/KrivineMclosed_HALT_to_SNclosed.v index a4f11f07c..e1650a636 100644 --- a/theories/LambdaCalculus/Reductions/KrivineMclosed_HALT_to_SNclosed.v +++ b/theories/LambdaCalculus/Reductions/KrivineMclosed_HALT_to_SNclosed.v @@ -15,7 +15,7 @@ Require Undecidability.L.L. From Undecidability.LambdaCalculus Require Import Krivine Lambda Util.Krivine_facts. Require Import Undecidability.LambdaCalculus.Util.term_facts. -Require Import Undecidability.Shared.deterministic_simulation. +Require Import Undecidability.Shared.simulation. Require Import Relations List. Import L (term, var, app, lam). @@ -93,6 +93,11 @@ Proof. move=> /step'_step_det H /step'_step. by apply: H. Qed. +Lemma step'_uc : uniformly_confluent step'. +Proof. + move=> ??? /step'_det /[apply] <-. by left. +Qed. + #[local] Notation I := (lam (var 0)). (* all encodings get I as a final argument to ensure redex uniqueness *) @@ -473,7 +478,7 @@ Proof. move=> [t Ht] /=. split. - move=> ?. apply: step'_step_SN. by apply: halt_cbn_rt_step'. - move=> /SN_terminates_step'. - move=> /(terminates_reflection step'_det Krivine_step_steps' Krivine_step_dec (sync_intro _ _ _)). + move=> /(terminates_reflection step'_uc Krivine_step_steps' Krivine_step_dec (sync_intro _ _ _)). move=> [[[ts' ctx'] t']] []. move=> /Krivine_step_halt_cbn'. apply; [by constructor|]. split; [|done]. diff --git a/theories/MinskyMachines/Reductions/L_computable_to_MMA_computable.v b/theories/MinskyMachines/Reductions/L_computable_to_MMA_computable.v deleted file mode 100644 index 8402c21a6..000000000 --- a/theories/MinskyMachines/Reductions/L_computable_to_MMA_computable.v +++ /dev/null @@ -1,28 +0,0 @@ -(* - Author(s): - Andrej Dudenhefner (1) - Affiliation(s): - (1) TU Dortmund University, Dortmund, Germany -*) - -(* - If a relation R is L_computable then it is MMA_computable. -*) - -From Undecidability Require Import - MinskyMachines.MMA L.L. - -From Undecidability Require Import - MinskyMachines.Reductions.L_computable_closed_to_MMA_computable - L.Util.ClosedLAdmissible. - -Require Import ssreflect ssrbool ssrfun. - -Set Default Goal Selector "!". - -Theorem L_computable_to_MMA_computable {k} (R : Vector.t nat k -> nat -> Prop) : - L_computable R -> MMA_computable R. -Proof. - move=> /L_computable_can_closed. - by apply: L_computable_closed_to_MMA_computable. -Qed. diff --git a/theories/MinskyMachines/Reductions/MM2_HALTING_to_MM2_ZERO_HALTING.v b/theories/MinskyMachines/Reductions/MM2_HALTING_to_MM2_ZERO_HALTING.v index 7934fc39a..53d4944c2 100644 --- a/theories/MinskyMachines/Reductions/MM2_HALTING_to_MM2_ZERO_HALTING.v +++ b/theories/MinskyMachines/Reductions/MM2_HALTING_to_MM2_ZERO_HALTING.v @@ -16,8 +16,8 @@ Require Import List PeanoNat Lia Relations.Relation_Operators Relations.Operator Require Import Undecidability.MinskyMachines.MM2. Require Import Undecidability.MinskyMachines.Util.MM2_facts. -Require Undecidability.Shared.deterministic_simulation. -Module sim := deterministic_simulation. +Require Undecidability.Shared.simulation. +Module sim := simulation. Require Import ssreflect ssrbool ssrfun. @@ -134,7 +134,7 @@ Section MM2_MM2. have Hx'y' : mm2'_reaches (shift_state (1, (a0, b0))) y'. { have [z [/mm2_steps_stop_refl Hyz Hinitz]] := mm2_steps_confluent Hxy' Hinit. by rewrite -(Hyz Hy'). } - have Hsim := sim.terminates_reflection (@mm2_step_det M') mm2_step_sim' (mm2_exists_step_dec M). + have Hsim := sim.terminates_reflection (sim.deterministic_uniformly_confluent _ (@mm2_step_det M')) mm2_step_sim' (mm2_exists_step_dec M). apply: (Hsim _ _ erefl). by exists y'. Qed. diff --git a/theories/MinskyMachines/Reductions/MMA_computable_to_MMA_mon_computable.v b/theories/MinskyMachines/Reductions/MMA_computable_to_MMA_mon_computable.v index 00b20fdc9..881d8220b 100644 --- a/theories/MinskyMachines/Reductions/MMA_computable_to_MMA_mon_computable.v +++ b/theories/MinskyMachines/Reductions/MMA_computable_to_MMA_mon_computable.v @@ -11,19 +11,19 @@ *) From Undecidability Require Import TM.TM. -From Undecidability.MinskyMachines Require Import MM MMA MMA.mma_defs Util.MMA_computable. +From Undecidability.MinskyMachines Require Import MM MMA MMA.mma_defs Util.MMA_computable Util.MMA_facts. From Undecidability.Shared.Libs.DLW Require Import Vec.pos Vec.vec Code.sss. -Require Undecidability.Shared.deterministic_simulation. +Require Undecidability.Shared.simulation. Require Import List PeanoNat Lia Relations. Import ListNotations. Require Import ssreflect. -Module Sim := deterministic_simulation. +Module Sim := simulation. Set Default Goal Selector "!". @@ -96,49 +96,6 @@ Qed. End Facts. Import Facts. -Lemma sss_compute_iff {n P s t} : P // s ->> t <-> clos_refl_trans _ (sss_step (@mma_sss n) P) s t. -Proof. - split. - - case=> k. elim: k s. - { move=> ? /sss_steps_0_inv <-. by apply: rt_refl. } - move=> ? IH ? H. inversion H. - by apply: rt_trans; [apply: rt_step|apply: IH]; eassumption. - - move=> /clos_rt_rt1n_iff. elim. - { move=> ?. exists 0. by constructor. } - move=> > ? _ ?. apply: sss_compute_trans; [|eassumption]. - exists 1. by econstructor; [eassumption|constructor]. -Qed. - -Lemma in_code_step {n s P} : - subcode.in_code (fst s) P -> - exists t, sss_step (@mma_sss n) P s t. -Proof. - move: s P => [i v] [offset P] /= ?. - case E: (nth_error P (i - offset)) => [instr|]; first last. - { move=> /nth_error_None in E. cbn in *. lia. } - have [t Ht] := mma_sss_total_ni instr (i, v). - move: E => /(nth_error_split P) [?] [?] [->] Hi. - eexists t, offset, _, instr, _, v. - split; [done|split; [|eassumption]]. - congr pair. lia. -Qed. - -Lemma out_code_iff {n s P} : subcode.out_code (fst s) P <-> Sim.stuck (sss_step (@mma_sss n) P) s. -Proof. - split. - - move=> /sss_steps_stall H t /in_sss_steps_S H'. - by have /H' /H [] : sss_steps (mma_sss (n:=n)) P 0 t t by apply: in_sss_steps_0. - - have [|] := subcode.in_out_code_dec (fst s) P; [|done]. - move=> /in_code_step [t] ? Hs. exfalso. by apply: (Hs t). -Qed. - -Lemma sss_terminates_iff {n s P} : sss_terminates (@mma_sss n) P s <-> Sim.terminates (sss_step (@mma_sss n) P) s. -Proof. - split. - - move=> [t] [/sss_compute_iff ? /out_code_iff ?]. by exists t. - - move=> [t] [/sss_compute_iff ? /out_code_iff ?]. by exists t. -Qed. - Module MMA_MMA_mon. Section FixedMMA. @@ -405,8 +362,8 @@ Qed. Lemma step1_intro s : (exists t, step1 s t) \/ (Sim.stuck step1 s). Proof. have [|] := subcode.in_out_code_dec (fst s) (1, P). - - move=> /in_code_step ?. by left. - - move=> /out_code_iff ?. by right. + - move=> /(in_code_step (@mma_sss_total_ni num_counters)) ?. by left. + - move=> /(out_code_iff (@mma_sss_total_ni num_counters)) ?. by right. Qed. Lemma simulation v v' w' c m : @@ -439,8 +396,8 @@ Proof. move=> /simulation /[apply] ?. eexists _, _. split; [eassumption|]. rewrite /= length_P' /=. lia. - - move=> v /sss_terminates_iff Hv. apply: H2P. - apply /sss_terminates_iff. move: Hv. - apply /(Sim.terminates_reflection step2_det fstep step1_intro). + - move=> v /(sss_terminates_iff (@mma_sss_total_ni _)) Hv. apply: H2P. + apply /(sss_terminates_iff (@mma_sss_total_ni _)). move: Hv. + apply /(Sim.terminates_reflection (Sim.deterministic_uniformly_confluent _ step2_det) fstep step1_intro). rewrite -vec_append_const. by apply: sync_intro. Qed. diff --git a/theories/MinskyMachines/Reductions/MM_computable_to_MMA_computable.v b/theories/MinskyMachines/Reductions/MM_computable_to_MMA_computable.v new file mode 100644 index 000000000..aea1d1c3c --- /dev/null +++ b/theories/MinskyMachines/Reductions/MM_computable_to_MMA_computable.v @@ -0,0 +1,190 @@ +(* + Author(s): + Andrej Dudenhefner (1) + Affiliation(s): + (1) TU Dortmund University, Dortmund, Germany +*) + +(* + If a relation R is MM_computable then it is MMA_computable +*) + +From Undecidability.MinskyMachines Require Import MM MMA MMA.mma_defs Util.MMA_computable Util.MMA_facts Util.MM_computable MM.mm_defs. +Require Import Undecidability.MinskyMachines.Util.MM_sss. + +From Undecidability.Shared.Libs.DLW + Require Import Vec.pos Vec.vec Code.sss. + +Require Import Undecidability.Shared.simulation. + +Require Import List PeanoNat Lia Relations. +Import ListNotations. + +Require Import ssreflect. + +Set Default Goal Selector "!". + +(* generic auxiliary facts *) +Lemma clos_t_rt_t {A : Type} {R : relation A} (x y z : A) : + clos_trans A R x y -> clos_refl_trans A R y z -> clos_trans A R x z. +Proof. + move=> H /clos_rt_rtn1_iff H'. elim: H' H; by eauto using clos_trans. +Qed. + +Module MM_MMA. + +Section FixedMMA. +Context {num_counters : nat}. +Context {P : list (mm_instr (pos num_counters))}. + +Definition addr (i : nat) := (i * 3) - 2. + +Lemma addr_spec i : addr i = (i * 3) - 2. +Proof. done. Qed. + +Opaque addr. + +Definition enc_instr '(i, instr) : list (mm_instr (pos num_counters)) := + match instr with + | INC X => [INC X; INC X; DEC X (addr (S i))] + | DEC X p => [DEC X (addr (S i)); INC X; DEC X (addr p)] + end. + +Definition P' : list (mm_instr (pos num_counters)) := + concat (map enc_instr (combine (seq 1 (length P)) P)). + +Lemma length_P' : length P' = length P * 3. +Proof. + rewrite /P' length_concat. move: (x in seq x). + elim: (P); first done. + move=> [] > /= IH ?; by rewrite IH. +Qed. + +Lemma P'_spec i {instr l r} : + i - 2 = 0 -> + P = l ++ instr :: r -> + nth_error P' (length l * 3 + i) = nth_error (enc_instr (S (length l), instr)) i. +Proof. + move=> Hi. rewrite /P'=> ->. + suff: forall k, nth_error + (concat (map enc_instr (combine (seq k (length (l ++ instr :: r))) (l ++ instr :: r)))) (length l * 3 + i) = + nth_error (enc_instr (k + (length l), instr)) i by apply. + elim: l. + - move=> k. rewrite /= Nat.add_0_r. + by move: i Hi instr => [|[|[|?]]] ? [] /=; try lia. + - move=> [] > IH ? /=. + + rewrite IH. congr nth_error. by rewrite !(Nat.add_succ_r _ (length _)). + + rewrite IH. congr nth_error. by rewrite !(Nat.add_succ_r _ (length _)). +Qed. + +#[local] Arguments firstn_skipn_middle {A n l x}. + +Lemma simulation_sss_step st st' : + sss_step (mm_sss (n:=num_counters)) (1, P) st st' -> + clos_trans _ (sss_step (mma_sss (n:=num_counters)) (1, P')) (addr (fst st), snd st) (addr (fst st'), snd st'). +Proof. + move: st'=> [i' v'] [offset] [l] [[]] x > [r] [v] [[<- HP]] [->]. + - (* INC *) + move=> /mm_sss_INC_inv [-> ->] /=. + apply: t_trans. + { apply: t_step. + rewrite -(firstn_skipn_middle (P'_spec 0 eq_refl HP)). apply: in_sss_step. + - rewrite /= addr_spec length_firstn length_P' HP length_app /=. lia. + - by apply: in_mma_sss_inc. } + apply: t_trans. + { apply: t_step. rewrite -(firstn_skipn_middle (P'_spec 1 eq_refl HP)). apply: in_sss_step. + - rewrite /= addr_spec length_firstn length_P' HP length_app /=. lia. + - by apply: in_mma_sss_inc. } + apply: clos_t_rt_t. + { apply: t_step. rewrite -(firstn_skipn_middle (P'_spec 2 eq_refl HP)). apply: in_sss_step. + - rewrite /= addr_spec length_firstn length_P' HP length_app /=. lia. + - apply: in_mma_sss_dec_1. by rewrite vec_change_eq. } + rewrite !vec_change_idem vec_change_eq; first done. + by apply: rt_refl. + - (* DEC *) + move E: (vec_pos v x) => [|?]. + + move=> /mm_sss_DEC0_inv => /(_ E) [-> ->] /=. + apply: t_trans. + { apply: t_step. rewrite -(firstn_skipn_middle (P'_spec 0 eq_refl HP)). apply: in_sss_step. + - rewrite /= addr_spec length_firstn length_P' HP length_app /=. lia. + - by apply: in_mma_sss_dec_0. } + apply: t_trans. + { apply: t_step. rewrite -(firstn_skipn_middle (P'_spec 1 eq_refl HP)). apply: in_sss_step. + - rewrite /= addr_spec length_firstn length_P' HP length_app /=. lia. + - by apply: in_mma_sss_inc. } + apply: clos_t_rt_t. + { apply: t_step. rewrite -(firstn_skipn_middle (P'_spec 2 eq_refl HP)). apply: in_sss_step. + - rewrite /= addr_spec length_firstn length_P' HP length_app /=. lia. + - apply: in_mma_sss_dec_1. by rewrite vec_change_eq. } + rewrite !vec_change_idem vec_change_same. by apply: rt_refl. + + move=> /mm_sss_DEC1_inv => /(_ _ E) [-> ->] /=. + apply: clos_t_rt_t. + { apply: t_step. rewrite -(firstn_skipn_middle (P'_spec 0 eq_refl HP)). apply: in_sss_step. + - rewrite /= addr_spec length_firstn length_P' HP length_app /=. lia. + - apply: in_mma_sss_dec_1. by eassumption. } + by apply: rt_refl. +Qed. + +Definition sync : nat * Vector.t nat num_counters -> nat * Vector.t nat num_counters -> Prop := + fun s s' => s' = (addr (fst s), snd s). + +#[local] Notation step1 := (sss_step (@mm_sss num_counters) (1, P)). +#[local] Notation step2 := (sss_step (@mma_sss num_counters) (1, P')). + +Fact mm_sss_total_ni {n : nat} (ii : mm_instr (pos n)) (s : MM.mm_state n) : + exists t : MM.mm_state n, mm_sss ii s t. +Proof. + have [t ?] := mm_sss_total ii s. by exists t. +Qed. + +Lemma fstep s t s' : step1 s t -> sync s s' -> + exists t', clos_trans _ step2 s' t' /\ sync t t'. +Proof. + move=> /simulation_sss_step ? ->. + eexists. by split; [eassumption|]. +Qed. + +Lemma step2_det s' t1' t2' : + sss_step (@mma_sss _) (1, P') s' t1' -> + sss_step (@mma_sss _) (1, P') s' t2' -> t1' = t2'. +Proof. + apply: sss_step_fun. by apply: mma_sss_fun. +Qed. + +Lemma step1_intro s : (exists t, step1 s t) \/ (stuck step1 s). +Proof. + have [|] := subcode.in_out_code_dec (fst s) (1, P). + - move=> /(in_code_step mm_sss_total_ni) ?. by left. + - move=> /(out_code_iff mm_sss_total_ni) ?. by right. +Qed. + +Lemma simulation v v' c : + sss_compute (mm_sss (n:= num_counters)) (1, P) (1, v) (c, v') -> + c < 1 \/ S (length P) <= c -> + sss_compute (mma_sss (n:= num_counters)) (1, P') (addr 1, v) (addr c, v'). +Proof. + move=> /sss_compute_iff. + move=> /(clos_refl_trans_transport fstep) => /(_ _ eq_refl). + move=> [t'] [->] ??. + by apply /sss_compute_iff. +Qed. + +End FixedMMA. +End MM_MMA. + +Theorem MM_computable_to_MMA_computable k (R : Vector.t nat k -> nat -> Prop) : + MM_computable R -> MMA_computable R. +Proof. + move=> /MM_computable_iff [k'] [P] [H1P H2P]. + apply /MMA_computable_iff. + exists k', (@MM_MMA.P' _ P). split. + - move=> v m /H1P [c] [v'] /=. + move=> /[dup] /eval_to_sss_compute + /eval_to_sss_out_code. + move=> /= + /[dup] Hc => /MM_MMA.simulation /[apply] ?. + eexists _, _. split; [eassumption|]. + rewrite /= MM_MMA.length_P' MM_MMA.addr_spec. + move: Hc => /=. lia. + - move=> v /(sss_terminates_iff (@mma_sss_total_ni _)) Hv. apply: H2P. + apply /(sss_terminates_iff MM_MMA.mm_sss_total_ni). move: Hv. + by apply /(terminates_reflection (deterministic_uniformly_confluent _ MM_MMA.step2_det) MM_MMA.fstep MM_MMA.step1_intro). +Qed. diff --git a/theories/MinskyMachines/Util/MMA_facts.v b/theories/MinskyMachines/Util/MMA_facts.v new file mode 100644 index 000000000..c62742503 --- /dev/null +++ b/theories/MinskyMachines/Util/MMA_facts.v @@ -0,0 +1,75 @@ +From Undecidability Require Import TM.TM. +From Undecidability.MinskyMachines Require Import MMA MMA.mma_defs Util.MMA_computable. + +From Undecidability.Shared.Libs.DLW + Require Import Vec.pos Vec.vec Code.sss. + +Require Undecidability.Shared.simulation. + +Require Import List PeanoNat Lia Relations. +Import ListNotations. + +Require Import ssreflect. + +Set Default Goal Selector "!". + +#[local] Notation "P // s ~~> t" := (sss_output (@mma_sss _) P s t). +#[local] Notation "P // s ->> t" := (sss_compute (@mma_sss _) P s t). + +Section Step. + Context {instr data : Set} {step : instr -> nat * data -> nat * data -> Prop}. + Context (Hstep : forall (ii : instr) (s : nat * data), exists t, step ii s t). + +Lemma sss_compute_iff {P s t} : + sss_compute step P s t <-> clos_refl_trans _ (sss_step step P) s t. +Proof. + split. + - case=> k. elim: k s. + { move=> ? /sss_steps_0_inv <-. by apply: rt_refl. } + move=> ? IH ? H. inversion H. + by apply: rt_trans; [apply: rt_step|apply: IH]; eassumption. + - move=> /clos_rt_rt1n_iff. elim. + { move=> ?. exists 0. by constructor. } + move=> > ? _ ?. apply: sss_compute_trans; [|eassumption]. + exists 1. by econstructor; [eassumption|constructor]. +Qed. + +Lemma in_code_step {s P} : + subcode.in_code (fst s) P -> + exists t, sss_step step P s t. +Proof using Hstep. + move: s P => [i v] [offset P] /= ?. + case E: (nth_error P (i - offset)) => [ii|]; first last. + { move=> /nth_error_None in E. cbn in *. lia. } + have [t Ht] := Hstep ii (i, v). + move: E => /(nth_error_split P) [?] [?] [->] Hi. + eexists t, offset, _, ii, _, v. + split; [done|split; [|eassumption]]. + congr pair. lia. +Qed. + +Lemma out_code_iff {s P} : subcode.out_code (fst s) P <-> simulation.stuck (sss_step step P) s. +Proof using Hstep. + split. + - move=> /sss_steps_stall H t /in_sss_steps_S H'. + by have /H' /H [] : sss_steps step P 0 t t by apply: in_sss_steps_0. + - have [|] := subcode.in_out_code_dec (fst s) P; [|done]. + move=> /in_code_step [t] ? Hs. exfalso. by apply: (Hs t). +Qed. + +Lemma sss_step_or_stuck p i P : + (exists q, sss_step step (i, P) p q) \/ simulation.stuck (sss_step step (i, P)) p. +Proof using Hstep. + have [|] := subcode.in_out_code_dec (fst p) (i, P). + - move=> /in_code_step ?. by left. + - move=> /out_code_iff ?. by right. +Qed. + +Lemma sss_terminates_iff {s P} : sss_terminates step P s <-> simulation.terminates (sss_step step P) s. +Proof using Hstep. + split. + - move=> [t] [/sss_compute_iff ? /out_code_iff ?]. by exists t. + - move=> [t] [/sss_compute_iff ? /out_code_iff ?]. by exists t. +Qed. + +End Step. diff --git a/theories/MinskyMachines/Util/MM_computable.v b/theories/MinskyMachines/Util/MM_computable.v index 361e85c92..bde3aed5c 100644 --- a/theories/MinskyMachines/Util/MM_computable.v +++ b/theories/MinskyMachines/Util/MM_computable.v @@ -8,19 +8,25 @@ Lemma MM_computable_iff {k} (R : Vector.t nat k -> nat -> Prop) : (exists n : nat, exists P : list (mm_instr (Fin.t (1 + k + n))), (forall v m, R v m -> exists c v', @MM.eval (1 + k + n) (1, P) (1, (0 :: v) ++ Vector.const 0 n) (c, m :: v')) /\ (forall v, sss.sss_terminates (@mm_sss _) (1, P) (1, (0 :: v) ++ Vector.const 0 n) -> exists m, R v m)) - -> MM_computable R. + <-> MM_computable R. Proof. - intros (n & P & H1 & H2). - exists n, P. intros v m. split. - - intros H % H1. eauto. - - intros (c & v' & H). - pose proof (H' := H). - edestruct H2 as [m' Hm']. - 1:{ eexists. eapply eval_iff. eauto. } - enough (m' = m) as -> by eauto. - eapply H1 in Hm' as (c' & v'' & H''). fold plus in *. - eapply eval_iff in H', H''. - destruct H' as [H1' H2']. destruct H'' as [H1'' H2'']. - eapply sss.sss_compute_fun in H1'; eauto. congruence. - eapply mm_sss_fun. + split. + - intros (n & P & H1 & H2). + exists n, P. intros v m. split. + + intros H % H1. eauto. + + intros (c & v' & H). + pose proof (H' := H). + edestruct H2 as [m' Hm']. + 1:{ eexists. eapply eval_iff. eauto. } + enough (m' = m) as -> by eauto. + eapply H1 in Hm' as (c' & v'' & H''). fold plus in *. + eapply eval_iff in H', H''. + destruct H' as [H1' H2']. destruct H'' as [H1'' H2'']. + eapply sss.sss_compute_fun in H1'; eauto. congruence. + eapply mm_sss_fun. + - intros [n [P HP]]. exists n, P. split. + + now intros ???%HP. + + intros v [[c' v'] H'P]. rewrite (Vector.eta v') in H'P. + exists (Vector.hd v'). apply HP. do 2 eexists. + apply sss_output_to_eval. eassumption. Qed. diff --git a/theories/Shared/deterministic_simulation.v b/theories/Shared/simulation.v similarity index 75% rename from theories/Shared/deterministic_simulation.v rename to theories/Shared/simulation.v index 57e01f7aa..19d65bb11 100644 --- a/theories/Shared/deterministic_simulation.v +++ b/theories/Shared/simulation.v @@ -3,7 +3,7 @@ step1 : X -> X -> Prop step2 : Y -> Y -> Prop such that - - step2 is deterministic (step2_det) + - step2 is uniformly confluent (step2_uc) - one step in step1 is simulated by a positive number of steps in step2 (fstep) - halting in step1 is simulated by termination in step2 (fstop) - step1 admits existential successor decision (step1_intro) @@ -25,7 +25,14 @@ Section Preliminaries. (* eventual termination *) Definition terminates s := exists t, clos_refl_trans X step s t /\ stuck t. - Fact terminates_extend {s t} : clos_refl_trans X step s t -> terminates t -> terminates s. + Definition uniformly_confluent := forall s t1 t2, step s t1 -> step s t2 -> t1 = t2 \/ exists t3, step t1 t3 /\ step t2 t3. + + Lemma deterministic_uniformly_confluent : (forall s t1 t2, step s t1 -> step s t2 -> t1 = t2) -> uniformly_confluent. + Proof. + intros H s t1 t2 H1 H2. left. now apply (H s t1 t2). + Qed. + + Lemma terminates_extend {s t} : clos_refl_trans X step s t -> terminates t -> terminates s. Proof. intros ? [u [??]]. exists u. eauto using clos_refl_trans. Qed. @@ -37,7 +44,7 @@ Section Preliminaries. End Preliminaries. -Section Deterministic_simulation. +Section Simulation. (* configuration spaces *) Context {X Y : Type}. @@ -48,9 +55,8 @@ Section Deterministic_simulation. (* configuration encoding *) Context {sync : X -> Y -> Prop}. - (* determinism of step2 *) - Context (step2_det : forall s' t1' t2', step2 s' t1' -> step2 s' t2' -> t1' = t2'). - Arguments step2_det {s' t1' t2'}. + (* uniform confluence of step2 *) + Context (step2_uc : uniformly_confluent step2). (* step simulation wrt. encoding *) Context (fstep : forall s t s', step1 s t -> sync s s' -> @@ -89,19 +95,25 @@ Section Deterministic_simulation. (* terminating configurations are accessible note that (Acc R^-1 s) means s is strongly normalizing for R in a constructive setting *) - Lemma terminating_Acc {s} : terminates step2 s -> Acc (fun y x => step2 x y) s. - Proof using step2_det. - intros [t [Hst%clos_rt_rt1n Ht]]. - induction Hst as [|??? Hxy Hyz IH]; constructor. - - now intros y ?%Ht. - - intros y' Hxy'. rewrite <- (step2_det Hxy Hxy'). now apply IH. + Lemma terminating_Acc {s'} : terminates step2 s' -> Acc (fun y x => step2 x y) s'. + Proof using step2_uc. + intros [t' [Hs't'%clos_rt_rt1n Ht']]. + induction Hs't' as [|??? Hxy Hyz IH]; constructor. + - now intros y ?%Ht'. + - intros y' Hxy'. specialize (IH Ht'). + clear z Hyz Ht'. revert x y' Hxy Hxy'. + induction IH as [z IH1 IH2]. + intros x y' Hxz Hxy'. constructor. intros v ?. + destruct (step2_uc _ _ _ Hxz Hxy') as [?|[w [Hzw ?]]]. + + subst. now apply IH1. + + eapply (IH2 _ Hzw); eassumption. Qed. (* reflection of termination by well-founded induction on transitive closure using Lemma Acc_clos_trans A R x : Acc R x -> Acc (clos_trans A R) x from the Coq standard library *) Lemma terminates_reflection {s s'} : sync s s' -> terminates step2 s' -> terminates step1 s. - Proof using step2_det step1_intro fstep. + Proof using step2_uc step1_intro fstep. intros Hss' Hs'%terminating_Acc%(Acc_clos_trans Y). revert s Hss'. induction Hs' as [s' _ IH]. intros s. destruct (step1_intro s) as [[t Hst] | Hs]. @@ -112,4 +124,4 @@ Section Deterministic_simulation. - intros _. exists s. eauto using clos_refl_trans. Qed. -End Deterministic_simulation. +End Simulation. diff --git a/theories/Synthetic/Models_Equivalent.v b/theories/Synthetic/Models_Equivalent.v index 15d3d4866..a5191f9a6 100644 --- a/theories/Synthetic/Models_Equivalent.v +++ b/theories/Synthetic/Models_Equivalent.v @@ -16,9 +16,11 @@ From Undecidability Require Import Diophantine Diophantine_to_MuRec_computable MuRec_computable_to_L_computable - L_computable_to_TM_computable - L_computable_to_MMA_computable - MMA_computable_to_TM_computable. + L_computable_closed_to_MMA_computable + MMA_computable_to_TM_computable + MMA_computable_to_L_computable_closed + MM_computable_to_MMA_computable + ClosedLAdmissible. Theorem equivalence {k} (R : Vector.t nat k -> nat -> Prop) : (TM_computable R -> BSM_computable R) /\ @@ -27,8 +29,11 @@ Theorem equivalence {k} (R : Vector.t nat k -> nat -> Prop) : (FRACTRAN_computable R -> Diophantine' R /\ functional R) /\ (Diophantine' R /\ functional R -> MuRec_computable R) /\ (MuRec_computable R -> L_computable R) /\ - (L_computable R -> MMA_computable R) /\ - (MMA_computable R -> TM_computable R). + (L_computable_closed R -> MMA_computable R) /\ + (MMA_computable R -> TM_computable R) /\ + (MMA_computable R -> L_computable_closed R) /\ + (MM_computable R -> MMA_computable R) /\ + (L_computable R -> L_computable_closed R). Proof. repeat split. - apply TM_computable_to_BSM_computable. @@ -38,6 +43,9 @@ Proof. - intros ? ? ? ? ?. eapply FRACTRAN_computable.FRACTRAN_computable_functional; eauto. - intros []. eapply Diophantine_to_MuRec_computable; eauto. - apply MuRec_computable_to_L_computable. - - apply L_computable_to_MMA_computable. + - apply L_computable_closed_to_MMA_computable. - apply MMA_computable_to_TM_computable. + - apply MMA_computable_to_L_computable_closed. + - apply MM_computable_to_MMA_computable. + - apply L_computable_can_closed. Qed. diff --git a/theories/TM/Reductions/HaltL_to_HaltTM_5.v b/theories/TM/Reductions/HaltLclosed_to_HaltTM_5.v similarity index 82% rename from theories/TM/Reductions/HaltL_to_HaltTM_5.v rename to theories/TM/Reductions/HaltLclosed_to_HaltTM_5.v index 94fbf457b..e7553f7cb 100644 --- a/theories/TM/Reductions/HaltL_to_HaltTM_5.v +++ b/theories/TM/Reductions/HaltLclosed_to_HaltTM_5.v @@ -2,15 +2,13 @@ From Undecidability Require Import L.L TM.TM Synthetic.Definitions Synthetic.ReducibilityFacts. From Undecidability Require - L.Reductions.HaltL_to_HaltLclosed LambdaCalculus.Reductions.HaltLclosed_to_wCBNclosed LambdaCalculus.Reductions.wCBNclosed_to_KrivineMclosed_HALT MinskyMachines.Reductions.KrivineMclosed_HALT_to_MMA_HALTING TM.Reductions.MMA_HALTING_n_to_HaltTM_n. -Lemma reduction : HaltL ⪯ HaltTM 5. +Lemma reduction : HaltLclosed ⪯ HaltTM 5. Proof. - apply (reduces_transitive HaltL_to_HaltLclosed.reduction). apply (reduces_transitive HaltLclosed_to_wCBNclosed.reduction). apply (reduces_transitive wCBNclosed_to_KrivineMclosed_HALT.reduction). apply (reduces_transitive KrivineMclosed_HALT_to_MMA_HALTING.reduction). diff --git a/theories/TM/Reductions/L_computable_to_TM_computable.v b/theories/TM/Reductions/L_computable_to_TM_computable.v deleted file mode 100644 index e20116f7f..000000000 --- a/theories/TM/Reductions/L_computable_to_TM_computable.v +++ /dev/null @@ -1,15 +0,0 @@ -From Undecidability Require Import - MinskyMachines.Reductions.L_computable_to_MMA_computable - MinskyMachines.Reductions.MMA_computable_to_MMA_mon_computable - TM.Reductions.MMA_mon_computable_to_TM_computable - L.L TM.TM. - -Lemma L_computable_to_TM_computable k (R : Vector.t nat k -> nat -> Prop) : - L_computable R -> TM_computable R. -Proof. - intros H. - apply MMA_mon_computable_to_TM_computable. - apply MMA_computable_to_MMA_mon_computable. - apply L_computable_to_MMA_computable. - exact H. -Qed. diff --git a/theories/TM/Reductions/MMA_mon_computable_to_TM_computable.v b/theories/TM/Reductions/MMA_mon_computable_to_TM_computable.v index f68350f8c..6babbf652 100644 --- a/theories/TM/Reductions/MMA_mon_computable_to_TM_computable.v +++ b/theories/TM/Reductions/MMA_mon_computable_to_TM_computable.v @@ -15,7 +15,7 @@ From Undecidability.TM Require Import TM. From Undecidability.TM Require Util.TM_facts Util.TM_computable. From Undecidability.MinskyMachines Require Import - MM MMA.mma_defs Reductions.MMA_computable_to_MMA_mon_computable. + MM MMA.mma_defs Util.MMA_facts Reductions.MMA_computable_to_MMA_mon_computable. From Undecidability.Shared.Libs.DLW Require Import Vec.pos Vec.vec Code.sss Code.subcode. @@ -24,8 +24,8 @@ Require Import Undecidability.Shared.Libs.PSL.FiniteTypes.FinTypesDef. From Undecidability.Shared.Libs.PSL Require Import CompoundFinTypes. Require Import Undecidability.Shared.Libs.PSL.EqDec. -From Undecidability Require Shared.deterministic_simulation. -Module Sim := deterministic_simulation. +From Undecidability Require Shared.simulation. +Module Sim := simulation. Require Import List Lia PeanoNat Compare_dec Relations. Import ListNotations. @@ -374,8 +374,8 @@ Qed. Lemma step1_intro s : (exists t, step1 s t) \/ (Sim.stuck step1 s). Proof. have [|] := subcode.in_out_code_dec (fst s) (1, M). - - move=> /in_code_step ?. by left. - - move=> /out_code_iff ?. by right. + - move=> /(in_code_step (@mma_sss_total_ni _)) ?. by left. + - move=> /(out_code_iff (@mma_sss_total_ni _)) ?. by right. Qed. Lemma halt'_terminates s' : halt' (TM_facts.cstate s') = true -> Sim.terminates step2 s'. @@ -489,8 +489,8 @@ Proof. + move: Hst' => /syncE. rewrite (Vector.eta b's) /=. by move=> [_ []]. - move=> v q ts /TM_facts.TM_eval_iff [n HPn]. - apply: H3M. apply /sss_terminates_iff. - apply /(Sim.terminates_reflection (step2_det M) (fstep M H1M) (step1_intro M) sync_init). + apply: H3M. apply /(sss_terminates_iff (@mma_sss_total_ni _)). + apply /(Sim.terminates_reflection (Sim.deterministic_uniformly_confluent _ (step2_det M)) (fstep M H1M) (step1_intro M) sync_init). move: n HPn => [|n]. { done. } rewrite /= P_init. by apply: terminates2I. Qed. diff --git a/theories/_CoqProject b/theories/_CoqProject index 2eae7a83c..8de4888b9 100644 --- a/theories/_CoqProject +++ b/theories/_CoqProject @@ -151,10 +151,7 @@ Shared/Libs/PSL/FiniteTypes/CompoundFinTypes.v Shared/Libs/PSL/FiniteTypes/DepPairs.v Shared/Libs/PSL/FiniteTypes/VectorFin.v -Shared/deterministic_simulation.v - -L/Util/NaryApp.v -L/Util/ClosedLAdmissible.v +Shared/simulation.v PCP/Util/Facts.v PCP/Util/PCP_facts.v @@ -330,6 +327,7 @@ MinskyMachines/ndMM2_undec.v MinskyMachines/Util/MM_sss.v MinskyMachines/Util/MM_computable.v MinskyMachines/Util/MM2_facts.v +MinskyMachines/Util/MMA_facts.v MinskyMachines/Util/MMA_pairing.v MinskyMachines/Util/MMA_computable.v @@ -351,8 +349,8 @@ MinskyMachines/Reductions/SBTM_to_MMA2_HALTING.v MinskyMachines/Reductions/BSM_computable_to_MM_computable.v MinskyMachines/Reductions/MM2_HALTING_to_MM2_ZERO_HALTING.v MinskyMachines/Reductions/L_computable_closed_to_MMA_computable.v -MinskyMachines/Reductions/L_computable_to_MMA_computable.v MinskyMachines/Reductions/MMA_computable_to_MMA_mon_computable.v +MinskyMachines/Reductions/MM_computable_to_MMA_computable.v MinskyMachines/Deciders/MPM2_HALT_dec.v MinskyMachines/Deciders/MM_2_HALTING_dec.v @@ -500,8 +498,7 @@ TM/Code/Code.v TM/Single/EncodeTapes.v TM/Single/StepTM.v -TM/Reductions/HaltL_to_HaltTM_5.v -TM/Reductions/L_computable_to_TM_computable.v +TM/Reductions/HaltLclosed_to_HaltTM_5.v TM/Reductions/MMA_mon_computable_to_TM_computable.v TM/Reductions/MMA_computable_to_TM_computable.v @@ -521,14 +518,27 @@ L/Enumerators/term_enum.v L/Prelim/ARS.v L/Util/L_facts.v +L/Util/term_facts.v -L/Tactics/Computable.v +L/Util/NaryApp.v +L/Util/ClosedLAdmissible.v -L/Tactics/LTactics.v +L/Reductions/MuRec_computable_to_L_computable.v +L/Reductions/MMA_HALTING_to_HaltLclosed.v +L/Reductions/MMA_computable_to_L_computable_closed.v + +L/Computability/Seval.v +L/AbstractMachines/wCBV.v + +L/Enumerators/HaltL_enum.v +L/L_enum.v +#extraction framework + +L/Tactics/Computable.v +L/Tactics/LTactics.v L/Tactics/Extract.v L/Tactics/GenEncode.v - L/Tactics/Lbeta_nonrefl.v L/Tactics/Lproc.v L/Tactics/Lbeta.v @@ -536,7 +546,6 @@ L/Tactics/Reflection.v L/Tactics/LClos.v L/Tactics/Lrewrite.v L/Tactics/Lsimpl.v - L/Tactics/ComputableTactics.v L/Datatypes/LUnit.v @@ -571,12 +580,9 @@ L/TM/TMinL/TMinL_extract.v L/TM/TapeFuns.v L/Reductions/TM_to_L.v L/Reductions/H10_to_L.v +L/Reductions/PCPb_to_HaltL.v L/Reductions/MuRec/MuRec_extract.v L/Reductions/HaltMuRec_to_HaltL.v -L/Reductions/HaltL_to_HaltLclosed.v -L/Reductions/MuRec_computable_to_L_computable.v - -L/AbstractMachines/wCBV.v L/Computability/Acceptability.v L/Computability/Computability.v @@ -584,14 +590,10 @@ L/Computability/Decidability.v L/Computability/Fixpoints.v L/Computability/MuRec.v L/Computability/Por.v -L/Computability/Seval.v L/Computability/Synthetic.v L/Computability/Scott.v L/Computability/Rice.v -L/Enumerators/HaltL_enum.v -L/L_enum.v - HOU/std/tactics.v HOU/std/misc.v HOU/std/decidable.v @@ -820,7 +822,6 @@ LambdaCalculus/Reductions/KrivineMclosed_HALT_to_SNclosed.v H10/Reductions/FRACTRAN_computable_to_Diophantine.v H10/Util/Diophantine.v -L/Reductions/PCPb_to_HaltL.v TM/KOSBTM/HaltKOSBTM_to_HaltBSM.v TM/KOSBTM/HaltTM_1_to_HaltKOSBTM.v