senvas/ladder-calculus
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

Compare commits

base: senvas:638ddf4fd1a3655264ded3852bf0074702af9e1b
Branches Tags
senvas:main
..
compare: senvas:6f8168610566d1d0d84eae46356041700e55a3e6
Branches Tags
senvas:main

No commits in common. "638ddf4fd1a3655264ded3852bf0074702af9e1b" and "6f8168610566d1d0d84eae46356041700e55a3e6" have entirely different histories.
638ddf4fd1 ... 6f81686105

9 changed files with 220 additions and 329 deletions
Show stats Expand all files Collapse all files

3
coq/_CoqProject
View file

@ -3,9 +3,8 @@ terms.v
equiv.v
subst.v
subtype.v
context.v
morph.v
typing.v
morph.v
smallstep.v
soundness.v
bbencode.v

9
coq/bbencode.v
View file

@ -55,8 +55,13 @@ Definition bb_succ : expr_term :=
(expr_var "z")))))))).
Definition e1 : expr_term :=
(expr_let "bb-zero" bb_zero
(expr_app (expr_app (expr_var "+") (expr_var "bb-zero")) (expr_var "bb-zero"))
(expr_let "bb-zero" (type_ladder (type_id "ℕ")
(type_ladder (type_id "BBNat")
(type_univ "α"
(type_fun (type_fun (type_var "α") (type_var "α"))
(type_fun (type_var "α") (type_var "α"))))))
bb_zero
(expr_app (expr_app (expr_var "+") (expr_var "bb-zero")) (expr_var "bb-zero"))
).
Definition t1 : expr_term := (expr_app (expr_var "x") (expr_var "x")).

21
coq/context.v
View file

@ -1,21 +0,0 @@
From Coq Require Import Strings.String.
Require Import terms.
Include Terms.
Module Context.
Inductive context : Type :=
| ctx_assign : string -> type_term -> context -> context
| ctx_empty : context
.
Inductive context_contains : context -> string -> type_term -> Prop :=
| C_take : forall (x:string) (X:type_term) (Γ:context),
(context_contains (ctx_assign x X Γ) x X)
| C_shuffle : forall x X y Y Γ,
(context_contains Γ x X) ->
(context_contains (ctx_assign y Y Γ) x X).
End Context.

120
coq/morph.v
View file

@ -3,100 +3,66 @@ Require Import terms.
Require Import subst.
Require Import equiv.
Require Import subtype.
Require Import context.
Require Import typing.
Include Terms.
Include Subst.
Include Equiv.
Include Subtype.
Include Context.
Include Typing.
Module Morph.
(* Given a context, there is a morphism path from τ to τ' *)
Reserved Notation "Γ '|-' σ '~>' τ" (at level 101, σ at next level, τ at next level).
Inductive morphism_path : context -> type_term -> type_term -> Prop :=
| M_Sub : forall Γ τ τ',
(τ :<= τ') ->
(Γ |- τ ~> τ')
Reserved Notation "Γ '|-' '[[' e ']]' '=' t" (at level 101, e at next level, t at level 0).
| M_Single : forall Γ h τ τ',
Inductive expand_morphisms : context -> expr_term -> expr_term -> Prop :=
| Expand_Transform : forall Γ e h τ τ',
(context_contains Γ h (type_morph τ τ')) ->
(Γ |- τ ~> τ')
(Γ |- e \is τ) ->
(Γ |- [[ e ]] = (expr_app (expr_var h) e))
| M_Chain : forall Γ τ τ' τ'',
(Γ |- τ ~> τ') ->
(Γ |- τ' ~> τ'') ->
(Γ |- τ ~> τ'')
| Expand_Otherwise : forall Γ e,
(Γ |- [[ e ]] = e)
| M_Lift : forall Γ σ τ τ',
(Γ |- τ ~> τ') ->
(Γ |- (type_ladder σ τ) ~> (type_ladder σ τ'))
| Expand_App : forall Γ f f' a a' σ τ,
(Γ |- f \compatible (type_fun σ τ)) ->
(Γ |- a \compatible σ) ->
(Γ |- [[ f ]] = f') ->
(Γ |- [[ a ]] = a') ->
(Γ |- [[ (expr_app f a) ]] = (expr_app f a'))
| M_MapSeq : forall Γ τ τ',
(Γ |- τ ~> τ') ->
(Γ |- (type_spec (type_id "Seq") τ) ~> (type_spec (type_id "Seq") τ'))
where "Γ '|-' s '~>' t" := (morphism_path Γ s t).
where "Γ '|-' '[[' e ']]' '=' t" := (expand_morphisms Γ e t).
Inductive translate_morphism_path : context -> type_term -> type_term -> expr_term -> Prop :=
| Translate_Subtype : forall Γ τ τ',
(τ :<= τ') ->
(translate_morphism_path Γ τ τ'
(expr_morph "x" τ (expr_var "x")))
| Translate_Lift : forall Γ σ τ τ' m,
(Γ |- τ ~> τ') ->
(translate_morphism_path Γ τ τ' m) ->
(translate_morphism_path Γ (type_ladder σ τ) (type_ladder σ τ')
(expr_morph "x" (type_ladder σ τ)
(expr_ascend (type_ladder σ τ') (expr_app m (expr_descend τ (expr_var "x"))))))
| Translate_Single : forall Γ h τ τ',
(context_contains Γ h (type_morph τ τ')) ->
(translate_morphism_path Γ τ τ' (expr_var h))
| Translate_Chain : forall Γ τ τ' τ'' m1 m2,
(translate_morphism_path Γ τ τ' m1) ->
(translate_morphism_path Γ τ' τ'' m2) ->
(translate_morphism_path Γ τ τ''
(expr_morph "x" τ (expr_app m2 (expr_app m1 (expr_var "x")))))
| Translate_MapSeq : forall Γ τ τ' m,
(translate_morphism_path Γ τ τ' m) ->
(translate_morphism_path Γ
(type_spec (type_id "Seq") τ)
(type_spec (type_id "Seq") τ')
(expr_morph "xs"
(type_spec (type_id "Seq") τ)
(expr_app (expr_app (expr_ty_app (expr_ty_app
(expr_var "map") τ) τ') m)
(expr_var "xs"))))
.
Example morphism_paths :
(ctx_assign "degrees-to-turns" [< $"Angle"$~$"Degrees"$~$"ℝ"$ ->morph $"Angle"$~$"Turns"$~$"ℝ"$ >]
(ctx_assign "turns-to-radians" [< $"Angle"$~$"Turns"$~$"ℝ"$ ->morph $"Angle"$~$"Radians"$~$"ℝ"$ >]
ctx_empty))
|- [< <$"Seq"$ $"Hue"$~$"Angle"$~$"Degrees"$~$"ℝ"$> >]
~> [< <$"Seq"$ $"Hue"$~$"Angle"$~$"Radians"$~$"ℝ"$> >]
(* For every well-typed term, there is an expanded exactly typed term *)
Lemma well_typed_is_expandable :
forall (e:expr_term),
(is_well_typed e) ->
exists Γ e', (expand_morphisms Γ e e') -> (is_exactly_typed e')
.
Proof.
intros.
apply M_MapSeq.
apply M_Lift.
apply M_Chain with (τ':=[<$"Angle"$~$"Turns"$~$"ℝ"$>]).
apply M_Single with (h:="degrees-to-turns"%string).
apply C_take.
apply M_Single with (h:="turns-to-radians"%string).
apply C_shuffle.
apply C_take.
Qed.
Admitted.
End Morph.
Example expand1 :
(ctx_assign "morph-radix"
[< <%"PosInt"% %"16"%> ->morph <%"PosInt"% %"10"%> >]
(ctx_assign "fn-decimal"
[< <%"PosInt"% %"10"%> -> <%"PosInt"% %"10"%> >]
(ctx_assign "x"
[< <%"PosInt"% %"16"%> >]
ctx_empty)))
|- [[ (expr_app (expr_var "fn-decimal") (expr_var "x")) ]]
= (expr_app (expr_var "fn-decimal")
(expr_app (expr_var "morph-radix") (expr_var "x")))
.
Proof.
apply Expand_App with (f':=(expr_var "fn-decimal")) (σ:=[< < %"PosInt"% %"10"% > >]) (τ:=[< < %"PosInt"% %"10"% > >]).
apply TCompat_Native.
Admitted.
End Morph.

31
coq/soundness.v
View file

@ -22,6 +22,15 @@ Definition is_stuck (e:expr_term) : Prop :=
~(exists e', e -->β e')
.
(* every exactly typed term is not stuck *)
Lemma exact_progress :
forall (e:expr_term),
(is_exactly_typed e) -> ~(is_stuck e)
.
Proof.
Admitted.
(* every well typed term is not stuck *)
Lemma progress :
forall (e:expr_term),
@ -31,14 +40,32 @@ Proof.
Admitted.
(* reduction step preserves well-typedness *)
Lemma preservation :
(* reduction step preserves the type *)
Lemma exact_preservation :
forall Γ e e' τ,
(Γ |- e \is τ) ->
(e -->β e') ->
(Γ |- e' \is τ)
.
Proof.
(*
intros.
generalize dependent e'.
induction H.
intros e' I.
inversion I.
*)
Admitted.
(* reduction step preserves well-typedness *)
Lemma preservation :
forall Γ e e' τ,
(Γ |- e \compatible τ) ->
(e -->β e') ->
(Γ |- e' \compatible τ)
.
Proof.
Admitted.
(* every well-typed expression can be reduced to a value *)

2
coq/subst.v
View file

@ -115,7 +115,7 @@ Fixpoint expr_subst (v:string) (n:expr_term) (e0:expr_term) :=
| expr_abs x t e => if (eqb v x) then e0 else expr_abs x t (expr_subst v n e)
| expr_morph x t e => if (eqb v x) then e0 else expr_morph x t (expr_subst v n e)
| expr_app e a => expr_app (expr_subst v n e) (expr_subst v n a)
| expr_let x a e => expr_let x (expr_subst v n a) (expr_subst v n e)
| expr_let x t a e => expr_let x t (expr_subst v n a) (expr_subst v n e)
| expr_ascend t e => expr_ascend t (expr_subst v n e)
| expr_descend t e => expr_descend t (expr_subst v n e)
end.

22
coq/terms.v
View file

@ -25,11 +25,12 @@ Inductive expr_term : Type :=
| expr_abs : string -> type_term -> expr_term -> expr_term
| expr_morph : string -> type_term -> expr_term -> expr_term
| expr_app : expr_term -> expr_term -> expr_term
| expr_let : string -> expr_term -> expr_term -> expr_term
| expr_let : string -> type_term -> expr_term -> expr_term -> expr_term
| expr_ascend : type_term -> expr_term -> expr_term
| expr_descend : type_term -> expr_term -> expr_term
.
(* TODO
Inductive type_DeBruijn : Type :=
@ -98,20 +99,11 @@ Notation "[{ e }]" := e
(e custom ladder_expr at level 80) : ladder_expr_scope.
Notation "'%' x '%'" := (expr_var x%string)
(in custom ladder_expr at level 0, x constr) : ladder_expr_scope.
Notation "'λ' x τ '↦' e" := (expr_abs x τ e) (in custom ladder_expr at level 0, x constr, τ custom ladder_type at level 99, e custom ladder_expr at level 99).
Notation "'Λ' t '↦' e" := (expr_ty_abs t e)
(in custom ladder_expr at level 10, t constr, e custom ladder_expr at level 80) : ladder_expr_scope.
Notation "'λ' x τ '↦' e" := (expr_abs x τ e)
(in custom ladder_expr at level 10, x constr, τ custom ladder_type at level 99, e custom ladder_expr at level 99) :ladder_expr_scope.
Notation "'λ' x τ '↦morph' e" := (expr_morph x τ e)
(in custom ladder_expr at level 10, x constr, τ custom ladder_type at level 99, e custom ladder_expr at level 99) :ladder_expr_scope.
Notation "'let' x ':=' e 'in' t" := (expr_let x e t)
(in custom ladder_expr at level 20, x constr, e custom ladder_expr at level 99, t custom ladder_expr at level 99) : ladder_expr_scope.
Notation "e 'as' τ" := (expr_ascend τ e)
(in custom ladder_expr at level 30, e custom ladder_expr, τ custom ladder_type at level 99) : ladder_expr_scope.
Notation "e1 e2" := (expr_app e1 e2)
(in custom ladder_expr at level 50) : ladder_expr_scope.
Notation "'(' e ')'" := e
(in custom ladder_expr at level 0) : ladder_expr_scope.
(in custom ladder_expr at level 0, t constr, e custom ladder_expr at level 80).
(* EXAMPLES *)
@ -120,7 +112,7 @@ Open Scope ladder_expr_scope.
Check [< ∀"α", (< $"Seq"$ %"α"% > ~ < $"List"$ %"α"% >) >].
Definition polymorphic_identity1 : expr_term := [{ Λ"T" ↦ λ"x"%"T"% ↦ (%"x"%) }].
Definition polymorphic_identity1 : expr_term := [{ Λ"T" ↦ λ"x"%"T"% ↦ %"x"% }].
Definition polymorphic_identity2 : expr_term := [{ Λ"T" ↦ λ"y"%"T"% ↦ %"y"% }].
Compute polymorphic_identity1.

250
coq/typing.v
View file

@ -6,55 +6,64 @@ Require Import terms.
Require Import subst.
Require Import equiv.
Require Import subtype.
Require Import context.
Require Import morph.
Include Terms.
Include Subst.
Include Equiv.
Include Subtype.
Include Context.
Include Morph.
Module Typing.
(** Typing Derivation *)
Inductive context : Type :=
| ctx_assign : string -> type_term -> context -> context
| ctx_empty : context
.
Inductive context_contains : context -> string -> type_term -> Prop :=
| C_take : forall (x:string) (X:type_term) (Γ:context),
(context_contains (ctx_assign x X Γ) x X)
| C_shuffle : forall x X y Y Γ,
(context_contains Γ x X) ->
(context_contains (ctx_assign y Y Γ) x X).
Reserved Notation "Gamma '|-' x '\is' X" (at level 101, x at next level, X at level 0).
Reserved Notation "Gamma '|-' x '\compatible' X" (at level 101, x at next level, X at level 0).
Inductive expr_type : context -> expr_term -> type_term -> Prop :=
| T_Var : forall Γ x τ,
(context_contains Γ x τ) ->
(Γ |- (expr_var x) \is τ)
| T_Let : forall Γ s σ t τ x,
| T_Let : forall Γ s (σ:type_term) t τ x,
(Γ |- s \is σ) ->
((ctx_assign x σ Γ) |- t \is τ) ->
(Γ |- (expr_let x s t) \is τ)
(Γ |- t \is τ) ->
(Γ |- (expr_let x σ s t) \is τ)
| T_TypeAbs : forall Γ e τ α,
| T_TypeAbs : forall Γ (e:expr_term) (τ:type_term) α,
Γ |- e \is τ ->
Γ |- (expr_ty_abs α e) \is (type_univ α τ)
| T_TypeApp : forall Γ α e σ τ τ',
| T_TypeApp : forall Γ α (e:expr_term) (σ:type_term) (τ:type_term),
Γ |- e \is (type_univ α τ) ->
(type_subst1 α σ τ τ') ->
Γ |- (expr_ty_app e σ) \is τ'
Γ |- (expr_ty_app e σ) \is (type_subst α σ τ)
| T_Abs : forall Γ x σ t τ,
((ctx_assign x σ Γ) |- t \is τ) ->
(Γ |- (expr_abs x σ t) \is (type_fun σ τ))
| T_Abs : forall (Γ:context) (x:string) (σ:type_term) (t:expr_term) (τ:type_term),
(context_contains Γ x σ) ->
Γ |- t \is τ ->
Γ |- (expr_abs x σ t) \is (type_fun σ τ)
| T_App : forall (Γ:context) (f:expr_term) (a:expr_term) (σ:type_term) (τ:type_term),
Γ |- f \is (type_fun σ τ) ->
Γ |- a \is σ ->
Γ |- (expr_app f a) \is τ
| T_MorphAbs : forall Γ x σ e τ,
((ctx_assign x σ Γ) |- e \is τ) ->
(context_contains Γ x σ) ->
Γ |- e \is τ ->
Γ |- (expr_morph x σ e) \is (type_morph σ τ)
| T_App : forall Γ f a σ' σ τ,
(Γ |- f \is (type_fun σ τ)) ->
(Γ |- a \is σ') ->
(Γ |- σ' ~> σ) ->
(Γ |- (expr_app f a) \is τ)
| T_MorphFun : forall Γ f σ τ,
Γ |- f \is (type_morph σ τ) ->
Γ |- f \is (type_fun σ τ)
@ -64,111 +73,84 @@ Inductive expr_type : context -> expr_term -> type_term -> Prop :=
(τ' :<= τ) ->
(Γ |- (expr_ascend τ' e) \is τ')
| T_DescendImplicit : forall Γ x τ τ',
| T_Descend : forall Γ x τ τ',
Γ |- x \is τ ->
(τ :<= τ') ->
Γ |- x \is τ'
| T_Descend : forall Γ x τ τ',
Γ |- x \is τ ->
(τ :<= τ') ->
Γ |- (expr_descend τ' x) \is τ'
where "Γ '|-' x '\is' τ" := (expr_type Γ x τ).
Inductive expr_type_compatible : context -> expr_term -> type_term -> Prop :=
| TCompat_Native : forall Γ e τ,
(Γ |- e \is τ) ->
(Γ |- e \compatible τ)
| TCompat_Let : forall Γ s (σ:type_term) t τ x,
(Γ |- s \is σ) ->
(context_contains Γ x σ) ->
(Γ |- t \compatible τ) ->
(Γ |- (expr_let x σ s t) \compatible τ)
| T_CompatTypeApp : forall Γ α (e:expr_term) (σ:type_term) (τ:type_term),
Γ |- e \compatible (type_univ α τ) ->
Γ |- (expr_ty_app e σ) \compatible (type_subst α σ τ)
| TCompat_App : forall Γ f a σ τ,
(Γ |- f \compatible (type_fun σ τ)) ->
(Γ |- a \compatible σ) ->
(Γ |- (expr_app f a) \compatible τ)
| TCompat_Morph : forall Γ h x τ τ',
(context_contains Γ h (type_morph τ τ')) ->
(Γ |- x \compatible τ) ->
(Γ |- x \compatible τ')
| TCompat_Sub : forall Γ x τ τ',
(Γ |- x \compatible τ) ->
(τ ~<= τ') ->
(Γ |- x \compatible τ')
where "Γ '|-' x '\compatible' τ" := (expr_type_compatible Γ x τ).
Definition is_well_typed (e:expr_term) : Prop :=
exists Γ τ,
Γ |- e \is τ
Γ |- e \compatible τ
.
Inductive translate_typing : context -> expr_term -> type_term -> expr_term -> Prop :=
| Expand_Var : forall Γ x τ,
(Γ |- (expr_var x) \is τ) ->
(translate_typing Γ (expr_var x) τ (expr_var x))
| Expand_Let : forall Γ x e e' t t' σ τ,
(Γ |- e \is σ) ->
((ctx_assign x σ Γ) |- t \is τ) ->
(translate_typing Γ e σ e') ->
(translate_typing (ctx_assign x σ Γ) t τ t') ->
(translate_typing Γ (expr_let x e t) τ (expr_let x e' t'))
| Expand_TypeAbs : forall Γ α e e' τ,
(Γ |- e \is τ) ->
(translate_typing Γ e τ e') ->
(translate_typing Γ
(expr_ty_abs α e)
(type_univ α τ)
(expr_ty_abs α e'))
| Expand_TypeApp : forall Γ e e' σ α τ,
(Γ |- e \is (type_univ α τ)) ->
(translate_typing Γ e τ e') ->
(translate_typing Γ (expr_ty_app e τ) (type_subst α σ τ) (expr_ty_app e' τ))
| Expand_Abs : forall Γ x σ e e' τ,
((ctx_assign x σ Γ) |- e \is τ) ->
(Γ |- (expr_abs x σ e) \is (type_fun σ τ)) ->
(translate_typing (ctx_assign x σ Γ) e τ e') ->
(translate_typing Γ (expr_abs x σ e) (type_fun σ τ) (expr_abs x σ e'))
| Expand_MorphAbs : forall Γ x σ e e' τ,
((ctx_assign x σ Γ) |- e \is τ) ->
(Γ |- (expr_abs x σ e) \is (type_fun σ τ)) ->
(translate_typing (ctx_assign x σ Γ) e τ e') ->
(translate_typing Γ (expr_morph x σ e) (type_morph σ τ) (expr_morph x σ e'))
| Expand_App : forall Γ f f' a a' m σ τ σ',
(Γ |- f \is (type_fun σ τ)) ->
(Γ |- a \is σ') ->
(Γ |- σ' ~> σ) ->
(translate_typing Γ f (type_fun σ τ) f') ->
(translate_typing Γ a σ' a') ->
(translate_morphism_path Γ σ' σ m) ->
(translate_typing Γ (expr_app f a) τ (expr_app f' (expr_app m a')))
| Expand_MorphFun : forall Γ f f' σ τ,
(Γ |- f \is (type_morph σ τ)) ->
(Γ |- f \is (type_fun σ τ)) ->
(translate_typing Γ f (type_morph σ τ) f') ->
(translate_typing Γ f (type_fun σ τ) f')
| Expand_Ascend : forall Γ e e' τ τ',
(Γ |- e \is τ) ->
(τ' :<= τ) ->
(Γ |- (expr_ascend τ' e) \is τ') ->
(translate_typing Γ e τ e') ->
(translate_typing Γ (expr_ascend τ' e) τ' (expr_ascend τ' e'))
| Expand_Descend : forall Γ e e' τ τ',
(Γ |- e \is τ) ->
(τ :<= τ') ->
(Γ |- e \is τ') ->
(translate_typing Γ e τ e') ->
(translate_typing Γ e τ' e')
Definition is_exactly_typed (e:expr_term) : Prop :=
exists Γ τ,
Γ |- e \is τ
.
(* Examples *)
Example typing1 :
ctx_empty |- [{ Λ"T" ↦ λ "x" %"T"% ↦ %"x"% }] \is [< ∀"T", %"T"% -> %"T"% >].
forall Γ,
(context_contains Γ "x" [< %"T"% >]) ->
Γ |- [{ Λ"T" ↦ λ "x" %"T"% ↦ %"x"% }] \is [< ∀"T", %"T"% -> %"T"% >].
(* Γ |- [ ΛT ↦ λx:T ↦ x ] : ∀T.(T->T) *)
Proof.
intros.
apply T_TypeAbs.
apply T_Abs.
apply H.
apply T_Var.
apply C_take.
apply H.
Qed.
Example typing2 :
ctx_empty |- [{ Λ"T" ↦ λ "x" %"T"% ↦ %"x"% }] \is [< ∀"U", %"U"% -> %"U"% >].
forall Γ,
(context_contains Γ "x" [< %"T"% >]) ->
Γ |- [{ Λ"T" ↦ λ "x" %"T"% ↦ %"x"% }] \is [< ∀"U", %"U"% -> %"U"% >].
Proof.
intros.
apply T_DescendImplicit with (τ:=[< ∀"T",(%"T"% -> %"T"%) >]).
apply T_Descend with (τ:=[< ∀"T",(%"T"% -> %"T"%) >]).
apply T_TypeAbs.
apply T_Abs.
apply H.
apply T_Var.
apply C_take.
apply H.
apply TSubRepr_Refl.
apply TEq_Alpha.
@ -179,18 +161,22 @@ Proof.
Qed.
Example typing3 :
ctx_empty |- [{
forall Γ,
(context_contains Γ "x" [< %"T"% >]) ->
(context_contains Γ "y" [< %"U"% >]) ->
Γ |- [{
Λ"T" ↦ Λ"U" ↦ λ"x" %"T"% ↦ λ"y" %"U"% ↦ %"y"%
}] \is [<
∀"S",∀"T",(%"S"%->%"T"%->%"T"%)
>].
Proof.
intros.
apply T_DescendImplicit with (τ:=[< ∀"T",∀"U",(%"T"%->%"U"%->%"U"%) >]) (τ':=[< ∀"S",∀"T",(%"S"%->%"T"%->%"T"%) >]).
apply T_Descend with (τ:=[< ∀"T",∀"U",(%"T"%->%"U"%->%"U"%) >]) (τ':=[< ∀"S",∀"T",(%"S"%->%"T"%->%"T"%) >]).
apply T_TypeAbs, T_TypeAbs, T_Abs.
apply H.
apply T_Abs.
apply T_Var.
apply C_take.
apply H0.
apply T_Var, H0.
apply TSubRepr_Refl.
apply TEq_Trans with (y:= [< ∀"S",∀"U",(%"S"%->%"U"%->%"U"%) >] ).
@ -214,70 +200,24 @@ Proof.
apply TSubst_VarReplace.
Qed.
Example typing4 : (is_well_typed
[{ Λ"T" ↦ Λ"U" ↦ λ"x" %"T"% ↦ λ"y" %"U"% ↦ %"x"% }]
).
Proof.
unfold is_well_typed.
exists ctx_empty.
exists (ctx_assign "x" [< %"T"% >]
(ctx_assign "y" [< %"U"% >] ctx_empty)).
exists [< ∀"T",∀"U",%"T"%->%"U"%->%"T"% >].
apply TCompat_Native.
apply T_TypeAbs.
apply T_TypeAbs.
apply T_Abs.
apply C_take.
apply T_Abs.
apply T_Var.
apply C_shuffle, C_take.
Qed.
Open Scope ladder_expr_scope.
Example typing5 : (is_well_typed
[{
let "deg2turns" :=
(λ"x" $"Angle"$~$"Degrees"$~$"ℝ"$
↦morph (((%"/"% %"x"%) %"360"%) as $"Angle"$~$"Turns"$~$"ℝ"$))
in ( %"deg2turns"% (%"60"% as $"Angle"$~$"Degrees"$~$"ℝ"$) )
}]
).
Proof.
unfold is_well_typed.
exists (ctx_assign "60" [< $"ℝ"$ >]
(ctx_assign "360" [< $"ℝ"$ >]
(ctx_assign "/" [< $"ℝ"$ -> $"ℝ"$ -> $"ℝ"$ >]
ctx_empty))).
exists [< $"Angle"$~$"Turns"$~$"ℝ"$ >].
apply T_Let with (σ:=[< $"Angle"$~$"Degrees"$~$"ℝ"$ ->morph $"Angle"$~$"Turns"$~$"ℝ"$ >]).
apply T_MorphAbs.
apply T_Ascend with (τ:=[< $"ℝ"$ >]).
apply T_App with (σ := [< $"ℝ"$ >]) (σ' := [< $"ℝ"$ >]).
apply T_App with (σ := [< $"ℝ"$ >]) (σ' := [< $"ℝ"$ >]).
apply T_Var.
apply C_shuffle. apply C_shuffle. apply C_shuffle. apply C_take.
apply T_DescendImplicit with (τ := [< $"Angle"$~$"Degrees"$~$"ℝ"$ >]).
apply T_Var.
apply C_take.
apply TSubRepr_Ladder. apply TSubRepr_Ladder.
apply TSubRepr_Refl. apply TEq_Refl.
apply M_Sub.
apply TSubRepr_Refl. apply TEq_Refl.
apply T_Var.
apply C_shuffle, C_shuffle, C_take.
apply M_Sub.
apply TSubRepr_Refl.
apply TEq_Refl.
apply TSubRepr_Ladder, TSubRepr_Ladder, TSubRepr_Refl.
apply TEq_Refl.
apply T_App with (σ:=[<$"Angle"$~$"Degrees"$~$"ℝ"$>]) (σ':=[<$"Angle"$~$"Degrees"$~$"ℝ"$>]).
apply T_MorphFun.
apply T_Var.
apply C_take.
apply T_Ascend with (τ:=[<$"ℝ"$>]).
apply T_Var.
apply C_shuffle. apply C_take.
apply TSubRepr_Ladder.
apply TSubRepr_Ladder.
apply TSubRepr_Refl. apply TEq_Refl.
apply M_Sub. apply TSubRepr_Refl. apply TEq_Refl.
apply T_Var.
apply C_take.
Qed.
End Typing.

91
paper/main.tex
View file

@ -518,23 +518,17 @@ while preserving its semantics.
\end{enumerate}
\end{example}
\subsubsection{Typing Context}
\subsubsection{Inference of Expression Types}
As usual, the typing-context \(\Gamma = \{ \metavariable{x_1} : \metavariable{\tau_1} , \quad \metavariable{x_2} : \metavariable{\tau_2} , \quad \ldots \}\)
is a finite mapping which assigns variables \(\metavariable{x_i} \in \exprvars\) to types \(\metavariable{\tau_i} \in \nonterm{T}\).
%Using the inference rules given in \ref{def:pathrules} \ref{def:typerules}, further typing-judgements
%of the form \(\Gamma \vdash \metavariable{e} : \metavariable{\tau} \quad\) read as "expression \(\metavariable{e}\) is of type \(\metavariable{\tau}\)"
%can be derived from the context \(\Gamma\) where \(\metavariable{e} \in \nonterm{E}\) and \(\metavariable{\tau} \in \nonterm{T}\).
\subsubsection{Morphism Graph}
Every typing context \(\Gamma\) implies a \emph{Morphism Graph}, a directed graph whose vertices are types
and the edges represent a type-transformations, as defined by morphisms.
A type \(\metavariable{\tau}\) can be implicitly coerced into a type \(\metavariable{\tau'}\),
provided there is a path from \(\metavariable{\tau}\) to \(\metavariable{\tau'}\) in the \emph{Morphism-Graph} of \(\Gamma\),
written as \(\Gamma \vdash \metavariable{\tau} \leadsto \metavariable{\tau'}\).
Using the inference rules given in \ref{def:typerules}, further typing-judgements
of the form \(\Gamma \vdash \metavariable{e} : \metavariable{\tau} \quad\) read as "expression \(\metavariable{e}\) is of type \(\metavariable{\tau}\)"
can be derived from the context \(\Gamma\) where \(\metavariable{e} \in \nonterm{E}\) and \(\metavariable{\tau} \in \nonterm{T}\).
\begin{definition}[Morphism Paths]
Given a typing context \(\Gamma\), any type \(\metavariable{\tau}\) can be transformed into \(\metavariable{\tau'}\), provided there is a path from \(\metavariable{\tau}\) to \(\metavariable{\tau'}\) in the \emph{Morphism-Graph} of \(\Gamma\), written as \(\Gamma \vdash \metavariable{\tau} \leadsto \metavariable{\tau'}\).
\label{def:pathrules}
\begin{mathpar}
@ -789,20 +783,6 @@ D_1
\and
\Big{\llbracket}
\inferrule[T-MorphAbs]{
D_1 :: \Gamma,\metavariable{x}:\metavariable{\tau} \vdash \metavariable{e} : \metavariable{\tau'} \\
\metavariable{\tau} \precsim \metavariable{\tau'}
}{
\Gamma \vdash (\exprterminal{\lambda} \metavariable{x} \exprterminal{:} \metavariable{\tau} \exprterminal{\mapsto_{morph}} \metavariable{e}) : \metavariable{\tau}\typeterminal{\rightarrow_\text{morph}}\metavariable{\tau'}
}
\Big{\rrbracket} =
\exprterminal{\lambda} \metavariable{x} \exprterminal{:} \metavariable{\tau}
\exprterminal{\mapsto_\text{morph}} \Big{\llbracket}D_1\Big{\rrbracket}
\and
\Big{\llbracket}
\inferrule[T-App]{
D_1 :: \Gamma \vdash \metavariable{f} : \metavariable{\sigma} \typeterminal{\rightarrow} \metavariable{\tau}\\
@ -925,17 +905,16 @@ Evaluation of an expression \(\metavariable{e} \in \nonterm{E}\) is defined by e
\rightarrow_\beta
\{ \metavariable{x} \mapsto \metavariable{a} \} \metavariable{e}
}
\inferrule[E-AppLamAscribe]{
}{
\exprterminal{(( \lambda \metavariable{x}:\metavariable{\sigma} \mapsto \metavariable{e} )}
\exprterminal{( \lambda \metavariable{x}:\metavariable{\sigma} \mapsto \metavariable{e} )}
\exprterminal{\text{ as }}
\typeterminal{\metavariable{\tau}}
\exprterminal{)}
\metavariable{a}
\metavariable{e}
\rightarrow_\beta
\exprterminal{( \lambda \metavariable{x}:\metavariable{\sigma} \mapsto \metavariable{e} )}
\metavariable{a}
\metavariable{v}
\metavariable{e}
}
\end{mathpar}
\end{definition}
@ -945,13 +924,10 @@ Evaluation of an expression \(\metavariable{e} \in \nonterm{E}\) is defined by e
\begin{lemma}[Preservation]
\label{lemma:preservation}
Assume the expression \(\metavariable{e}\) is well typed,
i.e. there is a type-derivation tree
\(D :: \Gamma \vdash \metavariable{e} : \metavariable{\tau}\)
for some type \(\metavariable{\tau}\) and context \(\Gamma\).
Then forall \(\metavariable{e'}\) with \(\llbracket D \rrbracket \rightarrow_{\beta} \metavariable{e'}\)
it holds that \(\Gamma \vdash \metavariable{e'} : \metavariable{\tau}\) as well.
Assume the expression \(\metavariable{e}\) is well typed, i.e. \(\emptyset \vdash \metavariable{e} : \metavariable{\tau}\)
for some type \(\metavariable{\tau}\).
Then forall \(\metavariable{e'}\) with \(\metavariable{e} \rightarrow_{\beta} \metavariable{e'}\)
it holds that \(\emptyset \vdash \metavariable{e'} : \metavariable{\tau}\) as well.
\begin{proof}
\todo{}
@ -960,31 +936,38 @@ it holds that \(\Gamma \vdash \metavariable{e'} : \metavariable{\tau}\) as well.
\begin{lemma}[Progress]
\label{lemma:progress}
Assume the expression \(\metavariable{e}\) is well typed,
i.e. there is a type-derivation tree
\(D :: \Gamma \vdash \metavariable{e} : \metavariable{\tau}\)
for some type \(\metavariable{\tau}\) and context \(\Gamma\).
Then either \(\metavariable{e}\) is a value
or there exists some \(\metavariable{e'}\) such that \(\llbracket D \rrbracket \rightarrow_{\beta} \metavariable{e'}\)
If \(\emptyset \vdash \metavariable{e} : \metavariable{\tau}\),
then either \(\metavariable{e}\) is a value
or there exists some \(\metavariable{e'}\) such that \(\metavariable{e} \rightarrow_{\beta} \metavariable{e'}\)
\begin{proof}
\todo{}
\end{proof}
\end{lemma}
\begin{theorem}[Soundness]
\label{theorem:semantic-soundness}
No well-typed expression is stuck.
\begin{theorem}[Syntactic Type Soundness]
\label{theorem:syntactic-soundness}
No syntactically well-typed expression is stuck.
Assume the typing derivation \(D :: \Gamma \vdash \metavariable{e}:\metavariable{\tau}\).
Assume the typing derivation \(D :: \emptyset \vdash \metavariable{e}:\metavariable{\tau}\).
Then it never occurs that \(\metavariable{e} \rightarrow_{\beta}^{*} \metavariable{e'}\) where \metavariable{e'} is in normal form but not a value.
\begin{proof}
Follows from \ref{lemma:progress} and \ref{lemma:preservation}.
\end{proof}
\end{theorem}
\begin{theorem}[Semantic Type Soundness]
\label{theorem:semantic-soundness}
No semantically well-typed expression is stuck.
Assume the typing derivation \(D :: \emptyset \vdash \metavariable{e}:\approx\metavariable{\tau}\).
Then it never occurs that \(\llbracket D \rrbracket \rightarrow_{\beta}^{*} \metavariable{e'}\) where \metavariable{e'} is in normal form but not a value.
\begin{proof}
\todo{}
%Assume the typing derivation \(D :: \Gamma \vdash \metavariable{e}:\approx\metavariable{\tau}\).
%By \ref{lemma:translation}, \(\Gamma \vdash \llbracket D \rrbracket : \metavariable{\tau}\)
%and thus it follows by \ref{theorem:syntactic-soundness} that \metavariable{e} is not stuck.
Assume the typing derivation \(D :: \emptyset \vdash \metavariable{e}:\approx\metavariable{\tau}\).
By \ref{lemma:translation}, \(\emptyset \vdash \llbracket D \rrbracket : \metavariable{\tau}\)
and thus it follows by \ref{theorem:syntactic-soundness} that \metavariable{e} is not stuck.
\end{proof}
\end{theorem}