Library Framework

Termination Framework

Require Export RealizorPredicates.
Require Export Reduction.
Require Import Termination.

Implicit Types rho : type_context.
Implicit Types Gamma Delta : context.

Implicit Types u v : inttype -> Prop.

Implicit Types x y z : var.
Implicit Types s t : term.

A valuation maps variables to Realizor Predicates
Definition rc_ctx := var -> realizorCandidate.
Implicit Types sigma : rc_ctx.

Definition valuation sigma := forall x, realizorPredicate (sigma x).

Valuations can be extended with Realizor Predicates
Lemma valuation_up {P sigma} : valuation sigma -> realizorPredicate P -> valuation (P .: sigma).
intros sigma_val rpP [|x] ; simpl ; auto. Qed.

Section General_Termination.
The termination framework works for any other type system ttype
  Variable ttype : Type.
  Implicit Types S T : ttype.

These types are interpreted under a valuation
  Variable int_ty : ttype -> rc_ctx -> realizorCandidate.

  Notation "[[ T ]] sigma" := (int_ty T sigma) (at level 1).

The type interpretation preserves Realizor Predicates if it interprets types as Realizor Predicates

  Definition rp_preservation := (forall T sigma, valuation sigma -> realizorPredicate [[T]]sigma).


  Section Compiler.
The termination framework accepts any source system that can be embedded into the pure lambda calculus

    Variable tterm : Type.
    Implicit Types a b c : tterm.

    Variable compiler : tterm -> term.
    Notation "[| a |]" := (compiler a) (at level 9).

Furthermore, we assume that there is a typing system that relates terms and types
    Variable ctty : tterm -> ttype -> Prop.

The typing system validates if it recognizes valid type contexts and valuations
    Variable vtty : forall rho sigma, tterm -> ttype -> Prop.
    Definition validation := forall a T,
      ctty a T <-> (exists rho sigma, valid rho /\ valuation sigma /\ vtty rho sigma a T).

In addition to this, we consider a reduction relation on the terms of the source system
    Variable tstep : tterm -> tterm -> Prop.
    Definition TSN := GSN tstep.

The compiler is consistent if it preserves reducibility
    Definition compiler_consistency := forall a b, tstep a b -> steps [|a|] [|b|].
The compiler is adequate if it compiles the term to a term which can be given types that correspond to the original type
    Definition cadequacy := forall {rho sigma}, valid rho -> valuation sigma -> forall {a T}, vtty rho sigma a T -> [[T]]sigma [ [|a|] ]rho.

Compiler consistency and the termination of the compilate imply termination of the source

    Lemma sn_tsn a : compiler_consistency -> SN [|a|] -> TSN a.
    intros H sn.
    apply sn_gsn in sn.
    remember ([|a|]) as t.
    revert a Heqt.
    induction sn as [? ? IH].
    constructor ; subst.
    intros b st. apply IH with ([| b |]) ; auto.
    Qed.

Any system that validates, preserves realizor predicates, and has an adequate and consistent compiler is terminating

    Theorem tsn : validation -> rp_preservation -> cadequacy -> compiler_consistency
      -> forall a T, ctty a T -> TSN a.
    intros v rpr ad cc a T tyt.
    unfold validation in *. rewrite v in tyt.
    destruct tyt as [rho [sigma [rho_val [sigma_val tyt ] ] ] ].
    assert (inRP := ad _ _ rho_val sigma_val _ _ tyt).
    destruct (excl_bot [[T]]sigma (rpr _ _ sigma_val) _ inRP) as [A [n Gamma comp styt] ].
    apply sn_tsn ; auto.
    apply (sn_system _ _ _ _ styt).
    Qed.
  End Compiler.

  Section LambdaCurry.
For the special case of lambda curry, we do not need to provide a special compiler
We can assume that lambda curry systems use contexts in their typing judgements
    Definition t_ctx := var -> ttype.
    Implicit Types tGamma : t_ctx.
    Variable tty : t_ctx -> term -> ttype -> Prop.

The lambda curry compiler is the identity mapping and is trivally consistent
    Definition lcc t := t.
    Lemma lcc_c : (compiler_consistency _ lcc step).
    cbv ; auto using one. Qed.

A type context validates a source context and and valuation if it is pointwise contained in the type interpretation of the source context
    Definition validates rho tGamma sigma := forall x, [[tGamma x]]sigma (rho x).

Validity is preserved under extension with compatible types and filters
    Lemma validates_up {rho tGamma sigma} : validates rho tGamma sigma -> forall T u, [[T]]sigma u ->
      validates (u .: rho) (T .: tGamma) sigma.
    intros rho_sigma_val A u Au [|x] ; simpl in * ; auto. Qed.

The top type context maps all variables to top and is valid
    Definition top_rho x := top.
    Lemma top_rho_valid : valid top_rho.

The top valuation maps all variables to the top realizor
    Definition top_sigma x := top_rp.
    unfold valid.
    eauto using top_filter. Qed.
    Lemma top_sigma_valuation : valuation top_sigma.
    unfold valuation.
    eauto using top_rp_realizable. Qed.

The typing judgement recognizes type contexts and valuations if the system preserves realizor predicates
    Inductive val_ty rho sigma t T : Prop := val_ty_gamma tGamma : validates rho tGamma sigma -> tty tGamma t T -> val_ty rho sigma t T.
    Lemma val_ty_v : rp_preservation -> validation term (fun t T => exists tGamma, tty tGamma t T) val_ty.
    intros rp t T.
    split.
    - intros [tGamma tyt].
      exists top_rho, top_sigma.
      intuition ; eauto using top_rho_valid, top_sigma_valuation.
      exists tGamma ; auto.
      intros x. unfold top_rho. apply incl_top, rp. apply top_sigma_valuation.
    - intros [? [? [? [? [tGamma ? tyt] ] ] ] ]. eauto.
    Qed.

The system is adequate if the term interpretation is contained in the type interpretation, i.e., the type interpretation contains all possible A-Types that can be given to its terms
    Definition adequacy := forall {tGamma t T}, tty tGamma t T -> forall {rho sigma}, valid rho -> valuation sigma -> validates rho tGamma sigma -> [[T]]sigma [t]rho.

Adequacy suffices to show that the lambda curry compiler is adequate
    Lemma adequacy_cadequacy : adequacy -> cadequacy _ lcc val_ty.
    intros ad rho sigma rho_val sig_val a T [tGamma rho_sigma_val tyt].
    eauto. Qed.

Therefore adequacy and preservation of realizor candidates imply termination in any lambda curry system
    Lemma sn : rp_preservation -> adequacy
      -> forall tGamma t T, tty tGamma t T -> SN t.
    intros rp ad tGamma t T tyt.
    assert ((fun t T => exists tGamma, tty tGamma t T) t T) by eauto.
    change SN with (TSN _ step).
    eauto using tsn, adequacy_cadequacy, val_ty_v, lcc_c.
    Qed.
  End LambdaCurry.
End General_Termination.