$`\require{color}%
\newcommand{\Keyword}[1]{ \textcolor{green}{ \bf #1} }%
\newcommand{\When}{\Keyword{when\:\:} }%
\newcommand{\And}{ \Keyword{\:\: and \:\:} }%
\newcommand{\Then}{ \Keyword{then\: } }%
\newcommand{\Holds}{ \Keyword{holds\:\:} }%
\newcommand{\cat}[1]{ \mathcal{#1} }%
\newcommand{\tapp}{ \triangleleft }%
\newcommand{\hasT}{ \;\boldsymbol{:}\; }%
`$
型ラムダ抽象と型適用を持つ計算体系。
評価書き換えルール
- 三角が型適用
- ブラケットで置換
- 大文字は型項
- 小文字は項
$`\Holds (\lambda\, \alpha : \cat{X}. t)\tapp T \leadsto t[T/\alpha]\\
\:\\
\When t \leadsto t' \\
\Then\\
\Holds t\tapp T \leadsto t'\tapp T
`$
型推論
$`\When \Gamma , \alpha : \cat{X} \vdash t \hasT T \\
\Then \\
\Holds \Gamma \vdash (\lambda\, \alpha : \cat{X}. t ) \hasT \Pi\,\alpha: \cat{X}. T \\
\:\\
\When \Gamma \vdash t \hasT \Pi\, \alpha:\cat{X}. T \\
\Then \\
\Holds \Gamma \vdash t\tapp T' \hasT T[T'/\alpha]
`$
別な書き方
$`\When t : (\Gamma , \alpha : \cat{X}) \to T \\
\Then \\
\Holds (\lambda\, \alpha : \cat{X}. t ) : \Gamma \to \Pi\,\alpha: \cat{X}. T \\
\:\\
\When t: \Gamma \to \Pi\, \alpha:\cat{X}. T \\
\Then \\
\Holds t\tapp T' : \Gamma \to T[T'/\alpha]
`$
