Library CoLoR.Term.Lambda.LCompClos

CoLoR, a Coq library on rewriting and termination.
See the COPYRIGHTS and LICENSE files.
  • Frederic Blanqui, 2013-05-02

Computability closure

and proof that it enforces termination of higher-order rewrite systems.
After "Inductive-data-type Systems", F. Blanqui, J.-P. Jouannaud and M. Okada, Theoretical Computer Science 272, p. 41-68, 2002, http://dx.doi.org/10.1016/S0304-3975(00)00347-9.

Set Implicit Arguments.


Module Export Def.

Abstract definition of the computability closure.


  Section cc.

We assume given a set F for function symbols, a set X for variables, and a set So for type constants.

    Variables F X : Type.

    Notation Te := (@Te F X).
    Notation Var := (@Var F X).
    Notation Fun := (@Fun F X).
    Notation Tes := (vector Te).
    Notation call := (@call F X).

    Variable So : Type.

    Notation Ty := (@Ty So).
    Notation Tys := (vector Ty).

We assume given a structure for finite sets on X.

    Variable ens_X : Ens X.

    Notation In := (Ens_In ens_X).
    Notation fvs := (@fvs F X ens_X).

We assume given a set En for typing environments equipped with the following functions:

    Variable env : Env X So.

    Notation En := (Env_type env).
    Notation MapsTo := (Env_MapsTo env).
    Notation add := (Env_add env).

We assume given a type for each function symbol.

    Variable typ : F -> Ty.

    Notation TypArgs := (@TypArgs F X So typ).

For each symbol f, we assume given a finite number of accessible arguments.

    Variables (Acc : F -> nat -> Prop)
      (Acc_arity : forall g i, Acc g i -> i < arity (typ g)).

We assume given an environment-indexed family of relations on calls.

    Variable gt1 : En -> relation call.

Definition of the computability closure for a call mk_call f ls.


    Section cc_def.

      Variables (f : F) (n : nat) (ls : Tes n).

      Inductive cc : En -> Te -> Ty -> Prop :=

      | cc_arg : forall E i (i1 : i < n) (i2 : i < arity (typ f)),
        cc E (Vnth ls i1) (Vnth (inputs (typ f)) i2)

      | cc_var : forall E x T,
        MapsTo x T E -> ~In x (fvs ls) -> cc E (Var x) T
      

      | cc_app : forall E t u A B,
        cc E t (A ~~> B) -> cc E u A -> cc E (App t u) B

      | cc_lam : forall E x A v B,
        ~In x (fvs ls) -> cc (add x A E) v B -> cc E (Lam x v) (A ~~> B)

      | cc_acc : forall E g (us : TypArgs g) i (hi : Acc g i),
        cc E (apps (Fun g) us) (Base (output_base (typ g))) ->
        cc E (Vnth us (Acc_arity hi)) (Vnth (inputs (typ g)) (Acc_arity hi))

      | cc_call : forall E g p (us : Tes p),
        0+p <= arity (typ g) -> gt1 E (mk_call f ls) (mk_call g us) ->
        (forall i (i1 : i < p) (i2 : i < arity (typ g)),
          cc E (Vnth us i1) (Vnth (inputs (typ g)) i2)) ->
        cc E (apps (Fun g) us) (output (typ g) p).

Variants of cc constructors for proving that some term is in cc.

     Lemma cc_arg' E v V i (i1 : i < n) (i2 : i < arity (typ f)) :
        v = Vnth ls i1 -> V = Vnth (inputs (typ f)) i2 -> cc E v V.

     Lemma cc_acc' E v V g (us : TypArgs g) i (hi : Acc g i) :
        cc E (apps (Fun g) us) (Base (output_base (typ g))) ->
        v = Vnth us (Acc_arity hi) ->
        V = Vnth (inputs (typ g)) (Acc_arity hi) -> cc E v V.

     Lemma cc_call' E v V g p (us : Tes p) :
        0+p <= arity (typ g) -> gt1 E (mk_call f ls) (mk_call g us) ->
        (forall i (i1 : i < p) (i2 : i < arity (typ g)),
          cc E (Vnth us i1) (Vnth (inputs (typ g)) i2)) ->
        v = apps (Fun g) us -> V = output (typ g) p -> cc E v V.

