Fandom

巨大数研究 Wiki

コメント0

計算と証明

独自研究よりの内容のメモ。

超数学の視点から、ある理論で全域性を証明できることを以て計算可能性の証明としてもいいが、そういうのはやめておく。その理論の無矛盾性の証明がなければ数学的な正確さに缺けるというのもある。

動機

証明とは、公理と呼ばれる前提条件から推論規則を有限回適用して、正しいということを示したい論理式を導き出すことを言う。公理と推論規則は本質的に区別がつくものではない。

矛盾した公理からは任意の論理式が証明できてしまうため、本当に正しい証明を得るためにはその前提条件が無矛盾でなければならない。しかし無矛盾であることの証明自体にも同じことが言えてしまう。そのため、本当に正しい証明は、たとえ存在するとしてもそれがなんであるかを知ることができない、ということになってしまう。

そこで、逆に無条件で正しいとする前提条件を作り、そこから矛盾が導かれる場合は推論規則なり方法論なりが間違っているとする立場について考える。

たとえば、「1」を入力されたら「真」という記号を、「0」を入力されたら「偽」という記号を返して停止する機械があるとする。この機械は「真」と「偽」を同時に出力することはないため矛盾(の形)が導かれてしまうことはない。

計算と証明の関係

type as proposition の立場から、モダスポーネンスが関数の適用に当たる。

ゲーデル数を利用して妥当性を形式的に確認することができるために不完全性定理が成り立ってしまう。

計算複雑性について

強化学習やディープラーニングなどは、専門的なことはさておき、原理からみてプログラミングをするプログラムということになる(実際はそこまで大層なものではないという意見もあるだろうが)。その強化されるプログラムは外界からの入力に対しより良い出力を返すことを旨とする。停止性の問題より、入力は型理論を応用して適切だと判断されたもののみを受け取るなり、入力する側が決まった範囲でしか入力しないなりの制限を設ける必要がある。そんなこんなで任意のプログラムが自分自身よりも複雑なプログラムを意図して返すことは、(イエス様の奇跡レベルの偶然にでも頼らない限り)不可能である。意図する意識の存在や奇跡については信仰の問題となる。

言語Lによって書かれるプログラムの列 σ_0,σ_1,σ_2,...

原始再帰

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


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

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

Fandomでも見てみる

おまかせWikia