ローダー数の数式的定義
- 1 モチベーション
- 2 数式的定義
- 2.1 準備
- 2.2 代入と正規化
- 2.2.1 \(S(v, y, c, t)\)
- 2.2.2 \(A(y, x)\)
- 2.2.3 \(L(x)\)
- 2.3 推論
- 2.4 ローダー数
過去の記事「ユーザーブログ:KawamoYurase/ローダー数の再定式化」ではわかりやすさを優先し、loader.cの出力とは異なる数を定義していたが、今回は本当にローダー数をc言語ではない方法で定義する。この記事だけでローダー数が何をやっているか理解するのは不可能に近いので、過去記事「ユーザーブログ:KawamoYurase/ローダー数を理解しよう(1):_プログラムの書き直し編」や「ユーザーブログ:KawamoYurase/ローダー数を理解しよう(2):_理論背景」を適宜参照してほしい。
非負整数のペア\(x, y\)をエンコードする関数を次で定義する。 \[\langle x, y \rangle = (2x+1)2^y\]
逆に、任意の自然数\(n\)について、\(n = (2x+1)2^y\)となる非負整数\(x, y\)は一意であるから、それを用いて \[l(n) = x, \; r(n) = y\] と定義する。
\(S(v, y, c, t)\)、\(A(y, x)\)、\(L(x)\)を次で定義する。
- \(a = l(t)\)、\(x = r(t)\)とする。
- \(a = 0\)または\(a = 1\)の場合、
- \(S(v, y, c, t) = \langle a, \langle S(v, y, c, l(x)), S(v+1, L(y), c, r(x)) \rangle\rangle\)
- \(a = 2\)の場合、
- \(S(v, y, c, t) = A(S(v, y, c, l(…
Extreme Shitagaki
- 1 もはや何でもない \(\Psi\)
- 1.1 激しく疑わしいOCF
- 1.2 \(T, PT, RT, KT\)
- 1.3 \(m\)
\(\pi\)は常に非可算正則基数を表す。
\(C(\alpha, \beta)\)は以下の閉包:
- \(\beta \cup \{0, K\}\)
- \((\xi, \eta) \mapsto \xi+\eta\)
- \(\xi \mapsto \omega^\xi\)
- \(\xi \mapsto \Xi(\xi)\)ただし\(\xi < \alpha\)
- \((\xi, \pi, \delta) \mapsto \Psi^\xi_\pi(\delta)\)ただし\(\xi \le \delta < \alpha\)
\(M^0 = K \cap Lim\)とし、\(\alpha > 0\)について \[ M^\alpha = \left\{ \pi < K \colon \begin{array}{rl} & \pi = K \cap C(\alpha, \pi) \land \alpha \in C(\alpha, \pi) \\ & \land (\forall \xi \in C(\alpha, \pi) \cap \alpha) [M^\xi \, \text{is stationary in} \, \pi] \end{array} \right\} \] と定める。
\[\Xi(\alpha) = \min(M^{\alpha} \cup \{K\})\]
\(\xi \leq \alpha\)について、 \[ \Psi^\xi_\pi(\alpha) = \min(\{\rho \in M^\xi \cap \pi \colon \rho = C(\alpha, …
ローダー数を理解しよう(2): 理論背景
今回はCoCが一体何物かを見ていく。
- 1 注意事項
- 2 ラムダ計算
- 2.1 型なしラムダ計算
- 2.1.1 β簡約
- 2.1.2 遊んでみよう：真偽値
- 2.1.3 チャーチ・ロッサー性
- 2.1.4 止まらないβ簡約
- 2.2 型付きラムダ計算
- 2.2.1 強正規化性
- 2.1 型なしラムダ計算
- 3 CoC
- 3.1 形式
- 3.1.1 項
- 3.1.2 自由変数
- 3.1.3 文脈
- 3.1.4 代入
- 3.1.5 推論ルール
- 3.2 推論ルールの意味
- 3.2.1 Productルール
- 3.2.1.1 \((s_1, s_2) = (*, *)\)のとき
- 3.2.1.2 \((s_1, s_2) = (\Box, *)\)のとき
- 3.2.1.3 \((s_1, s_2) = (*, \Box)\)のとき
- 3.2.1.4 \((s_1, s_2) = (\Box, \Box)\)のとき
- 3.2.1 Productルール
- 3.1 形式
- 4 Curry-Howard 同型対応
- 4.1 単純型付きラムダ計算において
- 4.2 CoCにおいて
- 4.2.1 型に依存する項
- 4.2.2 型に依存する型
- 4.2.3 項に依存する型
- 4.2.4 無矛盾性
- 4.2.5 直観論理
- 4.2.6 PropとSet
- 4.2.7 エンコードが引き起こす問題
- 5 de Bruijn index
- 5.1 型なしラムダ計算において
- 5.1.1 自由変数
- 5.2 CoCにおいて
- 5.2.1 β簡約
- 5.1 型なしラムダ計算において
- 6 System U、ECCと強められたAbstractionルール
筆者は計算機科学を専攻していない。誤った理解に基づく記述が含まれている可能性があり、この記事だけを読んでわかった気になるのは危険である。また、相当お気持ちに寄った記述をしていて、厳密な話が少なくなってしまっている。たとえば、「のようなもの」という表現が頻出するが、「のようなもの」は「そのものだと思うと痛い目に合う」という意味だと思ってほしい。
ラムダ計算は、「計算」という概念を抽象化したものであ…
ローダー数を理解しよう(1): プログラムの書き直し編
ローダー数はくそむずい。loader.cはBignum Bakeoffのエントリーであるため、512文字に収めるために悪魔のような書き方がされている。今回はとにかくloader.cを人類が読める状態に持っていくことを目標とする。プログラムの動作の内容には深く立ち入らない。
今回解説するプログラムはローダーのプログラムのリポジトリにあるが、Gwikiに記載があるloader.cはリポジトリには陽に含まれていない。リポジトリをクローンし、makeすることで出力されるreduced.cがそれである。
pair.cとpure.cを連結しfull.cを得る。 そのfull.cをperlスクリプトpure.plで変換することで得られるreduced.cがloader.cとしてエントリーされている。 pure.plは変数名の置換を行い、極限まで文字列を圧縮する役割を担う。 本質的な難しさはfull.cにあるとみて良いだろう。
今回はpair.cおよびpure.cの解説を行うことでloader.cの解説の代わりとする。 その前にC言語に関する知識を整理することから始める。
Cに真偽値型(bool)はない。代わりに（少なくともloader.cが扱う範囲では）0のみが偽の役割をし、0以外の全てが真としてふるまう。
たとえばif(a - b) { A; } else { B; }はa-bが0でないときにAが、0の時にBが実行される。
関係演算子などは偽のとき0に、真のとき1に評価される。
たとえば3 < 0は偽なので0、-1 0 ? a : b;はy > 0のときにxがaに代入され、y
Denisの弱マーロψについて
- 1 モチベーション
- 1.1 巨大関数
- 1.1.1 急増加関数
- 1.1.2 極限形
- 1.1.3 巨大関数
- 1.1 巨大関数
- 2 参考
Denisの弱マーロ\(\psi\)
- \(m = 0\)ならば、\(c_m := D(\textrm{dom}(c),0)\)である。
- \(m \neq 0\)ならば、\(c_m := D(\textrm{dom}(c),[c,c_{m-1}])\)である。
- \(n = \otimes(m,1_S)\)を満たす\(m \in \mathbb{N}\)が存在するならば、\([a,n] := D(b,[c,c_m])\)である。
- \(n = \otimes(m,1_S)\)を満たす\(m \in \mathbb{N}\)が存在しないならば、\([a,n] := 0\)である。
写像 \begin{eqnarray*} f \colon T \times \mathbb{N} & \to & \mathbb{N} \\ (a,n) & \mapsto & f_a(n) \end{eqnarray*} を次のように再帰的に定義する：
- \(a = 0\)のとき、\(f_a(n) := n+1\)である。
- それ以外のとき、\(f_a(n) := f_{[a, \otimes(n,1_S)]}(n)\)である。
写像 \begin{eqnarray*} \Lambda \colon \mathbb{N} & \to & T \\ n & \mapsto & \Lambda(n) \end{eqnarray*} を次のように再帰的に定義する：
- \(n = 0\)のとき、\(\Lambda(n) = N \oplus 1_S\)である。
- それ以外のとき、\(\Lambda(n) = W(\Lambda(n-1))\)である…