FANDOM


昔バシク行列の強さと計算可能性を計ろうとして失敗したシステム。

原則の整理

情報とは、0と1の数列や物体の配列など、手段や媒体は何でもいいが、可算無限の意味を表すことができる表現である。

任意の意味AとBにつき、AをBへ移す写像fが存在する。

任意の意味Aにつき、Aを含むクラスが存在する。

定義域Aの要素を値域Bの要素へ移す写像fはAとBどちらにも含まれない。

任意の写像fにつきfについて閉じているクラスが存在する。

以上のすべての意味を記述できる言語はいかなる関数も記述できるが、そのような言語は存在しない。

(関数型言語はすべてを関数として表現する。関数にあちこち写される情報のあり方やデータ構造を重視するのがオブジェクト指向、たぶん)

用意するもの

環境 \(Γ\);

すべての自然数とその型 \(0:M(0),1:M(0),2:M(0),\cdots\)

ここではすべての自然数からなる集合をM(0)とする。

後者関数とその型 \(m(1)::=λn.f(nfx):N→N\)

多相関数 \(λx.nx:*→*\)

ここで自然数 n がすでに多相的な扱いをされている。

再帰 \(f(f)\)

型推論

\(\displaystyle \frac{Γ|-f:∀α.α→α\quadΓ|-x:A}{Γ|-f(x):A}\)

m(n)変換

\(m(n)\in M(n)\)

\(M(n+1)::=M(n)→M(n)\)

αが極限順序数のとき、

\(M(α)::=\cup_{n<ω}M(α_n)\)

\(m(α+1)m_α::=let\ f=m_α\ in\ f(f)\)

注意:ラムダ式で書いてしまうと具体的な型を決定してしまってうまくいかない。

n>0 として、

\(m(α+n+1)::=λm.nm:M(α+n)→M(α+n)\)

\(m(ω+2)m(ω+1)m(ω)(x)=f_{ε_0}(x)\)

以上で m(ω^ω) つまり f[φ(ω,0)] まで計算可能

m(n) 変換では多相化の範囲が有界であるため、λx.nx をバシク行列ほど広く利用できない。

2階ラムダ計算、System F で計算できる関数の上限は \(ψ_Ω(Ω_ω)\)

高階多相ラムダ計算で \(ψ_Ω(Ω_Ω)\)

λΠ2で \(ψ_Ω(ψ_{χ(ω,0)}(0))\)

λΠω すなわちCoCで \(ψ_Ω(ε_{M+1})\) 、これはKP + "There exists a recursively Mahlo ordinal"の証明論強さであり、ローダー数は \(f[ψ_Ω(ε_{M+1})+1](5)\) と近似される。

多相的に直接巨大数を生成する関数クラスの定義

\((N\to N)\in U^f\)

\(*\in U^f\leftrightarrow(*→*)\in U^f\)

\((*\in m(α)^f\leftrightarrow(*→*)\in m(α)^f)→m(α)\in U^f\)

On^(n+1):On^(n)の極限を数え上げるクラス

Γ_0(On^(n))mapsto On^(n+1)

Γ_α:Γ_β(β<α)によって写されるすべてのクラスの不動点を数え上げるクラスへ移す作要素

型演算

広告ブロッカーが検出されました。


広告収入で運営されている無料サイトWikiaでは、このたび広告ブロッカーをご利用の方向けの変更が加わりました。

広告ブロッカーが改変されている場合、Wikiaにアクセスしていただくことができなくなっています。カスタム広告ブロッカーを解除してご利用ください。

FANDOMでも見てみる

おまかせWiki