Novembre 2018 - Typer - mailman.iro.umontreal.ca

[Git][monnier/typer][master] * samples/hurkens.typer: Add a few comments.
by Stefan 23 Nov '18

23 Nov '18

Stefan pushed to branch master at Stefan / Typer Commits: 749381e0 by Stefan Monnier at 2018-11-23T22:51:34Z * samples/hurkens.typer: Add a few comments. - - - - - 1 changed file: - samples/hurkens.typer Changes: ===================================== samples/hurkens.typer ===================================== @@ -21,13 +21,25 @@ * = Type; \square = Type1; -%% p (S) = (S -> *); FIXME: internal error! +%% 𝓅 is the "powerset". +%% 𝓅 S = (S -> *); FIXME: internal error! 𝓅 : \square -> \square; 𝓅 (S : \square) = (S -> Type); 𝓅𝓅 S = 𝓅 (𝓅 S); +%%%% A "powerful" universe (U, σ, τ). +%% We need that ∀ C : 𝓅𝓅 U +%% +%% σ(τ C) = {X | {y|τ(σ y) ∈ X} ∈ C} +%% +%% i.o.w +%% +%% (σ ∘ τ) = (τ ∘ σ)** +%% +%% where * is ... + U : \square; -U = (X : \square) ≡> (𝓅𝓅 X -> X) -> 𝓅𝓅 X; +U = (X : \square) ≡> (𝓅𝓅 X -> X) -> 𝓅𝓅 X; % Uses the (▵,□,□) rule! τ : 𝓅𝓅 U -> U; τ t = lambda (X : \square) @@ -38,29 +50,41 @@ U = (X : \square) ≡> (𝓅𝓅 X -> X) -> 𝓅𝓅 X; σ : U -> 𝓅𝓅 U; σ (s : U) = (s (X := U) (lambda (t : 𝓅𝓅 U) -> τ t)); +τσ y = τ (σ y); +%% στ x = σ (τ x); + Δ : 𝓅 U; -Δ = lambda (y : U) -> ¬((p : 𝓅 U) ≡> σ y p -> p (τ (σ y))); +Δ = lambda (y : U) -> ¬((p : 𝓅 U) ≡> σ y p -> p (τσ y)); +%% Ω = τ {X | X is inductive} Ω : U; Ω = τ (lambda (p : 𝓅 U) -> ((y : U) ≡> σ y p -> p y)); -boom1 : ((p : 𝓅 U) ≡> ((y : U) ≡> σ y p -> p y) -> p Ω) -> ⊥; +%%%% Proof that Ω is both well-founded and not + +%% FIXME: Not sure if this means well-founded or the opposite! +well-founded = ((p : 𝓅 U) ≡> ((y : U) ≡> σ y p -> p y) -> p Ω); + +boom1 : ¬ well-founded; boom1 = lambda (v0 : (p : 𝓅 U) ≡> ((y : U) ≡> σ y p -> p y) -> p Ω) -> v0 (p := Δ) (lambda (y : U) ≡> lambda (v2 : σ y Δ) -> - lambda (v3 : (p : 𝓅 U) ≡> σ y p -> p (τ (σ y))) + lambda (v3 : (p : 𝓅 U) ≡> σ y p -> p (τσ y)) -> v3 (p := Δ) v2 (lambda (p : 𝓅 U) - ≡> v3 (p := lambda (y : U) -> p (τ (σ y))))) - (lambda (p : 𝓅 U) ≡> v0 (p := lambda (y : U) -> p (τ (σ y)))); + ≡> v3 (p := lambda (y : U) -> p (τσ y)))) + (lambda (p : 𝓅 U) ≡> v0 (p := lambda (y : U) -> p (τσ y))); -boom2 : (p : 𝓅 U) ≡> ((y : U) ≡> σ y p -> p y) -> p Ω; +boom2 : well-founded; boom2 = lambda (p : 𝓅 U) ≡> lambda (v1 : (y : U) ≡> σ y p -> p y) -> v1 (y := Ω) - (lambda (y : U) ≡> v1 (y := τ (σ y))); + %% FIXME: (lambda (x : U) ≡> v1 (y := τσ x)) + %% signals a spurious "DeBruijn index 1 refers to wrong name. + %% Expected: `y` got `x`". + (lambda (y : U) ≡> v1 (y := τσ y)); %% FIXME: Defining `boom` as below inf-loops, which I believe is a bug %% (call it an accidental feature)! View it on GitLab: https://gitlab.com/monnier/typer/commit/749381e080170dc733ee71b977f14a6b3f2… -- View it on GitLab: https://gitlab.com/monnier/typer/commit/749381e080170dc733ee71b977f14a6b3f2… You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer][master] * samples/hurkens.typer: New file.
by Stefan 23 Nov '18

23 Nov '18

Stefan pushed to branch master at Stefan / Typer Commits: ae543b55 by Stefan Monnier at 2018-11-23T21:43:09Z * samples/hurkens.typer: New file. - - - - - 4 changed files: - btl/builtins.typer - + samples/hurkens.typer - src/builtin.ml - src/eval.ml Changes: ===================================== btl/builtins.typer ===================================== @@ -31,6 +31,9 @@ %%%% Base Types used in builtin functions +%% TypeLevel_succ = Built-in "TypeLevel.succ" : TypeLevel -> TypeLevel; +%% TypeLevel_⊔ = Built-in "TypeLevel.⊔" : TypeLevel -> TypeLevel -> TypeLevel; + %% The trivial type which carries no information. Unit = typecons Unit unit; unit = datacons Unit unit; @@ -423,10 +426,10 @@ Test_info = Built-in "Test.info" : String -> String -> IO Unit; %% Test_location = Built-in "Test.location" : Unit -> String; -%%% -%%% Do some test which print a message: "[ OK]" or "[FAIL]" -%%% followed by a message passed as argument -%%% +%% +%% Do some test which print a message: "[ OK]" or "[FAIL]" +%% followed by a message passed as argument +%% %% %% Takes a message and a boolean which should be true ===================================== samples/hurkens.typer ===================================== @@ -0,0 +1,71 @@ +%%% hurkens.typer --- Hurken's paradox + +%%% Commentary: + +%% @InProceedings{Hurkens95, +%% author = {Antonius Hurkens}, +%% title = {A simplification of {G}irard's paradox}, +%% crossref = {TLCA95}, +%% url = {http://www.cs.cmu.edu/~kw/scans/hurkens95tlca.pdf}, +%% pages = {266-278} +%% } + +%%% Code: + +⊥ : Type; +⊥ = (p : Type) ≡> p; + +¬ : Type -> Type; +¬ t = t -> ⊥; + +* = Type; +\square = Type1; + +%% p (S) = (S -> *); FIXME: internal error! +𝓅 : \square -> \square; +𝓅 (S : \square) = (S -> Type); +𝓅𝓅 S = 𝓅 (𝓅 S); + +U : \square; +U = (X : \square) ≡> (𝓅𝓅 X -> X) -> 𝓅𝓅 X; + +τ : 𝓅𝓅 U -> U; +τ t = lambda (X : \square) + ≡> lambda (f : (𝓅𝓅 X) -> X) + -> lambda (p : 𝓅 X) + -> t (lambda (y : U) -> p (f ((y (X := X) f)))); + +σ : U -> 𝓅𝓅 U; +σ (s : U) = (s (X := U) (lambda (t : 𝓅𝓅 U) -> τ t)); + +Δ : 𝓅 U; +Δ = lambda (y : U) -> ¬((p : 𝓅 U) ≡> σ y p -> p (τ (σ y))); + +Ω : U; +Ω = τ (lambda (p : 𝓅 U) -> ((y : U) ≡> σ y p -> p y)); + +boom1 : ((p : 𝓅 U) ≡> ((y : U) ≡> σ y p -> p y) -> p Ω) -> ⊥; +boom1 = lambda (v0 : (p : 𝓅 U) ≡> ((y : U) ≡> σ y p -> p y) -> p Ω) + -> v0 (p := Δ) + (lambda (y : U) ≡> + lambda (v2 : σ y Δ) -> + lambda (v3 : (p : 𝓅 U) ≡> σ y p -> p (τ (σ y))) + -> v3 (p := Δ) + v2 + (lambda (p : 𝓅 U) + ≡> v3 (p := lambda (y : U) -> p (τ (σ y))))) + (lambda (p : 𝓅 U) ≡> v0 (p := lambda (y : U) -> p (τ (σ y)))); + +boom2 : (p : 𝓅 U) ≡> ((y : U) ≡> σ y p -> p y) -> p Ω; +boom2 = lambda (p : 𝓅 U) + ≡> lambda (v1 : (y : U) ≡> σ y p -> p y) + -> v1 (y := Ω) + (lambda (y : U) ≡> v1 (y := τ (σ y))); + +%% FIXME: Defining `boom` as below inf-loops, which I believe is a bug +%% (call it an accidental feature)! +%%boom : ⊥; +%%boom = boom1 boom2; + + +%%% hurkens.typer ends here. ===================================== src/builtin.ml ===================================== @@ -152,7 +152,7 @@ let new_builtin_type name kind = let register_builtin_csts () = add_builtin_cst "TypeLevel" DB.type_level; - add_builtin_cst "TypeLevel.z" DB.level0; + add_builtin_cst "TypeLevel_z" DB.level0; add_builtin_cst "Type" DB.type0; add_builtin_cst "Type1" DB.type1; add_builtin_cst "Int" DB.type_int; ===================================== src/eval.ml ===================================== @@ -973,16 +973,27 @@ let test_neq loc depth args_val = match args_val with ttrue) | _ -> error loc "Test.neq takes a String and two values as argument" +let typelevel_succ loc (depth : eval_debug_info) (args_val: value_type list) = + match args_val with + | [Vint v] -> Vint(v + 1) + | _ -> error loc ("`Typlevel.succ` expects 1 TypeLevel argument") +let typelevel_lub loc (depth : eval_debug_info) (args_val: value_type list) = + match args_val with + | [Vint v1; Vint v2] -> Vint(max v1 v2) + | _ -> error loc ("`Typlevel.⊔` expects 2 TypeLevel argument2") + let register_builtin_functions () = List.iter (fun (name, f, arity) -> add_builtin_function name f arity) [ - ("Sexp.block" , make_block, 1); + ("Sexp.block" , make_block, 1); ("Sexp.symbol" , make_symbol, 1); ("Sexp.string" , make_string, 1); ("Sexp.integer" , make_integer, 1); ("Sexp.float" , make_float, 1); ("Sexp.node" , make_node, 2); ("Sexp.dispatch" , sexp_dispatch, 7); + ("TypeLevel.succ" , typelevel_succ, 1); + ("TypeLevel.⊔" , typelevel_lub, 2); ("Parser.default", parser_default,1); ("Parser.custom" , parser_custom,2); ("Parser.newest" , parser_newest,1); View it on GitLab: https://gitlab.com/monnier/typer/commit/ae543b55a78b4cf86c6b90d344eeb6ab268… -- View it on GitLab: https://gitlab.com/monnier/typer/commit/ae543b55a78b4cf86c6b90d344eeb6ab268… You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer] Deleted branch report/selit
by Stefan 19 Nov '18

19 Nov '18

Stefan deleted branch report/selit at Stefan / Typer -- You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer][report/itd] -
by Stefan 17 Nov '18

