Merge pull request #220 from mrhaandi/HO-matching

Higher-order beta-matching

README.md

@@ -100,6 +100,7 @@ An equivalence proof that most of the mentioned models of computation compute th
 - Strong normalization for given terms in the strong call-by-name 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))
+- Higher-order matching wrt. beta-equivalence (`HOMbeta` in [`LambdaCalculus/HOMatching.v`](theories/LambdaCalculus/HOMatching.v))
 
 #### Decidable Problems
 

theories/LambdaCalculus/HOMatching.v

@@ -0,0 +1,41 @@
+(*
+  Author(s):
+    Andrej Dudenhefner (TU Dortmund University, Germany)
+
+  Problem(s):
+    Higher-Order Matching wrt. beta-equivalence (HOMbeta)
+
+  Literature:
+  [1] Loader, Ralph. "Higher order β-matching is undecidable." Logic Journal of the IGPL 11.1 (2003): 51-68.
+*)
+
+Require Import List Relation_Operators.
+
+Require Undecidability.L.L Undecidability.LambdaCalculus.Lambda.
+
+(* lambda-term syntax *)
+Import L (term, var, app, lam).
+
+(* beta-reduction (strong call-by-name reduction) *)
+Import Lambda (step).
+
+(* simple types with a single atom *)
+Inductive ty : Type :=
+  | atom (* type variable *)
+  | arr (s t : ty). (* function type *)
+
+(*
+  simply typed lambda-calculus with a single atom
+  "stlc Gamma M s" means that in the type environment Gamma the term M is assigned the type s
+*)
+Inductive stlc (Gamma : list ty) : term -> ty -> Prop :=
+  | stlc_var x t : nth_error Gamma x = Some t -> stlc Gamma (var x) t
+  | stlc_app M N s t : stlc Gamma M (arr s t) -> stlc Gamma N s -> stlc Gamma (app M N) t
+  | stlc_lam M s t : stlc (cons s Gamma) M t -> stlc Gamma (lam M) (arr s t).
+
+(* Higher-Order Matching wrt. beta-equivalence *)
+Definition HOMbeta : { '(s, t, F, N) : (ty * ty * term * term) | stlc nil F (arr s t) /\ stlc nil N t } -> Prop :=
+  (* given simply typed terms F : s -> t and N : t *)
+  fun '(exist _ (s, t, F, N) _) =>
+    (* is there a simply typed term M : s such that F A is beta-equivalent to B? *)
+    exists (M : term), stlc nil M s /\ clos_refl_sym_trans term step (app F M) N.

theories/LambdaCalculus/HOMatching_undec.v

@@ -0,0 +1,22 @@
+(*
+  Author(s):
+    Andrej Dudenhefner (TU Dortmund University, Germany)
+
+  Undecidability Result(s):
+    Higher-Order Matching wrt. beta-equivalence (HOMbeta_undec)
+*)
+
+From Undecidability.Synthetic Require Import Undecidability.
+
+Require Import Undecidability.LambdaCalculus.HOMatching.
+Require Undecidability.LambdaCalculus.Reductions.SSTS01_to_HOMbeta.
+Require Import Undecidability.StringRewriting.SSTS_undec.
+
+(* Undecidability of Higher-Order Matching wrt. beta-equivalence *)
+Theorem HOMbeta_undec : undecidable HOMbeta.
+Proof.
+  apply (undecidability_from_reducibility SSTS01_undec).
+  exact SSTS01_to_HOMbeta.reduction.
+Qed.
+
+Check HOMbeta_undec.

theories/LambdaCalculus/Reductions/HaltLclosed_to_wCBNclosed.v

@@ -334,7 +334,7 @@ Qed.
 
 Lemma closed_colon {s} : closed s -> forall sigma, subst sigma (colon s (lam (var 0))) = colon s (lam (var 0)).
 Proof.
-  move=> Hs sigma. rewrite subst_closed; last done.
+  move=> Hs sigma. rewrite subst_L_closed; last done.
   by apply /closed_dcl /bound_colon; apply /closed_dcl.
 Qed.