Add Intersection Type related problems

README.md

@@ -63,7 +63,7 @@ Target problems are very expressive and thus work well as targets for reduction,
 - Halting problem for Binary Stack Machines (`BSM_HALTING` in [`StackMachines/BSM.v`](theories/StackMachines/BSM.v))
 - Halting problems for Minsky machines (`MM_HALTING` and `MMA_HALTING n` in [`MinskyMachines/MM.v`](theories/MinskyMachines/MM.v))
 - Halting problem for partial recursive functions (`MUREC_HALTING` in [`MuRec/recalg.v`](theories/MuRec/recalg.v))
-- Halting problem for the weak call-by-name lambda-calculus (`wCBN` in [`LambdaCalculus/wCBN.v`](theories/LambdaCalculus/wCBN.v))
+- Halting problem for the weak call-by-name lambda-calculus (`wCBNclosed` in [`LambdaCalculus/Lambda.v`](theories/LambdaCalculus/Lambda.v))
 
 An equivalence proof that most of the mentioned models of computation compute the same `n`-ary functional relations over natural numbers is available in [`Models_Equivalent.v`](theories/Synthetic/Models_Equivalent.v).
 
@@ -96,8 +96,10 @@ An equivalence proof that most of the mentioned models of computation compute th
 - Finite multiset constraint solvability (`FMsetC_SAT` in [`SetConstraints/FMsetC.v`](theories/SetConstraints/FMsetC.v))
 - Uniform boundedness of deterministic, length-preserving stack machines (`SMNdl_UB` in [`StackMachines/SMN.v`](theories/StackMachines/SMN.v))
 - Semi-unification (`SemiU` in [`SemiUnification/SemiU.v`](theories/SemiUnification/SemiU.v))
-- System F Inhabitation (`SysF_INH` in [`SystemF/SysF.v`](theories/SystemF/SysF.v)), System F Typability (`SysF_TYP` in [`SystemF/SysF.v`](theories/SystemF/SysF.v)), System F Type Checking (`SysF_TC` in [`SystemF/SysF.v`](theories/SystemF/SysF.v))
 - Halting problem for Krivine machines (`KrivineM_HALT` in [`LambdaCalculus/Krivine.v`](theories/LambdaCalculus/Krivine.v))
+- Strong normalization wrt. beta-reduction in the lambda-calculus (`SNclosed` in [`LambdaCalculus/Lambda.v`](theories/LambdaCalculus/Lambda.v))
+- System F Inhabitation (`SysF_INH` in [`SystemF/SysF.v`](theories/SystemF/SysF.v)), System F Typability (`SysF_TYP` in [`SystemF/SysF.v`](theories/SystemF/SysF.v)), System F Type Checking (`SysF_TC` in [`SystemF/SysF.v`](theories/SystemF/SysF.v))
+- Intersection Type Inhabitation (`CD_INH` in [`IntersectionTypes/CD.v`](theories/IntersectionTypes/CD.v)), Intersection Type Typability (`CD_TYP` in [`IntersectionTypes/CD.v`](theories/IntersectionTypes/CD.v)), Intersection Type Type Checking (`CD_TC` in [`IntersectionTypes/CD.v`](theories/IntersectionTypes/CD.v))
 
 #### Decidable Problems
 

theories/IntersectionTypes/CD.v

@@ -0,0 +1,57 @@
+(*
+  Author(s):
+    Andrej Dudenhefner (1)
+  Affiliation(s):
+    (1) TU Dortmund University, Dortmund, Germany
+*)
+
+(*
+  Problem(s):
+    Intersection Type Type Checking  (CD_TC)
+    Intersection Type Typability (CD_TYP)
+    Intersection Type Inhabitation (CD_INH)
+
+  Literature:
+    [1] Coppo, Mario, and Mariangiola Dezani-Ciancaglini.
+        "An extension of the basic functionality theory for the lambda-calculus."
+        Notre Dame journal of formal logic 21.4 (1980): 685-693.
+*)
+
+Require Undecidability.L.L.
+Require Import List.
+Import L (term, var, app, lam).
+
+(* strict types are of shape: a | (s1 /\ s2 /\ .. /\ sn -> t) *)
+Inductive sty : Type :=
+  | atom : nat -> sty
+  | arr : sty -> list sty -> sty -> sty.
+
+(* a type is a (non-empty) list of strict types *)
+Notation ty := (sty * list sty)%type.
+
+(* Coppo-Dezani Intersection Type System *)
+Inductive type_assignment (Gamma : list ty) : term -> sty -> Prop :=
+  | type_assignment_var x s phi t :
+      nth_error Gamma x = Some (s, phi) ->
+      In t (s::phi) ->
+      type_assignment Gamma (var x) t
+  | type_assignment_app M N s phi t :
+      type_assignment Gamma M (arr s phi t) ->
+      type_assignment Gamma N s ->
+      Forall (type_assignment Gamma N) phi ->
+      type_assignment Gamma (app M N) t
+  | type_assignment_arr M s phi t :
+      type_assignment ((s, phi) :: Gamma) M t ->
+      type_assignment Gamma (lam M) (arr s phi t).
+
+(* Intersection Type Type Checking *)
+Definition CD_TC : (list ty) * term * sty -> Prop :=
+  fun '(Gamma, M, t) => type_assignment Gamma M t.
+
+(* Intersection Type Typability *)
+Definition CD_TYP : term -> Prop :=
+  fun M => exists Gamma t, type_assignment Gamma M t.
+
+(* Intersection Type Inhabitation *)
+Definition CD_INH : (list ty) * sty -> Prop :=
+  fun '(Gamma, t) => exists M, type_assignment Gamma M t.