Inversion lemma and tactic for cc.

      Lemma inv_cc : forall E t T, cc E t T ->
        (exists i (i1 : i < n) (i2 : i < arity (typ f)),
          t = Vnth ls i1 /\ T = Vnth (inputs (typ f)) i2)
        \/ (exists x, t = Var x /\ MapsTo x T E /\ ~In x (fvs ls))
        \/ (exists v V u, t = App u v /\ cc E u (V ~~> T) /\ cc E v V)
        \/ (exists x v A B, t = Lam x v /\ T = A ~~> B /\ ~In x (fvs ls)
          /\ cc (add x A E) v B)
        \/ (exists g (us : TypArgs g) i (hi : Acc g i),
          t = Vnth us (Acc_arity hi) /\ T = Vnth (inputs (typ g)) (Acc_arity hi)
          /\ cc E (apps (Fun g) us) (Base (output_base (typ g))))
        \/ (exists g p (us : Tes p),
          t = apps (Fun g) us /\ T = output (typ g) p
          /\ 0+p <= arity (typ g) /\ gt1 E (mk_call f ls) (mk_call g us)).

    End cc_def.

    Lemma cc_cast : forall f n (ls : Tes n) p (h : n=p) E v V,
      cc f (Vcast ls h) E v V <-> cc f ls E v V.

  End cc.


  Ltac inv_cc h := apply inv_cc in h;
    let i := fresh "i" in let g := fresh "g" in let us := fresh "us" in
      let x := fresh "x" in let u := fresh "u" in let v := fresh "v" in
        let A := fresh "A" in let B := fresh "B" in let p := fresh "p" in
          let h1 := fresh "h" in let h2 := fresh "h" in
            let h3 := fresh "h" in let h4 := fresh "h" in
              destruct h as
                [[i [h1 [h2 [h3 h4]]]]
|[[x [h1 [h2 h3]]]
|[[v [A [u [h1 [h2 h3]]]]]
|[[x [v [A [B [h1 [h2 [h3 h4]]]]]]]
|[[g [us [i [h1 [h2 [h3 h4]]]]]]
|[g [p [us [h1 [h2 [h3 h4]]]]]]]]]]].

End Def.

Ingredients of a computability closure.


Module Type CC_Struct.

We assume given a BI structure.

  Declare Module Export BI : BI_Struct.

Some notations.

  Notation caeq := (@caeq F X FOrd.eq_dec XOrd.eq_dec ens_X var_notin).
  Notation cc := (@cc F X So ens_X env typ Acc Acc_arity).

End CC_Struct.

Axiomatic proof of correctness of the computability closure.


Module Comp (Export CC : CC_Struct)
  (Export CP : CP_Struct with Module L := CC.BI.ST.L).

  Module Export CS := LCompSimple.Make CC.BI.ST CP.
  Module Export C := LCall.Make CC.BI.ST.

  Section comp.

    Variables

      
We assume given an interpretation of base types as computability predicates.

      (I : So -> set Te) (I_cp : forall b, cp (I b))

      
We assume that the accessible arguments of a computable term of the form apps (Fun g) ts are computable.

      (comp_acc : forall g (ts : Tes (arity (typ g))),
        int I (Base (output_base (typ g))) (apps (Fun g) ts) ->
        forall i (hi : Acc g i),
          int I (Vnth (inputs (typ g)) (Acc_arity hi)) (Vnth ts (Acc_arity hi)))

      
We assume given an environment-indexed family of relations on calls.

      (gt1 : En -> relation call)

      
