対象言語の字母

角括弧 [,]

括弧 (,)

自然数 0,1,2,...

行列の定義

行列の連結

バシク行列の式の定義

自然数を角括弧でかこった文字列は式である。

\(\forall n(\lceil[n]\rceil\in\text{BMFml})\)

式の右側に行列を連結させたものも式である

\(\forall \bar m\in \text{Mat}\forall \bar f\in\text{BMFml}(\bar f\bar\frown\bar m\in\text{BMFml})\)

停止状態

\(\forall n(\lceil[n]\rceil\in\text{Halt})\)

簡約

\(\forall t\forall \bar f\in\text{Mat}\forall n(\text{Step}(t)=\lceil[n]\rceil\bar\frown\bar f\bar\frown\lceil(0)\rceil\to\text{Step}(Succ(t))=\lceil[n^n]\rceil\bar\frown\bar f)\)


1行 単純型付きλ計算

2行 大きな型を追加

3行 型の高階化(SytemF_ω)?

4行 ・・・

特に記載のない限り、コミュニティのコンテンツはCC-BY-SA ライセンスの下で利用可能です。