17 Nov '18

Stefan pushed to branch report/itd at Stefan / Typer Commits: 556c1ffa by Stefan Monnier at 2018-11-17T06:40:11Z - - - - - - 1 changed file: - paper.tex Changes: ===================================== paper.tex ===================================== @@ -1531,13 +1531,21 @@ system differs from that of~\citet{Gimenez94} in the following aspects: \newcommand \TIrefl {\kw{refl}~} \newcommand \TIJ[3] {\kw{J}~#1~#2~#3} -\begin{figure} +\begin{figure}[tb] \begin{displaymath} \begin{array}{l@{\;=\;}l} \TIUnit & \Tind{x}{\Type0}{x} \\ \TIunit & \Tcon{0}{\TIUnit} \\ \TIPair{x}{\tau_1}{\tau_2} & \Tind{y}{\Type?}{\Tarw{x}{\tau_1}{\Tsarw{\tau_2}{y}}} \\ \TIpair{x}{e_1}{e_2}{\tau_2} & \Tcon{0}{\TIPair{x}{\,?}{\tau_2}}~e_1~e_2 \\ + \TIproj 1 e & + \TIcase{\Tlam{\_}{\,?}{\tau_1}}{e}{?}{\Tlam{x}{\,?}{\Tlam{\_}{\,?}{x}}} + %% \;\;\;\;\text{where }\Jtype{e}{\TIPair{x}{\tau_1}{\tau_2}} + \\ + \TIproj 2 e & + \TIcase{\Tlam{x_e}{\,?}%% {\TIPair{x}{\tau_1}{\tau_2}} + {\Tapp{(\Tlam{x}{\,?}{\tau_2})}{(\TIproj 1 x_e)}}} + {e}{?}{\Tlam{\_}{\,?}{\Tlam{x}{\,?}{x}}} \\ \TIeq{e_1} & \Tind{x}{\,\Tsarw{?}{x}}{\Tapp{x}{e_1}} \\ \TIrefl{e_1} & \Tcon{0}{\TIeq{e_1}} \\ \TIJ{e_\equiv}{e_f}{e} & @@ -1564,6 +1572,11 @@ system differs from that of~\citet{Gimenez94} in the following aspects: \;\;\;\;\;\;\;\text{if }\Jsubtype {\tau_1}{\tau_3} \end{array} \end{displaymath} + \caption{Auxiliary definitions used to map CUC to CIC.} + \label{fig:cuc-to-cic-aux} +\end{figure} + +\begin{figure} \begin{displaymath} \begin{array}{l@{\;=\;}l} \Ftocic x & x \\ @@ -1597,21 +1610,24 @@ system differs from that of~\citet{Gimenez94} in the following aspects: }} \\ \Ftocic {\Tapp{(\Tlam x {\tau_1} {e_1})}{\Tproj {e_2} i}} & \MAlign{ - \TIcase {\Tlam \_ {\tau_{e_2}} {?}} {e_2} {?} - {\Tlam {x_0} {\tau_0} {\Tlam {y} {\Ftocic{\Tuple \Delta}} {?}}} \\ + \Tapp{(\TIcase {\tau_r} {e_2} {?} + {b})} + {(\TIrefl{(\TIproj 1 {e_2})})} \\ \;\;\text{where } \MAlign{ - %% ¡¡FIXME: \tau_1 is not equal to the type of y.(i-1)!! - %% We can get a proof `P : x₀=π₁ e₂` and then use - %% `J P y` to get y' that will have the appropriate type, - %% but then \JIdecreasing will not know that y' is - %% smaller than e₂ so termination checking fails! \FIXME{Wow!} \\ + b = {\Tlam {x_0} {\tau_0} {\Tlam {y} {\Ftocic{\Tuple \Delta}} + {\textsl{body}}}} \\ + \textsl{body} = \Tlam{x_\equiv}{\Teq{x_0}{\TIproj 1 {e_2}}}{?} \\ e' = \Ftocic{\Tapp{(\Tlam x {\tau_1} {e_1})} {\Tproj {y} {(i - 1)}}} \\ \Jtype{e_2}{\tau_{e_2}} \text{ and }{\tau_{e_2} = \Tuple {x_0\:\tau_0,\Delta}} \\ - \Jtype[\Gamma,x\:\tau_1]{e_1}{\tau_2}}} + \Jtype[\Gamma,x\:\tau_1]{e_1}{\tau_2} \\ + \tau_r = \Tlam {x_e} {\,?} {\Tarw{\_} + {\Teq{\TIproj 1 {x_e}}{\TIproj 1 {e_2}}} + {\Subst{\tau_2}{\Ftocic{\Tproj {e_2}{i}}}{x}}} + }} \medskip \\ \Ftocic {\Teq{e_1}{e_2}} & \TIeq{\Ftocic{e_1}}~{\Ftocic{e_2}} \\ \Ftocic {\Trefl{e_1}} & \TIrefl{\Ftocic{e_1}} \\ View it on GitLab: https://gitlab.com/monnier/typer/commit/556c1ffa897f9f5322cc04578abef152170… -- View it on GitLab: https://gitlab.com/monnier/typer/commit/556c1ffa897f9f5322cc04578abef152170… You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer][report/itd] -
by Stefan 16 Nov '18

16 Nov '18

Stefan pushed to branch report/itd at Stefan / Typer Commits: 09881d77 by Stefan Monnier at 2018-11-16T23:25:42Z - - - - - - 1 changed file: - paper.tex Changes: ===================================== paper.tex ===================================== @@ -847,8 +847,8 @@ the explicit equality witnesses can be used to get the same effect. \Infer{\Jsubtype {\tau_1}{\tau_2}} {\Jsubtype {\tau_1}{\TUnion{\tau_2}{\tau_3}}} - \Infer{\Jsubtype {\tau_1}{\tau_2}} - {\Jsubtype {\tau_1}{\TUnion{\tau_3}{\tau_2}}} + \Infer{\Jsubtype {\tau_1}{\tau_3}} + {\Jsubtype {\tau_1}{\TUnion{\tau_2}{\tau_3}}} \Infer{\Jsubtype {\tau_1}{\tau_3} \\ {\Jsubtype {\tau_2}{\tau_3}}} {\Jsubtype {\TUnion{\tau_1}{\tau_2}}{\tau_3}} @@ -1044,6 +1044,12 @@ Section~\ref{sec:erasure}. \JUdecreasing {\{x\}\cup\nu} {e_1}} {\JUdecreasing \nu {\Tapp{(\Tlam x \tau {e_1})}{(\Tunfold{\_}{\_}{e_2})}}} + \Infer{e_2 = \Tapp{x_e}{\vec \_} \\ + \JUdecreasing {\nu} {e_2} \\ + x_e \in \nu \\ + \JUdecreasing {\{x\}\cup\nu} {e_1}} + {\JUdecreasing \nu {\Tapp{(\Tlam x \tau {e_1})}{(\TJ{\_}{\_}{e_2})}}} + \Infer{\JUdecreasing {\nu} {\tau_e} \\ \JUdecreasing {\nu} {\tau_r} \\ \JUdecreasing {\nu} {e} \\ @@ -1515,14 +1521,49 @@ system differs from that of~\citet{Gimenez94} in the following aspects: \subsection{CUC to CIC} -\newcommand \TIeither[2] {\id{Either}~#1~#2} -\newcommand \TIUnit {\id{Unit}} -\newcommand \TIunit {\id{unit}} +\newcommand \TIeither[2] {\kw{Either}~#1~#2} +\newcommand \TIUnit {\kw{Unit}} +\newcommand \TIunit {\kw{unit}} \newcommand \TIPair[3] {\Sigma #1\:#2. #3} -\newcommand \TIpair[2] {\id{dcons}~#1~#2} +\newcommand \TIpair[4] {\langle#1=#2,#3:#4\rangle} \newcommand \TIproj[2] {\pi_{#1}~#2} +\newcommand \TIeq[1] {\kw{eq}~#1} +\newcommand \TIrefl {\kw{refl}~} +\newcommand \TIJ[3] {\kw{J}~#1~#2~#3} \begin{figure} + \begin{displaymath} + \begin{array}{l@{\;=\;}l} + \TIUnit & \Tind{x}{\Type0}{x} \\ + \TIunit & \Tcon{0}{\TIUnit} \\ + \TIPair{x}{\tau_1}{\tau_2} & \Tind{y}{\Type?}{\Tarw{x}{\tau_1}{\Tsarw{\tau_2}{y}}} \\ + \TIpair{x}{e_1}{e_2}{\tau_2} & \Tcon{0}{\TIPair{x}{\,?}{\tau_2}}~e_1~e_2 \\ + \TIeq{e_1} & \Tind{x}{\,\Tsarw{?}{x}}{\Tapp{x}{e_1}} \\ + \TIrefl{e_1} & \Tcon{0}{\TIeq{e_1}} \\ + \TIJ{e_\equiv}{e_f}{e} & + \TIcase{\Tlam{x}{\,?}{\Tlam{\_}{\,?}{\Tapp{e_f}{x}}}}{e_\equiv}{}{e} \\ + \TIeither{\tau_1}{\tau_2} & \Tind{x}{\Type?}{\Tsarw{\tau_1}{x}, \Tsarw{\tau_1}{x}} \\ + \end{array} + \end{displaymath} + \begin{displaymath} + \begin{array}{l@{\;=\;}l} + \Ftocic{\Jsubtype \tau \tau} & \Tlam{x}{\tau}{x} \\ + \Ftocic{\Jsubtype {\TUnion{\tau_1}{\tau_2}} {\tau_3}} & + \MAlign{\Tlam{x}{\TIeither{\tau_1}{\tau_2}}{} \\ + \;\;\TIcase{\Tlam{\_}{\,?}{\tau_3}}{x}{} + {\Ftocic{\Jsubtype {\tau_1} {\tau_3}}, + \Ftocic{\Jsubtype {\tau_2} {\tau_3}}}} \\ + \Ftocic{\Jsubtype {\tau_1} {\TUnion{\tau_2}{\tau_3}}} & + \Tlam{x}{\tau_1}{\Tcon{0}{\TIeither{\tau_2}{\tau_3}} + ~(\Tapp{\Ftocic{\Jsubtype {\tau_1}{\tau_2}}}{x})} + \;\;\;\;\;\;\;\text{if }\Jsubtype {\tau_1}{\tau_2} + \\ + \Ftocic{\Jsubtype {\tau_1} {\TUnion{\tau_2}{\tau_3}}} & + \Tlam{x}{\tau_1}{\Tcon{1}{\TIeither{\tau_2}{\tau_3}} + ~(\Tapp{\Ftocic{\Jsubtype {\tau_1}{\tau_3}}}{x})} + \;\;\;\;\;\;\;\text{if }\Jsubtype {\tau_1}{\tau_3} + \end{array} + \end{displaymath} \begin{displaymath} \begin{array}{l@{\;=\;}l} \Ftocic x & x \\ @@ -1531,9 +1572,12 @@ system differs from that of~\citet{Gimenez94} in the following aspects: \Ftocic {\Tarw{x}{\tau_1}{\tau_2}} & \Tarw{x}{\Ftocic {\tau_1}}{\Ftocic {\tau_2}} \medskip \\ \Ftocic {\Tuple \EmptyCtx} & \TIUnit \\ - \Ftocic {\Tuple {x\:\tau_0,\Delta}} & \TIPair{x}{\tau_0}{\Ftocic {\Tuple \Delta}} \\ + \Ftocic {\Tuple {x\:\tau_0,\Delta}} & + \TIPair{x}{\Ftocic{\tau_0}}{\Ftocic {\Tuple \Delta}} \\ \Ftocic {\tuple \Delta {\cdot}} & \TIunit \\ - \Ftocic {\tuple \Delta {e,\vec e}} & \TIpair e {\Ftocic {\tuple \Delta {\vec e}}}\\ + \Ftocic {\tuple {x\:\tau_0,\Delta} {e,\vec e}} & + \TIpair{x}{\Ftocic e} + {\Ftocic {\tuple \Delta {\vec e}}}{\Ftocic {\Tuple \Delta}} \\ %% Note: The translation has reduction steps that don't correspond %% to any matching state in CUC. \Ftocic {\Tproj e i} & @@ -1541,12 +1585,16 @@ system differs from that of~\citet{Gimenez94} in the following aspects: %% Combined proj and let-binding, used for termination checking! \Ftocic {\Tapp{(\Tlam x {\tau_1} {e_1})}{\Tproj {e_2} 0}} & \MAlign{ - \TIcase {\Tlam x {\tau_{e_2}} {\Subst{\tau_2}{\TIproj 1 x}{x}}} {e_2} {?} - {\Tlam x {\tau_1} {\Tlam {\_} {\Ftocic{\Tuple \Delta}} {e_1}}} \\ + \TIcase {\tau_r} + {\Ftocic {e_2}} {?} + {\Tlam x {\Ftocic {\tau_1}} {\Tlam {\_} {\Ftocic{\Tuple \Delta}} + {\Ftocic{e_1}}}} \\ \;\;\text{where } \MAlign{\Jtype{e_2}{\tau_{e_2}} - \text{ and }{\tau_{e_2} = \Tuple {y\:\tau_0,\Delta}} \\ - \Jtype[\Gamma,x\:\tau_1]{e_1}{\tau_2}}} \\ + \text{ and }{\tau_{e_2} = \Tuple {x\:\tau_1,\Delta}} \\ + \Jtype[\Gamma,x\:\tau_1]{e_1}{\tau_2} \\ + \tau_r = \Tlam x {\Ftocic {\tau_{e_2}}} {\Subst{\Ftocic {\tau_2}}{\TIproj 1 x}{x}} + }} \\ \Ftocic {\Tapp{(\Tlam x {\tau_1} {e_1})}{\Tproj {e_2} i}} & \MAlign{ \TIcase {\Tlam \_ {\tau_{e_2}} {?}} {e_2} {?} @@ -1554,24 +1602,38 @@ system differs from that of~\citet{Gimenez94} in the following aspects: \;\;\text{where } \MAlign{ %% ¡¡FIXME: \tau_1 is not equal to the type of y.(i-1)!! + %% We can get a proof `P : x₀=π₁ e₂` and then use + %% `J P y` to get y' that will have the appropriate type, + %% but then \JIdecreasing will not know that y' is + %% smaller than e₂ so termination checking fails! + \FIXME{Wow!} \\ e' = \Ftocic{\Tapp{(\Tlam x {\tau_1} {e_1})} {\Tproj {y} {(i - 1)}}} \\ \Jtype{e_2}{\tau_{e_2}} \text{ and }{\tau_{e_2} = \Tuple {x_0\:\tau_0,\Delta}} \\ \Jtype[\Gamma,x\:\tau_1]{e_1}{\tau_2}}} \medskip \\ - \Ftocic {\id{Eq}} & \id{Eq} \\ - \Ftocic {\id{refl}} & \id{refl} \\ - \Ftocic {J} & J + \Ftocic {\Teq{e_1}{e_2}} & \TIeq{\Ftocic{e_1}}~{\Ftocic{e_2}} \\ + \Ftocic {\Trefl{e_1}} & \TIrefl{\Ftocic{e_1}} \\ + \Ftocic {\TJ{e_\equiv}{e_f}{e}} & + \TIJ{\Ftocic{e_\equiv}}{\Ftocic{e_f}}{\Ftocic{e}} + %% \;\;\text{where }\MAlign{ + %% \Jtype{e_\equiv}{\Teq{e_1}{e_2}} \\ + %% \Jtype{e_1}{\tau_1 : \Type{\ell_1}} \\ + %% \Jtype{\Tapp{e_f}{e_1}}{\Type{\ell_2}}}} \medskip \\ - \Ftocic {\Tmu[i]{x}{\tau}{e}} & \Tfix{i}{x}{\tau}{e} \\ + \Ftocic {\Tmu[i]{x}{\tau}{e}} & \Tfix{i}{x}{\Ftocic{\tau}}{\Ftocic{e}} \\ \Ftocic {\Tmu{x}{\tau}{(\Tmlam y \tau e)}} & - \Tind{x}{\tau}{\Tmarw y \tau {e\to \Tapp x {\vec y}}} \\ - \Ftocic {\Tfold \tau {\vec p} e} & \Tcon{\Ftocic {\tau}}{0}~{\vec p}~e \\ + \Tind{x}{\Ftocic{\tau}} + {\Tmarw y {\Ftocic{\tau}} {\Ftocic{e}\to \Tapp x {\vec y}}} \\ + \Ftocic {\Tfold \tau {\vec p} e} & + \Tcon{\Ftocic {\tau}}{0}~{\vec {\Ftocic{p}}}~{\Ftocic{e}} \\ \Ftocic {\Tunfold{\tau}{\vec p} e} & - \Ftocic {\Tapp{(\Tlam x {\Tapp{\tau}{\vec p}} x)}{(\Tunfold{\tau}{\vec p} e)}} \\ + \Ftocic {\Tapp{(\Tlam x {\,?} x)}{(\Tunfold{\tau}{\vec p} e)}} \\ \Ftocic {\Tapp{(\Tlam x \tau {e_1})}{(\Tunfold{\tau}{\vec p} e)}} & - \TIcase{?}{e}{\Tapp{\tau}{\vec p}}{\Tmlam y {\tau_y} {\Tlam x x}} \\ + \MAlign{ + \FIXME{Wow!} \\ + \TIcase{?}{e}{\Tapp{\tau}{\vec p}}{\Tmlam y {\tau_y} {\Tlam x x}}} \\ \medskip \\ \Ftocic {\TUnion{\tau_1}{\tau_2}} & \TIeither{\Ftocic {\tau_1}}{\Ftocic {\tau_2}} \\ %% \Ftocic {\Jsubtype{\tau_1}{\tau_2}} & \Tsarw{\Ftocic {\tau_1}}{\Ftocic {\tau_2}} \\ @@ -1654,6 +1716,8 @@ judgments into the logic: $\Tapp{\id{terminating-function}}{f}$ (FIXME: how would this work? Can we just defer to F-star instead?). \item \kw{cast} can take a proof of type $\tau_1 \subseteq \tau_2$. +\item \kw{fold}/\kw{unfold} can be replaced by a proof of equality between + the folded and unfolded type, so \kw{J} can do the folding/unfolding. \item \kw{switch}'s ordering/splitting relation can similarly be reified. \item \kw{tuple} can take a list of fields (type $\Tapp{\id{field-list}}{\ell}$) \end{itemize} View it on GitLab: https://gitlab.com/monnier/typer/commit/09881d771b3308299e0253de905e1b58dff… -- View it on GitLab: https://gitlab.com/monnier/typer/commit/09881d771b3308299e0253de905e1b58dff… You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer][report/itd] -
by Stefan 16 Nov '18

16 Nov '18

Stefan pushed to branch report/itd at Stefan / Typer Commits: 3f11c53d by Stefan Monnier at 2018-11-16T05:07:26Z - - - - - - 2 changed files: - paper.tex - refs.bib Changes: ===================================== paper.tex ===================================== @@ -112,7 +112,7 @@ %% \newcommand \Jstepr[1] {#1 \leadsto^{\!*}} \newcommand \JUstepArw {\stackrel{U}{\leadsto}} \newcommand \JUstep[1] {#1 \;\;\JUstepArw\;\; } -\newcommand \JUstepr[1] {#1 \JUstepArw{\!\!}^*~} +\newcommand \JUstepr[2][*] {#2 \JUstepArw{\!\!}^{#1}~} %% \newcommand \MetaFunction[2] {\llbracket #2 \rrbracket_{#1}} \newcommand \MetaFunction[2] {\left\llbracket #2 \right\rrbracket_{#1}} @@ -278,7 +278,8 @@ The contributions of this article are: \newcommand \Tind[3] {\kw{Ind}(#1\:#2)\langle#3\rangle} \newcommand \Tcon[2] {\kw{Con}(#1,#2)} -\newcommand \TIcase[4] {\langle#1\rangle\kw{Case}~#2 :#3 ~\kw{of}~\langle#4\rangle} +\newcommand \TIcase[4] {\langle#1\rangle\kw{Case}~#2 %% :#3 + ~\kw{of}~\langle#4\rangle} \newcommand \Tfix[3] {\kw{Fix}_{#1}~#2:#3~=~} In this section, we briefly present the two problems our design aims @@ -1183,13 +1184,13 @@ On the other hand, we do need to introduce a new reduction judgment $e_1 of the erased calculus are the following: %% \begin{mathpar} - \JEstep{\Tapp{(\Tlam x \tau {e_1})}{e_2}}{\Subst{e_1}{e_2}x} + \JEstep{\Tapp{(\Tlam x \_ {e_1})}{e_2}}{\Subst{e_1}{e_2}x} - \JEstep{(\tuple \Delta {\vec e}).i}{e_i} + \JEstep{(\tuple {\_} {\vec e}).i}{e_i} \JEstep {\TJ{(\Trefl{\_})}{\_}{x}}{x} - \Infer{e = \tuple[l'] \Delta {\vec e}} + \Infer{e = \tuple[l'] {\_} {\_}} {\JEstep{ \TUcase {e} {\tau_e} {\Ttagvar}{x}{e_\Ttagvar}{y}{e_d} }{ @@ -1201,7 +1202,7 @@ of the erased calculus are the following: }} %% \JEstep{\Tunfold{\_}{\_}{(\Tfold{\_}{\_}{e})}}{e} - \Infer{e_i = \tuple{\_}{\_} \\ e = \Tmu[i]{x}{\tau}{e'}} + \Infer{e = \Tmu[i]{x}{\_}{e'} \\ e_i = \tuple{\_}{\_}} {\JEstep{\Tapp{e}{\vec e}} {\Tapp{(\Subst{e'}{e}{x})}{\vec e}}} \end{mathpar} @@ -1259,7 +1260,7 @@ compiled to this CIC, and the reverse as well. \newcommand \BT[2] {\id{BT}\llbracket #1 \rrbracket_{#2}} \newcommand \JIstepArw {\stackrel{I}{\leadsto}} \newcommand \JIstep[1] {#1 \;\;\JIstepArw\;\; } -\newcommand \JIstepr[1] {#1 \JIstepArw{\!\!}^*~} +\newcommand \JIstepr[2][*] {#2 \JIstepArw{\!\!}^{#1}~} \begin{figure*} %% Syntax @@ -1286,8 +1287,7 @@ compiled to this CIC, and the reverse as well. } {\Jcic{\Tind{x}{\tau}{\vec c}}{\tau}} - \Infer{\Jcic e {\tau_e} \\ - \tau_e = {\tau_I~{\vec p}} \\ + \Infer{\Jcic e {\tau_I~{\vec p}} \\ \tau_I = \Tind{x}{\Tmarw{z}{\tau_z}{s}}{\vec c} \\ \Jcic {\tau_r}~{\Tmarw{z}{\tau_z}{\Tsarw{\tau_I~\vec z}s}} \\\\ \forall i. \\ @@ -1485,7 +1485,7 @@ system differs from that of~\citet{Gimenez94} in the following aspects: \begin{itemize} \item We omitted the obvious congruence rules for the $\JIstepArw$ relation and the termination judgment; -\item Our rules are extended to a tower of universes; and the typing rule of +\item Our rules are extended to a tower of universes and the typing rule of \kw{Ind} enforces predicativity; \item Giménez does not include the \kw{Ind} rule of $\JIpos e$; which allows us to define for example an inductive type $t$ where one of the fields has @@ -1523,26 +1523,42 @@ system differs from that of~\citet{Gimenez94} in the following aspects: \newcommand \TIproj[2] {\pi_{#1}~#2} \begin{figure} - Tags are erased, union types are converted to tagged sums, and \kw{cast} - replaced by a chunk of code \begin{displaymath} \begin{array}{l@{\;=\;}l} \Ftocic x & x \\ - \Ftocic {\Tlam{x}{\tau}{e}} & \Tlam{x}{\Ftocic {\tau}}{\Ftocic {e}} \\ + \Ftocic {\Tlam{x}{\tau_1}{e}} & \Tlam{x}{\Ftocic {\tau_1}}{\Ftocic {e}} \\ \Ftocic {\Tapp{e_1}{e_2}} & \Tapp{\Ftocic {e_1}}{\Ftocic {e_2}} \\ \Ftocic {\Tarw{x}{\tau_1}{\tau_2}} & \Tarw{x}{\Ftocic {\tau_1}}{\Ftocic {\tau_2}} \medskip \\ \Ftocic {\Tuple \EmptyCtx} & \TIUnit \\ - \Ftocic {\Tuple {x\:\tau,\Delta}} & \TIPair{x}{\tau}{\Ftocic {\Tuple \Delta}} \\ + \Ftocic {\Tuple {x\:\tau_0,\Delta}} & \TIPair{x}{\tau_0}{\Ftocic {\Tuple \Delta}} \\ \Ftocic {\tuple \Delta {\cdot}} & \TIunit \\ \Ftocic {\tuple \Delta {e,\vec e}} & \TIpair e {\Ftocic {\tuple \Delta {\vec e}}}\\ - \Ftocic {\Tproj e 0} & \TIproj 1 {\Ftocic {e}} \\ - \Ftocic {\Tproj e i} & \TIproj 2 {\Ftocic {\Tproj e {i - 1}}} \\ - \Ftocic {\Tapp{(\Tlam x {\tau} {e_1})}{\Tproj {e_2} 0}} & - \TIcase {\Tlam \_ \_ ?} {e_2} {?} - {\Tlam x \tau {\Tlam {x_2} \_ {e_1}}} \\ - \Ftocic {\Tapp{(\Tlam x {\tau} {e_1})}{\Tproj {e_2} i}} & - \TIproj 2 {\Ftocic {\Tproj e {i - 1}}} + %% Note: The translation has reduction steps that don't correspond + %% to any matching state in CUC. + \Ftocic {\Tproj e i} & + \TIproj 1 (\TIproj 2 {(\dots~{(\TIproj 2 {\Ftocic {e}})})}) \\ + %% Combined proj and let-binding, used for termination checking! + \Ftocic {\Tapp{(\Tlam x {\tau_1} {e_1})}{\Tproj {e_2} 0}} & + \MAlign{ + \TIcase {\Tlam x {\tau_{e_2}} {\Subst{\tau_2}{\TIproj 1 x}{x}}} {e_2} {?} + {\Tlam x {\tau_1} {\Tlam {\_} {\Ftocic{\Tuple \Delta}} {e_1}}} \\ + \;\;\text{where } + \MAlign{\Jtype{e_2}{\tau_{e_2}} + \text{ and }{\tau_{e_2} = \Tuple {y\:\tau_0,\Delta}} \\ + \Jtype[\Gamma,x\:\tau_1]{e_1}{\tau_2}}} \\ + \Ftocic {\Tapp{(\Tlam x {\tau_1} {e_1})}{\Tproj {e_2} i}} & + \MAlign{ + \TIcase {\Tlam \_ {\tau_{e_2}} {?}} {e_2} {?} + {\Tlam {x_0} {\tau_0} {\Tlam {y} {\Ftocic{\Tuple \Delta}} {?}}} \\ + \;\;\text{where } + \MAlign{ + %% ¡¡FIXME: \tau_1 is not equal to the type of y.(i-1)!! + e' = \Ftocic{\Tapp{(\Tlam x {\tau_1} {e_1})} + {\Tproj {y} {(i - 1)}}} \\ + \Jtype{e_2}{\tau_{e_2}} + \text{ and }{\tau_{e_2} = \Tuple {x_0\:\tau_0,\Delta}} \\ + \Jtype[\Gamma,x\:\tau_1]{e_1}{\tau_2}}} \medskip \\ \Ftocic {\id{Eq}} & \id{Eq} \\ \Ftocic {\id{refl}} & \id{refl} \\ @@ -1579,28 +1595,12 @@ The first question about CUC is whether this calculus is sound, meaning that if we consider it as a logic, we want to know that this logic is consistent. Rather than show it directly we do it by reducing the problem to that of the consistency of CIC. More specifically, we present a translation $\Ftocic \cdot$ -which takes any expression of CUC and translates it to an equivalent +which takes any type derivation of CUC and translates it to an equivalent expression in CIC; then we show that this translation is type preserving, and then we use this result to show that there can only be a proof of $\bot$ in -CUC if there is a proof of $\bot$ in CIC. - -If we have forall $e$ and $\tau$, -$\Jcuc e \tau$ then $\Jcic {\Ftocic e} {\Ftocic \tau}$. - -Corollary: CUC is as sound as CIC in the sense that there is an $e$ such that -$\Jcuc e \bot$ only if there's a $e'$ such that $\Jcic {e'} \bot$, because -$\Ftocic \bot = \bot$. - -\FIXME{Second take:} -%% This is much better, but we need to adjust the presentation accordingly: -%% - We can throw away some type annotations (yay!) -%% - We have to explain that while $\Ftocic\cdot$ is defined on derivations -%% we present it as if it was derived on the syntax of terms, to be -%% more concise. - -We define a translation function $\Ftocic\cdot$ which takes a derivation -$\Jcuc{e}{\tau}$ and returns an equivalent expression $e'$ in CIC. As an abuse -of notation, we will often write $\Ftocic e$ instead of $\Ftocic{\Jcuc{e}{\tau}}$. +CUC if there is a proof of $\bot$ in CIC. Figure~\ref{fig:cuc-to-cic} shows +the definition of $\Ftocic \cdot$. As an abuse of notation, we +often write $\Ftocic e$ instead of $\Ftocic{\Jcuc{e}{\tau}}$. \begin{lemma}[Type Preserving translation] Given $\Jcuc e \tau$, we have $\Jcuc \tau s$ and @@ -1612,8 +1612,8 @@ of notation, we will often write $\Ftocic e$ instead of $\Ftocic{\Jcuc{e}{\tau}} done by induction on the derivation. It requires proving several side lemmas such as the fact that a strictly positive recursive type is translated to a strictly positive inductive type, same for terminating - recursive functions, as well as the fact that $\JUstepr{e}{e'}$ implies - $\JIstepr{\Ftocic e}{\Ftocic{e'}}$, which itself requires proving that + recursive functions, as well as the fact that $\JUstepr[]{e}{e'}$ implies + $\JIstepr[+]{\Ftocic e}{\Ftocic{e'}}$, which itself requires proving that reduction preserves types. \end{proof} ===================================== refs.bib ===================================== @@ -3,7 +3,7 @@ @techreport{Monnier19a, author = {Stefan Monnier}, institution = {Université de Montréal - DIRO}, - title = {Typer: ML boosted with type theory and Scheme}, + title = {Typer: {ML} boosted with type theory and {S}cheme}, year = {2019}, url = {https://www.iro.umontreal.ca/\~{}monnier/typer-overview- 2019.pdf}, View it on GitLab: https://gitlab.com/monnier/typer/commit/3f11c53d814be35621e2e06e05cad47fc51… -- View it on GitLab: https://gitlab.com/monnier/typer/commit/3f11c53d814be35621e2e06e05cad47fc51… You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer][report/tcvi] -
by Stefan 15 Nov '18

15 Nov '18

Stefan pushed to branch report/tcvi at Stefan / Typer Commits: 603156f3 by Stefan Monnier at 2018-11-15T22:59:56Z - - - - - - 2 changed files: - paper.tex - refs.bib Changes: ===================================== paper.tex ===================================== @@ -239,16 +239,17 @@ is a need to try and better understand what those limits to impredicativity should look like. Let's disappoint the optimistic reader right away: this paper does not solve -this problem. Instead we consider several existing impredicative systems -which are believed to be consistent, and look at them through the lens of -erasability, arguing that \emph{maybe} the soundness of impredicative -quantification is linked to whether or not it's used in a significant way, -as suggested by Carnap~\cite{Fruchart96}. +this problem. But during the design of our experimental language +Typer~\cite{Monnier19a}, we noticed an interesting property shared by several +existing impredicative systems which are believed to be consistent, that +seemed to link impredicativity and erasability, hinting that \emph{maybe} the +soundness of impredicative quantification is linked to whether or not it's +used in a significant way, as suggested by Carnap~\cite{Fruchart96}. More specifically, we take those systems and refine them with annotations of -\emph{erasability} (which \citet{Miquel01} calls \emph{implicitness}) very -similar to those used in ICC* and EPTS~\cite{Barras08,MishraLinger08}, and -then show that all places that make use of impredicativity can be annotated +\emph{erasability} (which \citet{Miquel01} calls \emph{implicitness}) like +those used in ICC* and EPTS~\cite{Barras08,MishraLinger08}, and then show +that all places that make use of impredicativity can be annotated as erasable. Armed with this proverbial hammer, we then look at a few other forms of @@ -266,8 +267,8 @@ The contributions of this work are: fields of inductive types are also erasable. \item A suggestion for how to consistently extend CIC with strong elimination of large inductive types. -\item A proof that the same idea cannot similarly be used to consistently - extend CCω with impredicativity in other universes than the bottom one. +\item A proof that the same idea cannot similarly be used to allow + impredicativity in more than one universe. \item A sketch of a calculus with both inductive types and erasability annotations. While this is straightforward, we do not know of such a system published so far, the closest we found being the one described ===================================== refs.bib ===================================== @@ -37,6 +37,15 @@ year = {2000}, } +@techreport{Monnier19a, + author = {Stefan Monnier}, + institution = {Université de Montréal - DIRO}, + title = {Typer: {ML} boosted with type theory and {S}cheme}, + year = {2019}, + url = {https://www.iro.umontreal.ca/\~{}monnier/typer-overview- + 2019.pdf}, +} + @techreport{Fruchart96, address = {Paris}, author = {Thomas Fruchart and Guiseppe Longo}, View it on GitLab: https://gitlab.com/monnier/typer/commit/603156f372e9c4c564066174161065e0571… -- View it on GitLab: https://gitlab.com/monnier/typer/commit/603156f372e9c4c564066174161065e0571… You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer][report/tcvi] -
by Stefan 15 Nov '18

15 Nov '18

Stefan pushed to branch report/tcvi at Stefan / Typer Commits: 64359fcf by Stefan Monnier at 2018-11-15T22:33:09Z - - - - - - 2 changed files: - paper.tex - refs.bib Changes: ===================================== paper.tex ===================================== @@ -58,21 +58,22 @@ \renewcommand \cite \citep \DeclareUnicodeCharacter{03A9}{\ensuremath{\Omega}} +\DeclareUnicodeCharacter{03B1}{\ensuremath{\alpha}} +\DeclareUnicodeCharacter{03BB}{\ensuremath{\lambda}} +\DeclareUnicodeCharacter{03C3}{\ensuremath{\sigma}} +\DeclareUnicodeCharacter{03C4}{\ensuremath{\tau}} \DeclareUnicodeCharacter{03C9}{\ensuremath{\omega}} -\DeclareUnicodeCharacter{2203}{\ensuremath{\exists}} -\DeclareUnicodeCharacter{2261}{\ensuremath{\equiv}} -\DeclareUnicodeCharacter{21DB}{\ensuremath{\Rrightarrow}} -\DeclareUnicodeCharacter{2980}{\ensuremath{|||}} +\DeclareUnicodeCharacter{0394}{\ensuremath{\Delta}} \DeclareUnicodeCharacter{2081}{\ensuremath{_1}} \DeclareUnicodeCharacter{2082}{\ensuremath{_2}} \DeclareUnicodeCharacter{21D2}{\ensuremath{\Rightarrow}} +\DeclareUnicodeCharacter{21DB}{\ensuremath{\Rrightarrow}} \DeclareUnicodeCharacter{2200}{\ensuremath{\forall}} -\DeclareUnicodeCharacter{03C3}{\ensuremath{\sigma}} -\DeclareUnicodeCharacter{03BB}{\ensuremath{\lambda}} -\DeclareUnicodeCharacter{03C4}{\ensuremath{\tau}} -\DeclareUnicodeCharacter{0394}{\ensuremath{\Delta}} -\DeclareUnicodeCharacter{1D4C5}{\ensuremath{\wp}} +\DeclareUnicodeCharacter{2203}{\ensuremath{\exists}} +\DeclareUnicodeCharacter{2261}{\ensuremath{\equiv}} +\DeclareUnicodeCharacter{2980}{\ensuremath{|||}} \DeclareUnicodeCharacter{1D4B0}{\ensuremath{\mathcal{U}}} +\DeclareUnicodeCharacter{1D4C5}{\ensuremath{\wp}} %% The doc says `vcenter` should work, but I get an error :-( %% \newcommand \Infer[1][] [\inferrule*[vcenter,right=#1]] @@ -140,7 +141,7 @@ %% %% can be repeated if necessary; %% %% contents suppressed with 'anonymous' -\author{Stefan Monnier} +\author{Stefan Monnier\inst{1} \and Nathaniel Bos\inst{2}} %% \affiliation{ %% %% \department{DIRO} %% \institution{Université de Montréal - DIRO} @@ -150,6 +151,9 @@ \institute{ Université de Montréal - DIRO \\ \email{monnier(a)iro.umontreal.ca} + \and + McGill University - SCS \\ + \email{nathaniel.bos(a)mail.mcgill.ca} } %% \author{Other author} @@ -217,7 +221,7 @@ might still enjoy consistency. %% Discuss how SELIT enters into the picture. %% - Maybe discuss UTT and Coq and how they don't fit this model. -Propositions such as ``This is a lie!'' and other diagonalization proofs +Diagonalization proofs and paradoxes such as ``This sentence is false'' show the dangers of self reference: admitting such propositions in a logic leads to inconsistencies. For this reason Russell introduced the concept of \emph{type} as well as \emph{predicativity} (and its inverse). @@ -248,12 +252,12 @@ then show that all places that make use of impredicativity can be annotated as erasable. Armed with this proverbial hammer, we then look at a few other forms of -impredicativity that break consistency and argue that they like nails: by -restricting those forms of impredicativity to be erasable we may be able to -recover consistency. While there is admittedly ample room in the margins, -in order not to spoil their pleasure, we carefully leave it as an exercise -for the readers to prove (or disprove) that the resulting extensions are -indeed consistent. +impredicativity that break consistency and argue that they look like nails: +by restricting those forms of impredicativity to be erasable we may be able +to recover consistency. While there is admittedly ample room in the +margins, in order not to spoil their pleasure, we carefully leave it as an +exercise for the readers to prove (or disprove) the consistency of some of +the resulting extensions. The contributions of this work are: \begin{itemize} @@ -376,10 +380,10 @@ erasability as follows: \end{array} \end{displaymath} This version has 4 different abstractions, allowing both System-F's value -abstractions $\lambda$ and type abstractions $\Lambda$ to be annotated as either erasable or -normal. It is well known that System-F enjoys the \emph{phase distinction}, -so we could also define an EPTS equivalent to System-F with only -2 abstractions, using the following rules instead: +abstractions $\lambda$ and type abstractions $\Lambda$ to be annotated as either +erasable or normal. It is well known that System-F enjoys the phase +distinction~\cite{Cardelli88}, so we could also define an EPTS equivalent +to System-F with only 2 abstractions, using the following rules instead: \begin{displaymath} \mathcal{R} = \MAlign{ @@ -394,7 +398,7 @@ Figure~\ref{fig:epts} shows the typing rules of our EPTS. Compared to a normal CPTS, the only difference is that the typing rule for functions is split into \textsc{n-Lam} and \textsc{e-Lam} where \textsc{e-Lam} includes the additional constraint $x \not\in \kw{fv}(\Ferase e)$ that enforces the -erasability of the argument. ``$\Ferase e$'' is the \emph{erasure} of $e$, +erasability of the argument. The expression ``$\Ferase e$'' is the \emph{erasure} of $e$, where the erasure function $\Ferase{(\cdot)}$ erases type annotations as well as all erasable arguments: \begin{displaymath} @@ -445,7 +449,7 @@ every well-typed term $e$ in an EPTS $S$ has a corresponding well-typed term $\Fforget e$ in $\Fforget S$, so the consistency of the corresponding PTS would not automatically carry over to the EPTS. -\citet{Barras08} argues in favor of using such a stronger rule by showing +\citet{Barras08} argue in favor of using such a stronger rule by showing some example applications where it is able to equate more terms by erasing (and hence ignoring) some proofs, in a sense internalizing a form of proof irrelevance similar to that of Coq. But those examples all rely on @@ -564,27 +568,30 @@ The calculus we use for that can be described by the following EPTS: \mathcal{S} &=& \{~ \kw{Prop}; \Type \ell ~|~ \ell\in\mathbb{N} ~\} \\ \mathcal{A} &=& \{~ (\kw{Prop} : \Type 0); - (\Type \ell : \Type {\ell+1}) ~|~ \ell\in\mathbb{N} ~\} \\ + (\Type \ell : \Type {\ell+1}) ~~|~~ \ell\in\mathbb{N} ~\} \\ \mathcal{R} &=& \MAlign{ \{~ (k, \kw{Prop}, s, s); - (k, s, \kw{Prop}, \kw{Prop}) ~|~ s \in \mathcal{S} ~\} \\ + (k, s, \kw{Prop}, \kw{Prop}) + ~~|~~ s \in \mathcal{S}, k \in \{\kw{n},\kw{e}\} ~\} \\ \cup ~\{~ - (k, \Type {\ell_1}, \Type {\ell_2}, \Type {\ell_1 \sqcup \ell_2}) - ~|~ \ell_1,\ell_2 \in\mathbb{N} ~\} + (k, \Type {\ell_1}, \Type {\ell_2}, \Type {\Tmax{\ell_1}{\ell_2}}) + ~~|~~ \ell_1,\ell_2 \in\mathbb{N}, k \in \{\kw{n},\kw{e}\} ~\} } \end{array} \end{displaymath} This calculus follows the tradition of having a special impredicative \kw{Prop} universe with a tower of predicative universes named $\Type \ell$. +$\Tmax{\ell_1}{\ell_2}$ denotes simply the least upper bound of $l_1$ and $l_2$. The calculus $\Fforget{\text{CCω}}$ we get by removing the erasability -annotations is sometimes also called CCω. And indeed the two are -equivalent: we can see that any well-typed term $e$ in $\Fforget{\text{CCω}}$ -has a corresponding well-typed term $\lceil e\rceil$ in CCω such that $\Fforget{\lceil e\rceil} -= e$ by simply making $\lceil\cdot\rceil$ add \kw{n} annotations everywhere. -Our calculus CCω is incidentally almost identical to the ICC* calculus of -\citet{Barras08} (except for the \textsc{Conv} rule, as discussed above). +annotations is sometimes also called CCω in the literature. And indeed the +two are equivalent: we can see that any well-typed term $e$ in +$\Fforget{\text{CCω}}$ has a corresponding well-typed term $\lceil e\rceil$ in CCω +such that $\Fforget{\lceil e\rceil} = e$ by simply making $\lceil\cdot\rceil$ add \kw{n} annotations +everywhere. Our calculus CCω is incidentally almost identical to the ICC* +calculus of \citet{Barras08} (except for the \textsc{Conv} rule, as +discussed above). With respect to impredicativity, the relevant rule in CCω is: $(k, s, \kw{Prop}, \kw{Prop})$ which allows functions in \kw{Prop} to take arguments @@ -625,7 +632,7 @@ And we will now show that the second is redundant: %% CCω's rule $(\kw{n}, s, \kw{Prop}, \kw{Prop})$ is redundant since for any derivation $\Jtype e \tau$ in CCω there is a corresponding derivation $\Jtype[\Gamma'] - {e'} {\tau'}$ in CCω' which does not use that rule and where + {e'} {\tau'}$ in CCω$'$ which does not use that rule and where $\Fforget{\Jtype e \tau} = \Fforget{\Jtype[\Gamma'] {e'} {\tau'}}$ \end{theorem} \begin{proof} @@ -633,7 +640,7 @@ And we will now show that the second is redundant: $\kw{n}$ with $\kw{e}$ on all functions, arrows, and applications that previously relied on the rule $(\kw{n}, s, \kw{Prop}, \kw{Prop})$. Since the erasability annotation is only used in the typing rule of - $\lambda$-abstractions, the proof follows trivial for all cases except this one. + $\lambda$-abstractions, the proof follows trivially for all cases except this one. For $\lambda$-abstractions that had an \kw{n} annotation that we need to convert to \kw{e}, we need to satisfy the additional condition that $x \not\in \kw{fv}(\Ferase e)$, which follows from Lemma~\ref{lem:erasable}: In the @@ -757,6 +764,7 @@ handle those additional terms: \Ferase {\Con{i}{e}} & \ConE{i} \\ \Ferase {\Case{\tau_r}{e}{\vec b}} & \CaseE{\Ferase e}{\overrightarrow {\Ferase b}} \\ + %% FIXME: Dropping the $i$ makes the reduction semantics tricky. \Ferase {(\Fix{i}{x}{\tau}{e})} & \FixE{x}{\Ferase e} \end{array} \end{displaymath} @@ -788,15 +796,15 @@ annotations placed on a given constructor $a_i$ must match the erasability annotations of the arguments expected by the corresponding branch $b_i$. Two important details are worth pointing out: \begin{itemize} -\item First, in the rule for \kw{Ind} the type of constructors is restricted - to be in \kw{Prop}: just like in CIC we only allow inductive types in our - bottom universe, contrary to what systems like Coq~\cite{Coq00} and - UTT~\cite{Luo92} allow. -\item Second in the \kw{Case} rule we have the condition that when the +\item In the rule for \kw{Ind} the type of constructors is restricted + to be in \kw{Prop}: just like in the original CIC we only allow inductive + types in our bottom universe, contrary to what systems like + Coq~\cite{Coq00} and UTT~\cite{Luo92} allow. +\item In the \kw{Case} rule we have the condition that when the result of the case analysis is not in \kw{Prop}, i.e.~when this is a form of strong elimination, the inductive type must be small, meaning that all its fields must be in \kw{Prop}. This restriction is taken from - \citet{Werner94} which presents it slightly differently because he splits + \citet{Werner94} who presents it slightly differently because he splits the \kw{Case} rule into two: one for weak elimination and one for strong elimination. \end{itemize} @@ -808,7 +816,7 @@ Their definition is not affected by the presence of erasability annotations and does not impact our work here. To show that the $(\kw{n}, s, \kw{Prop}, \kw{Prop})$ rule of non-erasable -impredicativity is still redundant in this new system, we proceed in the say +impredicativity is still redundant in this new system, we proceed in the same way: \begin{lemma}[Confinement of impredicativity in CIC] \label{lem:erasable-cic} \\ \normalfont @@ -828,9 +836,9 @@ way: \item If $e$ is of the form $\Fix{i}{x}{\tau}{e'}$, then $\tau$ does not matter because it's erased, and we can invoke the inductive hypothesis on $e'$. \item If $e$ is of the form $\Case{\tau_r}{e'}{\vec b}$, then $\tau_r$ does not - matter because it's erased, Also we know $e'$ is in $\kw{Prop}$ since + matter because it's erased. Also we know $e'$ is in $\kw{Prop}$ since all our inductive types are in $\kw{Prop}$, so we can invoke the - inductive hypothesis on $e'$. Also since $e$ in is $\kw{Prop}$, all + inductive hypothesis on $e'$. Also since $e$ is in $\kw{Prop}$, all $b_i$ are as well, hence we can also invoke the induction hypothesis on every $b_i$. \qed \end{itemize} @@ -840,7 +848,7 @@ way: %% CIC's rule $(\kw{n}, s, \kw{Prop}, \kw{Prop})$ is redundant since for any derivation $\Jtype e \tau$ in CIC there is a corresponding derivation $\Jtype[\Gamma'] - {e'} {\tau'}$ in CIC' which does not use that rule and where + {e'} {\tau'}$ in CIC$'$ which does not use that rule and where $\Fforget{\Jtype e \tau} = \Fforget{\Jtype[\Gamma'] {e'} {\tau'}}$ \end{theorem} \begin{proof} @@ -849,7 +857,7 @@ way: and applications that previously relied on the rule $(\kw{n}, s, \kw{Prop}, \kw{Prop})$. The interesting new case is when $e$ is of the form $\Case{\tau_r}{e'}{\vec b}$: - As mentioned, the vector $\vec c$ of erasability + as mentioned, the vector $\vec c$ of erasability annotations placed on a given constructor $a_i$ must match the erasability annotations of the arguments expected by the corresponding branch $b_i$. Since our inductive types all live in \kw{Prop}, it means all fields that @@ -918,7 +926,7 @@ applicability of large inductive types. \{~ (k, \kw{Prop}, s, s); (\kw{e}, s, \kw{Prop}, \kw{Prop}) ~|~ s \in \mathcal{S} ~\} \\ \cup ~\{~ - (k, \Type {\ell_1}, \Type {\ell_2}, \Type {\ell_1 \sqcup \ell_2}) + (k, \Type {\ell_1}, \Type {\ell_2}, \Type {\Tmax{\ell_1}{\ell_2}}) ~|~ \ell_1,\ell_2 \in\mathbb{N} ~\} } \end{array} @@ -947,14 +955,14 @@ large fields of impredicative inductive definitions, as we saw in the previous section. Figure~\ref{fig:ecic} shows a refinement of CIC we call ECIC: just like -CIC', it only has the $(\kw{e},s,\kw{Prop},\kw{Prop})$ rule and not the +CIC$'$, it only has the $(\kw{e},s,\kw{Prop},\kw{Prop})$ rule and not the $(\kw{n},s,\kw{Prop},\kw{Prop})$ rule, meaning that impredicativity can only be used with erasable arguments and fields. But additionally it has -a further difference to CIC and CIC' which is that its \kw{Case} rule does +a further difference to CIC and CIC$'$ which is that its \kw{Case} rule does not have the $\Jsmall e$ constraint. ECIC is more elegant and regular than CIC thanks to the absence of this -special corner case, and it allows typing more terms than CIC' and hence +special corner case, and it allows typing more terms than CIC$'$ and hence CIC. For instance in ECIC we can define the above $\Omega$ inductive type with an erasable $k$ and then prove the mentioned property (again with erasable $K_1$ and $K_2$). @@ -993,7 +1001,7 @@ which can be defined as an EPTS as follows: } \end{array} \end{displaymath} -Of the five sets of rules, three are impredicative: $(k,\square,*,*)$, +Of the five pairs of rules, three are impredicative: $(k,\square,*,*)$, $(k,\mathrm{\Delta},*,*)$, and $(k,\mathrm{\Delta},\square,\square)$, but since $*$ is the bottom universe and hence corresponds to \kw{Prop} in CCω, the first two are generally considered safe and are included in CCω. The new one is @@ -1017,7 +1025,7 @@ induction hypothesis on $\tau_1$ if $x$ is in the universe $\mathrm{\Delta}$, because $\tau_1$ might itself also be in the universe $\mathrm{\Delta}$ because of the $(k,\mathrm{\Delta},\square,\square)$ rule. -\begin{figure} +\begin{figure}[tb] \begin{displaymath} \begin{array}{c} \begin{array}{l@{\;\;=\;\;}l} @@ -1095,7 +1103,7 @@ types to live in \kw{Prop}. This was no accident: we can see in the proof of confinement that we rely on this property to show the erasability of impredicative arguments in CIC. We could relax this constraint by allowing inductive types in higher universes but disallowing elimination from those -types to \kw{Prop}. This would be a kind of opposite of the outlawing of +types to \kw{Prop}. This would be a kind of opposite to the outlawing of strong elimination of large inductive types. With such a restriction, we could then still show the erasability of impredicative arguments. @@ -1118,10 +1126,10 @@ be consistent. \section{Conclusion} We have taken a tour of the interactions between impredicativity and -erasability of arguments in EPTS. We have shown that 3 of the most well -known systems that admit impredicativity do it in a way to constrains all +erasability of arguments in EPTS. We have shown that three of the most well +known systems that admit impredicativity do it in a way that constrains all impredicative abstractions and fields to be erasable. We have also shown -while impredicativity and erasability seem to be correlated, erasability is +that while impredicativity and erasability seem to be correlated, erasability is neither a necessary nor a sufficient condition for impredicativity to be consistent, by showing that UTT's impredicative definitions are not all erasable and showing that $\lambda EU^-$ is not consistent. @@ -1134,9 +1142,6 @@ types without breaking consistency. \newcommand \grantsponsor[3] {#2 (#1)} \newcommand \grantnum[2] {#2} \begin{acks} - Thanks to Nathaniel who completed an earlier version of the proof - of erasability of impredicative arguments in CCω. - This work was supported by the \grantsponsor{NSERC}{Natural Sciences and Engineering Research Council of Canada}{http://nserc-crsng.gc.ca/} grant N$^o$~\grantnum{NSERC}{298311/2012}. Any opinions, findings, and ===================================== refs.bib ===================================== @@ -24,7 +24,7 @@ Instead it has an Emacs-based interface which allows programming by gradual refinement of incomplete type-correct terms.}, - url = {http://www.cse.chalmers.se/~ulfn/papers/tphols09/ + url = {http://www.cse.chalmers.se/\~{}ulfn/papers/tphols09/ tutorial.pdf}, } @@ -95,7 +95,7 @@ into the implicit calculus helps to reflect the computational meaning of the underlying terms in a more accurate way.}, - url = {https://www.fing.edu.uy/~amiquel/publis/tlca01.pdf}, + url = {https://www.fing.edu.uy/\~{}amiquel/publis/tlca01.pdf}, } @inproceedings{Barras08, @@ -128,8 +128,8 @@ static information. We also illustrate the main features of ICC∗ on classical examples of dependently typed programs.}, - url = {http://www.lix.polytechnique.fr/~bernardo/writings/barras- - bernardo-icc-fossacs08.pdf}, + url = {http://www.lix.polytechnique.fr/\~{}bernardo/writings/ + barras-bernardo-icc-fossacs08.pdf}, } @inproceedings{MishraLinger08, @@ -244,6 +244,13 @@ url = {http://doi.acm.org/10.1017/S0956796812000056}, } +@misc{Cardelli88, + author = {Luca Cardelli}, + howpublished = {DEC-SRC manuscript}, + title = {Phase Distinctions in Type Theory}, + year = {1988}, +} + @techreport{Gimenez94, author = {Eduardo Giménez}, institution = {École Normale Supérieure de Lyon}, @@ -290,7 +297,7 @@ title = {A unifying theory of dependent types: the schematic approach}, year = {1992}, - url = {http://www.cs.rhul.ac.uk/~zhaohui/TVER92.ps}, + url = {http://www.cs.rhul.ac.uk/\~{}zhaohui/TVER92.ps}, } @inproceedings{Coquand86b, @@ -381,7 +388,7 @@ pages = {266-278}, title = {A simplification of {G}irard's paradox}, year = {1995}, - url = {http://www.cs.cmu.edu/~kw/scans/hurkens95tlca.pdf}, + url = {http://www.cs.cmu.edu/\~{}kw/scans/hurkens95tlca.pdf}, } @proceedings{FOSSACS08, View it on GitLab: https://gitlab.com/monnier/typer/commit/64359fcfeb0448a4ba345294e53cb230b0f… -- View it on GitLab: https://gitlab.com/monnier/typer/commit/64359fcfeb0448a4ba345294e53cb230b0f… You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer][report/itd] -
by Stefan 15 Nov '18

15 Nov '18

Stefan pushed to branch report/itd at Stefan / Typer Commits: 6686fdae by Stefan Monnier at 2018-11-15T17:25:06Z - - - - - - 1 changed file: - paper.tex Changes: ===================================== paper.tex ===================================== @@ -1222,10 +1222,10 @@ be implemented as no-ops: \end{lemma} \begin{proof} By induction on the derivation of ${e_1}\JUstepArw{e_2}$ - resp. ${\Erase{e_1}}\JEstepArw{e_2}$. The proof is tedious because it - requires a various lemmas showing for example that if - $\Erase{e_1}=\tuple{\_}{\_}$ the terms that were erased cannot be - arbitrary but that \kw{fold} and \kw{unfold} come in pairs. + resp. ${\Erase{e_1}}\JEstepArw{e_2}$. The proof requires various lemmas + showing for example that if $\Erase{e_1}=\tuple{\_}{\_}$ the terms that + were erased cannot be arbitrary but that \kw{fold} and \kw{unfold} come + in pairs. \end{proof} \section{Equivalence} @@ -1241,7 +1241,7 @@ be implemented as no-ops: Now that we have defined a calculus which provides us with the intended run-time cost, we show that this calculus is sound and complete with respect to a more classic presentation of inductive types. We will first present -a variant of our base calculus extended with inductive types in the style +a variant of the base calculus extended with inductive types in the style of~\citet{Gimenez94}, and then show that any expression of our CUC can be compiled to this CIC, and the reverse as well. @@ -1449,7 +1449,7 @@ compiled to this CIC, and the reverse as well. We add inductive types following the style of \citet{Gimenez94} which separates induction into case analysis and recursive definitions, -combined with a syntactic check that the recursive calls corresponds to +combined with a syntactic check that the recursive calls correspond to a structural induction. The syntax of the base language is extended as follows: %% @@ -1466,13 +1466,13 @@ follows: \end{array} \end{displaymath} $\Tind{x}{\tau}{\vec c}$ is an inductive type of kind $\tau$ with $|\vec c|$ -constructors where $c_i$ is the type of the $i^{th}$ constructor; \\ +constructors where $c_i$ is the type of the $i^{th}$ constructor; $\Tcon{i}{e}$ -is the $i^{th}$ constructor of the inductive type $e$; \\ +is the $i^{th}$ constructor of the inductive type $e$; $\TIcase{\tau_r}{e}{\tau_e}{\vec b}$ performs case analysis on an object $e$ of inductive type; for an object built with the $i^{th}$ constructor, branch $b_i$ will be called, passing to it the -arguments that were passed to the constructor; \\ +arguments that were passed to the constructor; and finally $\Tfix{i}{x}{\tau}{e}$ defines a recursive function which performs a structural induction on its $i^{th}$ argument. @@ -1485,8 +1485,8 @@ system differs from that of~\citet{Gimenez94} in the following aspects: \begin{itemize} \item We omitted the obvious congruence rules for the $\JIstepArw$ relation and the termination judgment; -\item Our rules are extended to a tower of universes; -\item The typing rule of \kw{Ind} enforces predicativity; +\item Our rules are extended to a tower of universes; and the typing rule of + \kw{Ind} enforces predicativity; \item Giménez does not include the \kw{Ind} rule of $\JIpos e$; which allows us to define for example an inductive type $t$ where one of the fields has type $\id{List}~t$. Most proof assistants allow such a relaxation of the @@ -1495,10 +1495,10 @@ system differs from that of~\citet{Gimenez94} in the following aspects: fields of an object to be smaller than the object analyzed, whereas Giménez limits this to the fields which are in a \emph{recursive position}. -\end{itemize} -Giménez needs this additional restriction because his \kw{Set} universe is -impredicative, so he needs to disallow recursions such as the one hinted at -in~\cite{Coquand92}: + %% + Giménez needs this additional restriction because his \kw{Set} universe is + impredicative, so he needs to disallow infinite recursions such as the + following one, hinted at in~\cite{Coquand92}: \begin{displaymath} \MAlign{ D = \Tind{D}{\kw{Set}}{\Tsarw{(\Tarw{t}{\kw{Set}}{\Tsarw{t}{t}})}{D}}; \\ @@ -1510,6 +1510,7 @@ in~\cite{Coquand92}: \id{oops} = f~d; } \end{displaymath} +\end{itemize} \subsection{CUC to CIC} View it on GitLab: https://gitlab.com/monnier/typer/commit/6686fdaec12436f4bd4d1eaefc45e19263e… -- View it on GitLab: https://gitlab.com/monnier/typer/commit/6686fdaec12436f4bd4d1eaefc45e19263e… You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer][report/itd] -
by Stefan 14 Nov '18

14 Nov '18

Stefan pushed to branch report/itd at Stefan / Typer Commits: 0b4b89d4 by Stefan Monnier at 2018-11-14T23:22:18Z - - - - - - 1 changed file: - paper.tex Changes: ===================================== paper.tex ===================================== @@ -865,25 +865,19 @@ the explicit equality witnesses can be used to get the same effect. \JUstep{\TUcast{\tau}{\tau}e}{e} - \Infer{e = \TUcast {\tau}{\tau_e} e' \\ - e' = {\tuple \Delta {\vec e}} \\ - \JOrder {\tau_e}{\tau_l}{\tau_d}} - {\JUstep{ - \TUcase {e} {\tau_e} - {\Ttagvar}{x}{e_\Ttagvar}{y}{e_d} - }{ - \Subst{e_\Ttagvar}{\id{refl}~{\tau_e}~e, \TUcast {\tau}{\tau_l} e'}{x_\equiv,x} - }} - \Infer{e = \TUcast {\tau}{\tau_e} e' \\ e' = {\tuple[l'] \Delta {\vec e}} \\ - l \not= l' \\ \JOrder {\tau_e}{\tau_l}{\tau_d}} {\JUstep{ \TUcase {e}{\tau_e} {\Ttagvar}{x}{e_\Ttagvar}{y}{e_d} }{ - \Subst{e_d}{\id{refl}~{\tau_e}~e,\TUcast {\tau}{\tau_d} {e'}}{y_\equiv,y} + \left\{\begin{array}[c]{l@{\;\;}l} + \Subst{e_d}{\Trefl{e},\TUcast {\tau}{\tau_d} {e'}}{y_\equiv,y} & + \text{if }l=l' \\ + \Subst{e_\Ttagvar}{\Trefl{e}, \TUcast {\tau}{\tau_l} e'}{x_\equiv,x} & + \text{otherwise} + \end{array}\right. }} %% \end{array} \end{mathpar} @@ -1157,7 +1151,7 @@ The intention of our calculus is for \kw{cast}, \kw{fold}, and \kw{unfold} to have no run-time cost. In this section, we show that it is indeed the case, by defining an erasure function and showing that the evaluation and the erasure commute. - +%% The erasure function $\Erase{(\cdot)}$ is defined recursively on the syntax of terms in a straightforward manner: %% @@ -1180,7 +1174,7 @@ terms in a straightforward manner: \end{array} \end{displaymath} The $\cdots$ stand for all the remaining constructs where the function simply -recurses in the obvious way on all subterms. We do not need to introduce +recurses in the obvious way on all subterms. We do not introduce a new syntax for erased terms because they simply use a subset of the syntax of the non-erased terms. %% @@ -1191,32 +1185,22 @@ of the erased calculus are the following: \begin{mathpar} \JEstep{\Tapp{(\Tlam x \tau {e_1})}{e_2}}{\Subst{e_1}{e_2}x} - \begin{array}{c} - \JEstep{ - \TUcase {(\tuple \Delta {\vec e})} {\tau_e} - {\Ttagvar}{x}{e_\Ttagvar}{y}{e_d} \\ - }{ - \Subst{e_\Ttagvar} - {\id{refl},(\tuple \Delta {\vec e})} - {x_\equiv,x} - } - \end{array} - \JEstep{(\tuple \Delta {\vec e}).i}{e_i} - \begin{array}{c} - \JEstep{ - \TUcase {(\tuple[l'] \Delta {\vec e})}{\tau_e} - {\Ttagvar}{x}{e_\Ttagvar}{y}{e_d} \\ - }{ - \Subst{e_d} - {\id{refl},(\tuple[l'] \Delta {\vec e})} - {y_\equiv,y} - } - \end{array} - - \JEstep {J~\_~\_~\_~\_~\_~(\id{refl}~\_~\_)~x}x + \JEstep {\TJ{(\Trefl{\_})}{\_}{x}}{x} + + \Infer{e = \tuple[l'] \Delta {\vec e}} + {\JEstep{ + \TUcase {e} {\tau_e} {\Ttagvar}{x}{e_\Ttagvar}{y}{e_d} + }{ + \left\{\begin{array}[c]{l@{\;\;}l} + \Subst{e_\Ttagvar}{\Trefl{e},e}{x_\equiv,x} & + \text{if }l=l' \\ + \Subst{e_d}{\Trefl{e},e}{y_\equiv,y} & \text{otherwise} + \end{array}\right. + }} + %% \JEstep{\Tunfold{\_}{\_}{(\Tfold{\_}{\_}{e})}}{e} \Infer{e_i = \tuple{\_}{\_} \\ e = \Tmu[i]{x}{\tau}{e'}} {\JEstep{\Tapp{e}{\vec e}} {\Tapp{(\Subst{e'}{e}{x})}{\vec e}}} @@ -1228,17 +1212,20 @@ be implemented as no-ops: %% \begin{lemma}[Erasure] \label{lem:erasure} - Assuming $ \Jcuc e \tau$, we have: + Assuming $ \Jcuc {e_1} \tau$, we have: \begin{itemize} - \item If $e \JUstepArw {e_1}$ then either ${\Erase e} = {\Erase - {e_1}}$ or ${\Erase e}\JEstepArw{\Erase {e_1}}$. - \item If ${\Erase e}\JEstepArw{e_2}$ then there exists an $e_3$ such that - $\Erase{e_3} = e_2$ and $\JUstepr e {e_3}$. + \item If ${e_1}\JUstepArw{e_2}$ then either ${\Erase{e_1}}={\Erase{e_2}}$ + or ${\Erase{e_1}}\JEstepArw{\Erase{e_2}}$. + \item If ${\Erase{e_1}}\JEstepArw{e_2}$ then there exists an $e_3$ such + that $\Erase{e_3}=e_2$ and $\JUstepr{e_1}{e_3}$. \end{itemize} \end{lemma} \begin{proof} - The first part is proved by induction on the derivation of $e \JUstepArw - {e_1}$, + By induction on the derivation of ${e_1}\JUstepArw{e_2}$ + resp. ${\Erase{e_1}}\JEstepArw{e_2}$. The proof is tedious because it + requires a various lemmas showing for example that if + $\Erase{e_1}=\tuple{\_}{\_}$ the terms that were erased cannot be + arbitrary but that \kw{fold} and \kw{unfold} come in pairs. \end{proof} \section{Equivalence} @@ -1500,9 +1487,9 @@ system differs from that of~\citet{Gimenez94} in the following aspects: and the termination judgment; \item Our rules are extended to a tower of universes; \item The typing rule of \kw{Ind} enforces predicativity; -\item Giménez does not include the \kw{Ind} rule of $\JIpos e$; which allows to - define for example an inductive type $t$ where one of the fields has type - $\id{List}~t$. Most proof assistants allow such a relaxation of the +\item Giménez does not include the \kw{Ind} rule of $\JIpos e$; which allows + us to define for example an inductive type $t$ where one of the fields has + type $\id{List}~t$. Most proof assistants allow such a relaxation of the positivity requirement; \item The termination check on \kw{Case} is simpler in that it considers all fields of an object to be smaller than the object analyzed, whereas View it on GitLab: https://gitlab.com/monnier/typer/commit/0b4b89d4b4df16c076425d12c1f2c4a173d… -- View it on GitLab: https://gitlab.com/monnier/typer/commit/0b4b89d4b4df16c076425d12c1f2c4a173d… You're receiving this email because of your account on gitlab.com.

1 0

2024

2023

2022

2021

2020

2019

2018

2017

2016

Typer Novembre 2018