Library CL1
Require Import Framework.
Implicit Types rho : type_context.
Implicit Types x y z : var.
Implicit Types u v : inttype -> Prop.
Implicit Types rho : type_context.
Implicit Types x y z : var.
Implicit Types u v : inttype -> Prop.
Term syntax of combinatory logic
Inductive CL : Type :=
| S
| K
| app (a b : CL).
Implicit Types a b c : CL.
Coercion app : CL >-> Funclass.
| S
| K
| app (a b : CL).
Implicit Types a b c : CL.
Coercion app : CL >-> Funclass.
Type syntax of CL
Inductive simpletype : Type :=
| base (x : var) : simpletype
| arr (A B : simpletype) : simpletype.
Notation "A --> B" := (arr A B).
Implicit Types A B C : simpletype.
Typing relation of CL: Note absence of context
Inductive CL_ty : CL -> simpletype -> Prop :=
| CLS A B C : CL_ty S ((A --> B --> C) --> (A --> B) --> A --> C)
| CLK A B : CL_ty K (A --> B --> A)
| CLapp a b A B : CL_ty a (A --> B) -> CL_ty b A -> CL_ty (a b) B.
| CLS A B C : CL_ty S ((A --> B --> C) --> (A --> B) --> A --> C)
| CLK A B : CL_ty K (A --> B --> A)
| CLapp a b A B : CL_ty a (A --> B) -> CL_ty b A -> CL_ty (a b) B.
Interpret variables according to valuation,
arrow types as functional product
Fixpoint int_ty A sigma := match A with
| base x => sigma x
| arr A B => prod (int_ty A sigma) (int_ty B sigma)
end.
Notation "[[ A ]] sigma" := (int_ty A sigma) (at level 1).
| base x => sigma x
| arr A B => prod (int_ty A sigma) (int_ty B sigma)
end.
Notation "[[ A ]] sigma" := (int_ty A sigma) (at level 1).
Obviously, this yields realizor predicates
Lemma int_ty_rp : rp_preservation simpletype int_ty.
hnf.
induction T ; simpl ; auto using prod_realizable.
Qed.
hnf.
induction T ; simpl ; auto using prod_realizable.
Qed.
Reduction relation of CL
Inductive cl_step : CL -> CL -> Prop :=
| cl_stepS a b c : cl_step (S a b c) (a c (b c))
| cl_stepK a b : cl_step (K a b) a
| cl_step_appL a b c : cl_step a b -> cl_step (a c) (b c)
| cl_step_appR a b c : cl_step b c -> cl_step (a b) (a c).
| cl_stepS a b c : cl_step (S a b c) (a c (b c))
| cl_stepK a b : cl_step (K a b) a
| cl_step_appL a b c : cl_step a b -> cl_step (a c) (b c)
| cl_step_appR a b c : cl_step b c -> cl_step (a b) (a c).
Compile to equivalent terms
Fixpoint CLC a := match a with
| S => Lam (Lam (Lam (TVar 2 (TVar 0) (TVar 1 (TVar 0)))))
| K => Lam (Lam (TVar 1))
| app a b => CLC a (CLC b)
end.
The compiler is consistent
Lemma CLC_c : compiler_consistency _ CLC cl_step.
intros a b. induction 1 ; simpl.
- econstructor 2. auto using step_appL, step_beta.
econstructor 2. eauto using step_appL, step_beta.
constructor. asimpl. eauto using step_beta_eq.
- econstructor 2. auto using step_appL, step_beta.
constructor. asimpl. eauto using step_beta_eq.
- now apply steps_appL.
- now apply steps_appR.
Qed.
The compiler is adequate
Lemma in_int_ty : cadequacy simpletype int_ty CL CLC (fun _ _ => CL_ty).
hnf.
simpl.
intros rho sigma rho_val sigma_val a A clt.
induction clt ; simpl in *.
- constructor ; eauto using int_IF, closure_filter ; intros vf Af.
constructor ; eauto using int_IF, closure_filter ; intros vg Ag.
constructor ; eauto using int_IF, closure_filter ; intros vx Ax.
assert (IFilter vf) by apply Af.
assert (IFilter vg) by apply Ag.
assert (IFilter vx) by eauto using only_filter, int_ty_rp.
assert (realizorPredicate [[C]]sigma) by auto using int_ty_rp.
assert (rpA : realizorPredicate [[A]]sigma) by auto using int_ty_rp.
assert (rpABC : realizorPredicate (prod [[A]]sigma (prod [[B]]sigma [[C]]sigma))) by auto using int_ty_rp, prod_realizable.
assert (rpAB : realizorPredicate (prod [[A]]sigma [[B]]sigma)) by auto using int_ty_rp, prod_realizable.
assert (exists (A : inttype), vf A) by now apply rpABC.
assert (exists (A : inttype), vg A) by now apply rpAB.
assert (exists (A : inttype), vx A) by now apply rpA.
rewrite <- ! int_lam, ! int_st, ! int_x ; auto using valid_up.
simpl.
now apply Af, Ag.
- constructor ; eauto using int_IF, closure_filter ; intros vf Af.
constructor ; eauto using int_IF, closure_filter ; intros vg Ag.
assert (rpA : realizorPredicate [[A]]sigma) by auto using int_ty_rp.
assert (rpB : realizorPredicate [[B]]sigma) by auto using int_ty_rp.
assert (IFilter vf) by now apply rpA.
assert (IFilter vg) by now apply rpB.
assert (exists (A : inttype), vf A) by now apply rpA.
assert (exists (A : inttype), vg A) by now apply rpB.
rewrite <- ! int_lam, ! int_x ; auto using valid_up.
- assert (rpB : realizorPredicate [[B]]sigma) by auto using int_ty_rp.
rewrite ! int_st ; auto.
now apply IHclt1.
Qed.
The CL typing has no context and thus ignores the type contexts and valuations
Lemma CL_valid : validation _ _ CL_ty (fun _ _ => CL_ty).
split.
- intros ty. exists top_rho, top_sigma. intuition ; eauto 6 using top_rho_valid, top_sigma_valuation.
- intros [? [? [? [? tyt] ] ] ]. auto.
Qed.
CL terminates