theories/IntersectionTypes/CD_undec.v

@@ -0,0 +1,56 @@
+(*
+  Author(s):
+    Andrej Dudenhefner (1)
+  Affiliation(s):
+    (1) TU Dortmund University, Dortmund, Germany
+*)
+
+(*
+  Undecidability Result(s):
+    Intersection Type Inhabitation (CD_INH)
+    Intersection Type Typability (CD_TYP)
+    Intersection Type Type Checking (CD_TC)
+*)
+
+Require Import Undecidability.Synthetic.Undecidability.
+
+Require Import Undecidability.IntersectionTypes.CD.
+From Undecidability.IntersectionTypes.Reductions Require 
+  SSTS01_to_CD_INH CD_TYP_to_CD_TC SNclosed_to_CD_TYP.
+
+Require Import Undecidability.StringRewriting.SSTS_undec.
+Require Import Undecidability.LambdaCalculus.Lambda_undec.
+
+(* Undecidability of Intersection Type Inhabitation *)
+Theorem CD_INH_undec : undecidable CD_INH.
+Proof.
+  apply (undecidability_from_reducibility SSTS01_undec).
+  exact SSTS01_to_CD_INH.reduction.
+Qed.
+
+Check CD_INH_undec.
+
+(* Undecidability of Intersection Type Typability *)
+Theorem CD_TYP_undec : undecidable CD_TYP.
+Proof.
+  apply (undecidability_from_reducibility SNclosed_undec).
+  exact SNclosed_to_CD_TYP.reduction.
+Qed.
+
+Check CD_TYP_undec.
+
+
+(* Undecidability of Intersection Type Type Checking *)
+Theorem CD_TC_undec : undecidable CD_TC.
+Proof.
+  apply (undecidability_from_reducibility CD_TYP_undec).
+  exact CD_TYP_to_CD_TC.reduction.
+Qed.
+
+Check CD_TC_undec.
+
+(*
+Print Assumptions CD_INH_undec.
+Print Assumptions CD_TYP_undec.
+Print Assumptions CD_TC_undec.
+*)

theories/IntersectionTypes/Reductions/CD_TYP_to_CD_TC.v

@@ -0,0 +1,78 @@
+(*
+  Author(s):
+    Andrej Dudenhefner (1)
+  Affiliation(s):
+    (1) TU Dortmund University, Dortmund, Germany
+*)
+
+(*
+  Reduction from:
+    Intersection Type Typability (CD_TYP)
+  to:
+    Intersection Type Type Checking (CD_TC)
+*)
+
+From Undecidability.IntersectionTypes Require Import CD Util.CD_facts.
+Require Import Undecidability.LambdaCalculus.Util.term_facts.
+Require Undecidability.L.L.
+Require Import List PeanoNat Lia.
+Import L (term, var, app, lam).
+
+Require Import ssreflect.
+
+Set Default Goal Selector "!".
+
+Fixpoint var_bound M :=
+  match M with
+  | var x => 1 + x
+  | app M N => 1 + var_bound M + var_bound N
+  | lam M => var_bound M
+  end.
+
+Lemma var_bound_spec M : allfv (fun x => x < var_bound M) M.
+Proof.
+  elim: M=> /=.
+  - lia.
+  - move=> ? IH1 ? IH2. split.
+    + apply: allfv_impl IH1. lia.
+    + apply: allfv_impl IH2. lia.
+  - move=> ?. by apply: allfv_impl=> - [|?] /=; [|lia].
+Qed.
+
+Lemma var_bound_spec' Gamma M t : type_assignment Gamma M t -> 
+  type_assignment (map (fun i => match nth_error Gamma i with Some phi => phi | None => (atom 0, nil) end) (seq 0 (var_bound M))) M t.
+Proof.
+  move=> /type_assignment_ren_fv => /(_ _ id). rewrite ren_id_term. apply.
+  apply: allfv_impl (var_bound_spec M) => x ?.
+  move=> > /(@nth_error_split ty) [Gamma1] [Gamma2] [-> ?]. subst x.
+  rewrite nth_error_map nth_error_seq /=; first done.
+  by rewrite nth_error_app2 ?Nat.sub_diag.
+Qed.
+
+Lemma abs_Gamma_spec Gamma M t : type_assignment Gamma M t -> exists t', type_assignment nil (Nat.iter (length Gamma) lam M) t'.
+Proof.
+  elim: Gamma M t. { move=> ???. eexists. by eassumption. }
+  move=> [s phi] Gamma IH ?? /type_assignment_arr /IH /=.
+  congr ex. congr type_assignment.
+  elim: (length Gamma). { done. }
+  by move=> ? /= ->.
+Qed.
+
+Require Import Undecidability.Synthetic.Definitions.
+
+(* reduction from intersection type typability to intersection type type checking *)
+Theorem reduction : CD_TYP ⪯ CD_TC.
+Proof.
+  exists (fun M => (nil, app (lam (lam (var 0))) (Nat.iter (var_bound M) lam M), arr (atom 0) nil (atom 0))).
+  move=> M. split.
+  - move=> [Gamma] [t] /var_bound_spec' /abs_Gamma_spec [t'].
+    rewrite /= map_length seq_length=> ?. econstructor.
+    + do 3 econstructor; first done. by left.
+    + by eassumption.
+    + by apply: Forall_nil.
+  - move=> /= /type_assignmentE [] s phi _ + _.
+    elim: (var_bound M) (nil) (s).
+    { move=> ???. do 2 eexists. by eassumption. }
+    move=> ? IH ? [?|???] /= /type_assignmentE; first done.
+    by apply: IH.
+Qed.