$`\require{color} % 緑色 \newcommand{\In}{ \text{ in }} \newcommand{\mrm}[1]{ \mathrm{#1} } \newcommand{\Keyword}[1]{ \textcolor{green}{\text{#1}} }% \newcommand{\For}{\Keyword{For } } % 使用 \newcommand{\Let}{\Keyword{Let } }% 使用 \newco…

判断シーケント＝関数定義があるとする。$`\quad a : (\Gamma \vdash t : \beta)`$これを次のようにパックする。$`\quad (a : [\Gamma \to \beta], a := t^\wedge)`$ここで、$`t^\wedge`$ は項のフルカリー化。パックした定義は、環境コンテキストに追加でき…

$`\require{color} % 緑色 \newcommand{\Keyword}[1]{ \textcolor{green}{\text{#1}} }% \newcommand{\Providing}{\Keyword{Providing } }% \newcommand{\When}{\Keyword{When } }% \newcommand{\And}{\Keyword{And } }% \newcommand{\Holds}{\Keyword{Holds…

単に「コンテキスト」は混合コンテキスト 純コンテキスト＝宣言コンテキスト 混合コンテキスト＝宣言と定義のリスト 定義は、宣言（x:A）と割り当て（x:=t）のペア シーケントは三種類： 判断シーケント、事実シーケント、質問シーケント 判断シーケントは、…

ムービーはデータ構造 ムービーはフレームとトランジションからなる。 フレームはステージの構造的な集まり。 ステージはツリー構造を持つ。カレントステージが一意に決まる。 ステージは、シーケントとサブステージの集まり。 シーケントは判断シーケントか…

宣言のみからなるテレスコープ〈依存レコード | 指標〉を純コンテキストと呼ぶことにする。宣言と割り当てが混じったコンテキストを混合コンテキストと呼ぶ。純コンテキスト〈指標〉のあいだの手続きは多型判断〈poly-typejudgement〉と言ってもよい。次が予…