Mercurial > hg > Papers > 2018 > nozomi-master

comparison paper/type.tex @ 43:9030d2680559

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Wrote typed-lambda
author atton <atton@cr.ie.u-ryukyu.ac.jp>
date Sun, 29 Jan 2017 12:27:25 +0900
parents 142c8de4a24f
children 3b2446944d11
comparison
equal deleted inserted replaced
42:142c8de4a24f 43:9030d2680559
789 よって、関数適用 $ t_1 \; t_2 $ の評価順は、まずE-APP1を用いて$t_1$が値となった後にE-APP2を用いて$t_2$を値とし、最後にE-APPABSで関数を適用を行なう。 789 よって、関数適用 $ t_1 \; t_2 $ の評価順は、まずE-APP1を用いて$t_1$が値となった後にE-APP2を用いて$t_2$を値とし、最後にE-APPABSで関数を適用を行なう。
790 790
791 791
792 % }}} 792 % }}}
793 793
794 % {{{ 単純型付きラムダ計算
795
794 \section{単純型付きラムダ計算} 796 \section{単純型付きラムダ計算}
795 型無しラムダ計算に対して単純型を適用する場合、ラムダ抽象の型について考える必要がある。 797 型無しラムダ計算に対して単純型を適用する場合、ラムダ抽象の型について考える必要がある。
796 ラムダ抽象は値を取って値を返すため、関数として考えることもできる。 798 ラムダ抽象は値を取って値を返すため、関数として考えることもできる。
797 差し当たりBool型における関数の型を $ \lambda x . t : \rightarrow $ と定義する。 799 差し当たりBool型における関数の型を $ \lambda x . t : \rightarrow $ と定義する。
798 この定義においては $ \lambda x . true $ についても $\lambda x . \lambda y . y $ のような型も同一の型を持つ。 800 この定義においては $ \lambda x . true $ についても $\lambda x . \lambda y . y $ のような型も同一の型を持つ。
863 865
864 最後に関数適用の型付け規則を定義する。 866 最後に関数適用の型付け規則を定義する。
865 867
866 \begin{align*} 868 \begin{align*}
867 \AxiomC{$ \Gamma \vdash t_1 : T_{11} \rightarrow T_{12}$} 869 \AxiomC{$ \Gamma \vdash t_1 : T_{11} \rightarrow T_{12}$}
868 AxiomC{$ \Gamma \vdash t_2 : T_{11}$} 870 \AxiomC{$ \Gamma \vdash t_2 : T_{11}$}
869 \BinaryInfC{$ \Gamma \vdash t_1 \; t_2 : T_{12}$} 871 \BinaryInfC{$ \Gamma \vdash t_1 \; t_2 : T_{12}$}
870 \DisplayProof && \text{T-APP} 872 \DisplayProof && \text{T-APP}
871 \end{align*} 873 \end{align*}
872 874
873 もし $t_1$ が$ T_{11}$の引数を $ T_{12}$の計算結果に移す関数へ評価され、$ t_2$が型$T_{11}$の計算結果にに評価されるのであれば、$t_1$ を $ t_2$に適用した計算結果は $ T_{12}$の型を持つ。 875 もし $t_1$ が$ T_{11}$の引数を $ T_{12}$の計算結果に移す関数へ評価され、$ t_2$が型$T_{11}$の計算結果にに評価されるのであれば、$t_1$ を $ t_2$に適用した計算結果は $ T_{12}$の型を持つ。
874 ブール定数と条件式の型付け規則は型付き算術式と時と同様である。 876 ブール定数と条件式の型付け規則は型付き算術式と時と同様である。
875 877
876 最終的な型付きラムダ計算の規則を示す。 878 最終的な純粋単純型付きラムダ計算の規則を示す。
877 879 純粋とは基本型を持たないという意味であり、純粋単純型付きラムダ計算にはブールのような型を持たない。
878 \begin{definition} 880 この純粋単純型付きラムダ計算でブール値を扱う場合は型環境$\Gamma$を考慮してブール値の規則を追加すれば良い。
879 $ \rightarrow $ (型付き)の項 881
882 \begin{definition}
883 $ \rightarrow $ (型付き)の構文
880 884
881 \begin{align*} 885 \begin{align*}
882 t ::= && \text{項} \\ 886 t ::= && \text{項} \\
883 x && \text{変数} \\ 887 x && \text{変数} \\
884 \lambda x : T . t && \text{ラムダ抽象} \\ 888 \lambda x : T . t && \text{ラムダ抽象} \\
885 t \; t && \text{関数適用} \\ 889 t \; t && \text{関数適用} \\
886 \end{align*} 890 \end{align*}
887 \end{definition} 891
892 \begin{align*}
893 v ::= && \text{項} \\
894 \lambda x : T . t && \text{ラムダ抽象値} \\
895 \end{align*}
896
897 \begin{align*}
898 T ::= && \text{型} \\
899 T \rightarrow T && \text{関数型} \\
900 \end{align*}
901
902 \begin{align*}
903 \Gamma ::= && \text{文脈} \\
904 \emptyset && \text{空の文脈} \\
905 \Gamma , x : T && \text{項変数の束縛} \\
906 \end{align*}
907 \end{definition}
908
909 \begin{definition}
910 $ \rightarrow $ (型付き)の評価($ t \rightarrow t'$)
911
912 \begin{align*}
913 \AxiomC{$t_1 \rightarrow t_1'$}
914 \UnaryInfC{$t_1 \; t_2 \rightarrow t_1' \; t_2$}
915 \DisplayProof && \text{E-APP1} \\
916 \AxiomC{$t_2 \rightarrow t_2'$}
917 \UnaryInfC{$v_1 \; t_2 \rightarrow v_1 \; t_2'$}
918 \DisplayProof && \text{E-APP2} \\
919 (\lambda x : T_{11} . t_{12}) v_2 \rightarrow [ x \mapsto v_2] t_{12} &&
920 \text{E-APPABS}
921 \end{align*}
922 \end{definition}
923
924 \begin{definition}
925 $ \rightarrow $ (型付き)の型付け($\Gamma \vdash t : T $)
926
927 \begin{align*}
928 \AxiomC{$ x : T \in \Gamma$}
929 \UnaryInfC{$\Gamma \vdash x : T $}
930 \DisplayProof && \text{T-VAR} \\
931 \AxiomC{$\Gamma , x : T_1 \vdash t_2 : T_2$}
932 \UnaryInfC{$\Gamma \vdash \lambda x : T_1 . t_2 : T_1 \rightarrow T_2$}
933 \DisplayProof && \text{E-ABS} \\
934 \AxiomC{$ \Gamma \vdash t_1 : T_{11} \rightarrow T_{12}$}
935 \AxiomC{$ \Gamma \vdash t_2 : T_{11}$}
936 \BinaryInfC{$\Gamma \vdash t_1 \; t_2 : t_{12}$}
937 \DisplayProof && \text{T-APP}
938 \end{align*}
939 \end{definition}
940
941 単純型付きラムダ計算の型付け規則のインスタンスも型付き算術式のように導出木をすることで示せる。
942 例えば $ (\lambda x : Bool\; x) \; true $ が空の文脈において $ Bool$を持つことは以下の木で表せる。
943
944 \begin{prooftree}
945 \AxiomC{$ x : Bool \in x : Bool$}
946 \RightLabel{T-VAR}
947 \UnaryInfC{$x : Bool \vdash x : Bool$}
948 \RightLabel{T-ABS}
949 \UnaryInfC{$\vdash \lambda x : Bool . x : Bool \rightarrow Bool$}
950 \AxiomC{}
951 \RightLabel{T-TRUE}
952 \UnaryInfC{$\vdash true : Bool$}
953 \RightLabel{T-APP}
954 \BinaryInfC{$\vdash (\lambda x : Bool . x) \; true : Bool $}
955 \end{prooftree}
956
957 純粋型付きラムダ計算の型システムにおいて、閉じた項に対して進行定理と保存定理は成り立つ\ref{Pierce:2002:TPL:509043}\ref{pierce2013型システム入門プログラミング言語と型の理論}。 % FIXME: 進行定理と保存定理の証明。
958 閉じた項、という制限が付いているのは $ f \; true $ といった自由変数が存在する項は正規形ではあるが値でないからである。
959 しかし、開いた項に関しては評価が行なえないために型システムの検査対象に含まれない。
960
961 % }}}
888 962
889 \section{部分型付け} 963 \section{部分型付け}
890 \section{部分型と Continuation based C} 964 \section{部分型と Continuation based C}