We assume given a relation gt2 on max calls that is wellfounded, compatible with mcaeq and decreases whenever gt1 decreases.

      (gt2 : relation max_call) (gt2_wf : WF gt2)
      (gt2_mcaeq : Proper (mcaeq ==> mcaeq ==> impl) gt2)
      (gt2_gt1 : forall E f n (ls : Tes n) g p (us : Tes p),
        n <= arity (typ f) -> p <= arity (typ g) ->
        gt1 E (mk_call f ls) (mk_call g us) ->
        forall s (ts' : Tes (arity (typ f) - n)) (us' : Tes (arity (typ g) - p))
          (nf : n + (arity (typ f) - n) = arity (typ f))
          (pg : p + (arity (typ g) - p) = arity (typ g)),
          vint I (inputs (typ f)) (Vapp (Vmap (subs s) ls) ts') ->
          (forall x A, MapsTo x A E -> ~XSet.In x (fvs ls) -> int I A (s x)) ->
          gt2 (mk_max_call f (Vcast (Vapp (Vmap (subs s) ls) ts') nf))
              (mk_max_call g (Vcast (Vapp (Vmap (subs s) us) us') pg)))

      
Induction hypothesis: we assume that, given a mk_max_call f ts such that ts are computable, every call mk_max_call g us smaller in gt2, is computable whenever us are computable.

      (f : F) (ts : TypArgs f) (hts : vint I (inputs (typ f)) ts)
      (IH : forall g (us : TypArgs g),
          gt2 (mk_max_call f ts) (mk_max_call g us) ->
        vint I (inputs (typ g)) us ->
        int I (output (typ g) (arity (typ g))) (apps (Fun g) us))

      
We assume given some terms ls and some substitution s0 such that Vmap (subs s0) ls is alpha-equivalent to a prefix of ts.

      (n : nat) (ls : Tes n) (s0 : X -> Te) (h : 0+n <= arity (typ f))
      (hls : Vmap (subs s0) ls ~~~ Vsub ts h).

Correctness proof:

we prove that, if v is in the closure of mk_call f ls and E, and s is a substitution equal to s0 on fvs ls and computable on variables of E not in fvs ls, then subs s v is computable.

    Lemma cc_comp : forall E v V, cc gt1 f ls E v V -> forall s,
      (forall x, XSet.In x (fvs ls) -> s x = s0 x) ->
      (forall x A, MapsTo x A E -> ~XSet.In x (fvs ls) -> int I A (s x)) ->
      int I V (subs s v).

  End comp.

End Comp.

Axiomatic proof of the termination of a rewrite system

whose right hand-sides are in the computability closure of their corresponding left hand-sides.

Module Termin (Export CC : CC_Struct)
  (Export RS : RS_Struct with Module L := CC.BI.ST.L).

  Module Export CR := LCompRewrite.Make RS.

We use the CP structure for the union of beta-reduction and rewriting defined in LCompRewrite.

  Module CP := CP_beta_eta_rewrite RS.

  Module Export C := Comp CC CP.

  Section termin.

    Variables

      
We assume given an interpretation of base types as computability predicates.

      (I : So -> set Te) (I_cp : forall b, cp (I b))

      
We assume that the accessible arguments of a computable term of the form apps (Fun g) ts are computable.

      (comp_acc : forall g (ts : TypArgs g),
        int I (Base (output_base (typ g))) (apps (Fun g) ts) ->
        forall i (hi : Acc g i),
          int I (Vnth (inputs (typ g)) (Acc_arity hi)) (Vnth ts (Acc_arity hi)))

      
We assume that apps (Fun f) ts is computable if all its reducts and arguments ts are computable.

      (comp_fun : forall f (ts : TypArgs f),
        vint I (inputs (typ f)) ts ->
        (forall u, apps (Fun f) ts =>R u -> I (output_base (typ f)) u) ->
        I (output_base (typ f)) (apps (Fun f) ts))

      
We assume given an environment-indexed family of relations on calls.

      (gt1 : En -> relation call)

      
We assume given a relation gt2 on max calls that is wellfounded, compatible with mcaeq and clos_vaeq, and decreases whenever gt1 decreases.

      (gt2 : relation max_call) (gt2_wf : WF gt2)
      (gt2_mcaeq : Proper (mcaeq ==> mcaeq ==> impl) gt2)
      (gt2_gt1 : forall E f n (ls : Tes n) g p (us : Tes p),
        n <= arity (typ f) -> p <= arity (typ g) ->
        gt1 E (mk_call f ls) (mk_call g us) ->
        forall s (ts' : Tes (arity (typ f) - n)) (us' : Tes (arity (typ g) - p))
          (nf : n + (arity (typ f) - n) = arity (typ f))
          (pg : p + (arity (typ g) - p) = arity (typ g)),
          vint I (inputs (typ f)) (Vapp (Vmap (subs s) ls) ts') ->
          (forall x A, MapsTo x A E -> ~XSet.In x (fvs ls) -> int I A (s x)) ->
          gt2 (mk_max_call f (Vcast (Vapp (Vmap (subs s) ls) ts') nf))
              (mk_max_call g (Vcast (Vapp (Vmap (subs s) us) us') pg)))
      (gt2_clos_vaeq : forall f ts us, vint I (inputs (typ f)) ts ->
        ts ==>R us -> gt2 (mk_max_call f ts) (mk_max_call f us))

      
We assume that, for every rule, the right hand-side is in the computability closure of the left hand-side.

      (lhs_cc_rhs : forall l r (h : rule l r),
        cc gt1 (lhs_fun h) (lhs_args h) XMap.empty r
        (output (typ (lhs_fun h)) (lhs_nb_args h))).

Termination proof.


    Lemma tr_sn_cc : forall E v V, E |- v ~: V -> SN R_aeq v.

  End termin.

End Termin.

Termination proof of a rewrite system

whose right hand-sides are in the computability closure of their corresponding left hand-sides, using the interpretation of types as computability predicates defined in LCompInt, and a DLQO based on the accessible supterm ordering for comparing function calls.

Module SN_rewrite (Export CC : CC_Struct)
  (Export RS : RS_Struct with Module L := CC.BI.ST.L)
  (Export CO : DLQO_Struct with Module ST := CC.BI.ST).

  Module Import T := Termin CC RS.

  Module Export CI := LCompInt.Make CC.BI.ST CP BI.

  Module Import L := LCall.Lex CO.

For gt1, i.e. for comparing function calls in the computability closure, we use gt_call (gt_args_lex gt) where gt is the alpha-closure of the accessibility subterm ordering.

  Definition gt := clos_aeq (supterm_acc!).

  Definition gt1 (E : En) := gt_call (gt_args_lex gt).

  Lemma gt1_wf E : WF (gt1 E).

  Instance gt1_aeq E : Proper (caeq ==> caeq ==> impl) (gt1 E).


For gt2, i.e. for the termination proof, we use a variant of gt1 that is compatible with ==>R: we use gt_call on the union of gt_args_lex (gt0)! and gt_red R, where gt0 is the restriction on wellfounded terms of gt U R_aeq.

  Definition gt0 := RelUtil.restrict (SN R_aeq) (gt U R_aeq).

  Definition gt2c := gt_call (fun r => gt_args_lex (gt0!) r U gt_red R).

  Definition gt2 := Rof gt2c max_call_call.

Properties of gt0.

  Lemma gt0_wf : WF gt0.

  Instance gt0_aeq : Proper (aeq ==> aeq ==> impl) gt0.


We check that gt2 is invariant by mcaeq.

  Instance gt2c_caeq : Proper (caeq ==> caeq ==> impl) gt2c.


  Instance gt2_mcaeq : Proper (mcaeq ==> mcaeq ==> impl) gt2.


We prove that gt2 is wellfounded.

  Import Lexicographic_Product.
  Import Union.

  Lemma gt2_wf : WF gt2.

We check that gt2 is compatible with ==>R.

  Lemma gt2_clos_vaeq : forall f (ts us : TypArgs f),
    vint I (inputs (typ f)) ts -> ts ==>R us ->
    gt2 (mk_max_call f ts) (mk_max_call f us).

We check that gt1 makes gt2 decrease.

  Import Lexico.

  Lemma gt2_gt1 : forall E f n (ls : Tes n) g p (us : Tes p),
      n <= arity (typ f) -> p <= arity (typ g) ->
      gt1 E (mk_call f ls) (mk_call g us) ->
      forall s (ts' : Tes (arity (typ f) - n)) (us' : Tes (arity (typ g) - p))
        (nf : n + (arity (typ f) - n) = arity (typ f))
        (pg : p + (arity (typ g) - p) = arity (typ g)),
        vint I (inputs (typ f)) (Vapp (Vmap (subs s) ls) ts') ->
        (forall x A, MapsTo x A E -> ~XSet.In x (fvs ls) -> int I A (s x)) ->
        gt2 (mk_max_call f (Vcast (Vapp (Vmap (subs s) ls) ts') nf))
            (mk_max_call g (Vcast (Vapp (Vmap (subs s) us) us') pg)).

Termination theorem.

  Section termin.

    Variables
      (lhs_cc_rhs : forall l r (h : rule l r),
        cc gt1 (lhs_fun h) (lhs_args h)
        XMap.empty r (output (typ (lhs_fun h)) (lhs_nb_args h))).

    Lemma tr_sn_beta_eta_rewrite_aeq : forall E v V, E |- v ~: V -> SN R_aeq v.

  End termin.

End SN_rewrite.