Fandom

巨大数研究 Wiki

コメント0

バシク行列のプログラム

定義

方法論

とりあえず次の形による表現と計算をバシク行列系と呼んでおく。

\(G\frown B\frown N\rightarrow^βG\frown B\frown f(B)\frown f(f(B))\frown\cdots\frown f^n(B))\)

Gは良い部分
Bは悪い部分
Nは右端の列

具体的な定義は関数 f の定義による。

最初から定義を決めて計算するか、計算しながら行列の状態によって定義を決めるかで二手に分かれる。原始数列は前者であり、2行以上のバシク行列は後者となる。任意の定義可能な自然数から自然数への写像はバシク行列系の形で表現することができる、すなわち、関数の定義に関する問題を行列から行列への写像の問題と捉えることができる(自然数を表す記号の解釈や基本となる関数の問題が、場合によっては別途ついてくるものとして)。

述語論理によるプログラム

1行

\(∀a∀b∀c∀c'∀n∀α∀β∀γ[n<ω∧α<γ∧β<γ∧a+b<c']\)

\(Ω_{(n+1)}→Ω_{(n)}\)

\([((s_{(n+1)}=γ→s_(n)=c)\\∧(s_{(n+1)}=α→s_{(n)}=a)\\∧(s_{(n+1)}=β→s_{(n)}=b))\\→a+b<c∧c≦c']\)

\(Ω_{(n)}→Ω_{(n+1)}\)

\([((s_{(n)}=a→s_{(n+1)}=α)\\∧(s_{(n)}=b→s_{(n+1)}=β)\\∧α<β)\\→(s_{(n)}=a+b→s_{(n+1)}=β)∧(s_{(n)}=b+a→s_{(n+1)}=β)]\)

このプログラムは順序数でバシク行列の構造をあらわしただけであり、実際に計算するためには、s_(0) の値ごとにパラメータ t に適用される関数や、収束列の明確な展開の仕方などを書かなければならないが、ここでは割愛する。

言語

(n)(n+1)...((n+1)以上の数列)... で型 (n) の値を表し、(n) #_α が値 α、(n)#_β が値 β を表すとき、(n)#_α(n)#_β は型 (n) の値 α+β を表す( # は (n+1) 以上の数列、+ は * を型変数として *->*->* の抽象的な型=カインド?=2階の型? をもつ多相関数)。

任意の n について \(s_{(n)}∈Ω_{(n)}\) であり、\(Ω_{(n)}\) は全順序関係 \(<_{(n)}\) をもつすべての可算順序数からなる集合。計算可能な範囲のみでプログラムするのであればバシク行列順序数なるものでよい。

値((n)のn)で型を決定することで型の全称量化を可能にしており、多相関数 f_(n):Ω_(n+1)→Ω_(n) を適用していくことで計算をすすめる、推論規則 a:A,f:A→B|-fa:B より戻り値の型も形式的に決めることができる。

1行全体の構造を表現するのに最低でも1階の述語を量化する2階述語論理の表現力を必要とする。

\(∀l[Ω_{(m,0)-(m+n,1)}→Ω_{(m+l\cdot n,0)}]\)

\((s_{(m,0)-(m+n,1)}=γ\to s_{(m,0)-(m+l\cdot n,0)}=c)\\\land(s_{(m,0)-(m+n,1)}=γ'\to s_{(m,0)-(m+l\cdot n,0)}=c')\\\land(s_{(m,0)-(m+n,1)}=α\to s_{(m,0)-(m+l\cdot n,0)}=a)\\\to b<c\land c<c'\)

\(∀l[Ω_{(m+l\cdot n,0)}→Ω_{(m,0)-(m+n,1)}]\)

\(β<α\\\land((s_{(m,0)-(m+n,1)}=α\to s_{(m,0)-(m+l\cdot n,0)}=a')\\\land(s_{(m,0)-(m+n,1)}=β\to s_{(m,0)-(m+l\cdot n,0)}=b')\\\land b'\leq s_{(m,0)}<a))\\\toβ\leq s_{(m,0)-(m+n,1)}<α)\)

ここで \(m+l\cdot n>0\) のとき、\(Ω_{(m+l\cdot n,0)}=Ω_{(m+l\cdot n-1,X)-(m+l\cdot n,0)}\)

\(Ω_{(n,1)-(n+1,0)}→Ω_{(n,1)}\)

\(Ω_{(n,1)}→Ω_{(n,1)-(n+1,0)}\)

(アレ)

Ω_(0) の型は Ω→Ω

Ω_(1) の型は Ω→Ω→Ω

Ω_(2) の型は Ω→Ω→Ω→Ω

・・・

Ω_(1,1) の型は Ω→Ω_(α)

ひとまず保留


プランB

Ω_(0) の型は N→N

Ω_(1) の型は N→N→N

Ω_(2) の型は N→N→N→N

・・・

Ω_(1,1) の型は N→Ω_(n)

Nの値によって戻り値の型が決まる依存関数

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


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

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

Fandomでも見てみる

おまかせWiki