パスワードを忘れた? アカウント作成
61388 journal

okkyの日記: 停止性問題のいやらしいところ 9

日記 by okky

ちょっとだけ書いておく。

http://ja.wikipedia.org/wiki/%E5%81%9C%E6%AD%A2%E6%80%A7%E5%95%8F%E9%A1%8C の証明の部分を読めば判るが、停止性問題を常に正しく解くプログラムHは存在しないというこの証明は、プログラムHが「Hを含んだ系を正しく処理できる」と仮定すると自己矛盾を引き起こすことを利用している。別に H が「全ての」処理系を正しく判断できるかどうかは関係なかったりする。

つまり Pを含む系の正しさをPで正しく解くことはできない のがポイントなのだ。

これはつまり、あるプログラム H1 の正しさを証明しようとすると、それは H1ではなく、別の処理系 H2を持ってこなくてはいけない、という事になる。じゃぁ、H2は? H3が必要になる…とこのようにして無限の信頼の鎖が必要になるがこのチェーンは半無限に続く(一方の端は H1だが、他方の端 Hn をあらわすような有限の数 n は存在しない)。

半無限に続いてもどこかで輪になってくれれば…と期待する向きもあろうが、これも駄目。

話を簡単にするために H5 は H6で証明でき、H6は H5で証明できる、と仮定しよう。すると H5( H6 ( H5 )) が正しく処理できることになる。しかしこれは、外側の H5が正しく処理できる系は H5自身を含んでいることになる。

これは別に2つで輪を作るのでなく、いくつで輪を作っても一緒だ。信頼の鎖を輪にするということは、その瞬間に自己言及性が発生することになってしまう。つまりこの鎖を輪の状態につなぐことは許されない。

.

ただし、これは分岐を許さない、というわけではない。信頼の鎖はプログラム Hi間を有方向グラフでつないだ物なので、分岐とマージは許される。

   → B →
  A        D
   → C →

のように A から D へ到達するパスがB とCの2つある、というのはOKなのだ。

.

で。このときに。どこまでが証明できて、どこからが証明できなくなるのか、というのが議論されている話。現在わかっているのは、「かなりの確率で、あらゆるものが空中楼閣」ということ。

.

昔、星新一の娘さんだったかが、「この宇宙は全体が自由落下中なだけ」という趣旨のショートショートを書いて、星新一さんが「これはすばらしい」とほめていた、という記憶がある。

われわれのよって立っている論理も、自由落下中なのかもしれない。

少なくとも、「証明」できるかどうかに、「証明者が人間かどうか」は関係ない、ということすら判らない人がごろごろいる事からかんがみるに、ほとんどの人の知能はフリーフォールで低下中、と言えよう。
大前研一が『「知の衰退」からいかに脱出するか?』なんて本を書く気になる気持ちが、すごくよく判った。

この議論は、okky (2487)によって ログインユーザだけとして作成されたが、今となっては 新たにコメントを付けることはできません。
  • バグは事実存在しないかも知れない。 しかし、存在しないという証明はできないんだよね、残念ながら。
    悪魔の証明に他ならないんだから、自明だと思うんだけどなぁ……

    • 悪魔の証明は、あくまでも「規模問題」に見えます。なので、こういう話がわからない人には、悪魔の証明は「証明可能」に見えてしまうのですよ。

      例えばここに 1Mbit のプログラムがあるとします。

      21Mパターン全部作って、動かしてみればどれが正しいかわかるじゃん

      他人に責任とかを丸投げして、自分では何もしないくせに「俺がいないとあいつらは仕事をしない」とか寝言をほざく連中には、規模問題と言う概念が無いので、こういうことを平気で言うのです。

      .

      別の例。

      「このソフトウェアに対する 100時間連続稼動テストを、3日で終わらせろ」

      この程度の算数すらやらない人間が蔓延しているのです。できるできないではなく、やらない。

      .

      とりあえずこういう連中に参政権を与えてはいけないと思うんですが…。

      --
      fjの教祖様
      親コメント
  •  dodongaです。
     コメントを書いてプレビュ~で落とされました;;
     http://srad.jp/~dodonga/journal/467710
     に断片が、いや、欠片を書いておきました。

    > http://ja.wikipedia.org/wiki/%E5%81%9C%E6%AD%A2%E6%80%A7%E5%95%8F%E9%A1%8C の
    > 証明の部分を読めば判るが、

     ???。
     このWikipediaの解説は"無限ル~プ"がミスリ~ドされてますので参考にはなりません。

    > 停止性問題を常に正しく解くプログラムHは存在しないというこの証明は、
    > プログラムHが「Hを含んだ系を正しく処理できる」と仮定すると自己矛盾を引き起こすことを利用している。
    > 別に H が「全ての」処理系を正しく判断できるかどうかは関係なかったりする。 

     ???。
     数学用語での "∀全ての" "∀任意の" "∃在る" "¬否定" "⇒"  "∃存在する" etc
     解って言ってますか?。

    > つまり Pを含む系の正しさをPで正しく解くことはできない のがポイントなのだ。

     ???。
     Pの定義は?
     甘んじて論理体系としても主張が理解出来ません。
     もしかして、ゲ~デルの不完全定理を言ってます?それだと主張は判らなくなります;;
     説明ください。

    > 話を簡単にするために H5 は H6で証明でき、H6は H5で証明できる、と仮定しよう。

     ???。
     停止性問題の説明が「読めば判る」と仰っているのに、なんでこの仮定が出でくるのでしょうか?

    > すると H5( H6 ( H5 )) が正しく処理できることになる。しかしこれは、外側の H5が正しく処理できる系は
    > H5自身を含んでいることになる

     ???。
     この式で考えるのならば含んでいません。H6は真か偽しか返さないですから。
    #真偽は0,1でもいいです。

    > これは別に2つで輪を作るのでなく、いくつで輪を作っても一緒だ。信頼の鎖を輪にするということは、
    > その瞬間に自己言及性が発生することになってしまう。
    > つまりこの鎖を輪の状態につなぐことは許されない。

     ???。
     説明ください;;。

    > 信頼の鎖はプログラム Hi間を有方向グラフでつないだ物なので、分岐とマージは許される。
    >
    > → B →
    > A D
    > → C →
    >
    > のように A から D へ到達するパスがB とCの2つある、というのはOKなのだ。

     ???。
     説明ください;;。

    > で。このときに。どこまでが証明できて、どこからが証明できなくなるのか、というのが議論されている話。

     議論されている場所はどこですか?
     証明の前提、目的と証明先を教えてください。

    > 現在わかっているのは、「かなりの確率で、あらゆるものが空中楼閣」ということ。

     ???。

     停止性問題はいずこに?

    <<

     盛大は釣りですか?

     表のコメントは擁護してたつもりだたけど。

     釣られた表の方はナムですね
    --
    閑話休題
    •  dodongaです。

       この日記で気づいた「信頼の絆」。表にも書いてあったね。表での議論と何処が関係在るの?
       噛み合うわけ無いじゃない。

       信頼の絆でしょ?。これこそ「停止性問題の決定不能性定理」の典型じゃない。

       アホかい。

       表でもここでの私でも、話が噛み合う訳ないではないですか。
       しっかりと、表のコメントへに自分自身でオフトピつけてください。

       前日記の

      > チューリングの停止性不能問題を理解していない、証明って何? すらも理解していない、
      > そんな人間がこんなにたくさんいることには絶望した。

       には、ほのちょっと同情しちゃたけどね。
       
       okkyさんも理解してないようで。

      #ここへはコメント付けないでください。
      #上のコメントに私の疑問に答えながらコメント付けて下さい。

       付ける気があるならばねxxx。付けられないよねw^^。
       停止性問題を正しく理解してない事がこの日記に書いてあるもの。
       証明を正しく理解してない事がこの日記に書いてあるもの。
      --
      閑話休題
      親コメント
    • そもそも dodonga さんのほうが何もわかっていないとしか見えない。
      前提知識をどこまで戻ればいいのか判らないじゃないか。

      まず、不完全性定理と停止性問題は同質ではない。停止性問題の証明は「第1不完全性定理」を完全に包括していない。第2も包括していない。がそれぞれの部分集合を持っている。停止性問題は「アルゴリズム」というものの持つ性質であり、それはつまり「証明」と言うものが持っている性質。ここまでは大前提として判っているのか?

      さらに、既存のプログラムが「書ける」事と「あるプログラムP がある性質を持っている事を証明する」事とは話が違う、と言うこともわかっているか?!

      議論されている場所はどこですか?

      君は AMS [ams.org]も知らないでこういうことにくちばしを突っ込もうとしているのか?

      --
      fjの教祖様
      親コメント
      •  dodongaです。

        > 前提知識をどこまで戻ればいいのか判らないじゃないか。

         私は、どこまででもかまいませんですよ^^。
        # でも、Chain of Trust の詳細まではご勘弁を;

         私、一応、数学科出です。それなりにはついて行けます。本職はプログラマですが;;。

         こいう掲示板ですと何を、何処まで深く、書いたら良いか迷うのは確かです;

         でも、okkyさんとはでは遠慮いらないですね。
         私も大丈夫です。

         AMS でてきてびくりしました。最近はもう観に行てないです;;。
         もう、数学は鉛筆でしかしてないです。

        >>閑話休題<<

        > 不完全性定理と停止性問題は同質ではない。
        > 停止性問題の証明は「第1不完全性定理」を完全に
        > 包括していない。第2も包括していない。
        > がそれぞれの部分集合を持っている。
        > 停止性問題は「アルゴリズム」というものの持つ
        > 性質であり、それはつまり「証明」と言うものが
        > 持っている性質。ここまでは大前提として判って
        > いるのか?

         心得ています。大丈夫です。
         この記述は、私の

        |> つまり Pを含む系の正しさをPで正しく解くこと
        |> はできない のがポイントなのだ。
        |
        | ???。
        |
        | Pの定義は?
        | 甘んじて論理体系としても主張が理解出来ません。
        | もしかして、ゲ~デルの不完全定理を言って
        | ます?それだと主張は判らなくなります;;
        | 説明ください。

         を、受けてだと思います。

         「Pを含む系の正しさをPで正しく解くことはできない のがポイントなのだ。」

         が、私には引っかかったからです。表でも不完全定理がごちゃになっていた方が
         いましたから。

         それ以降の私の???は元日記の議論がChain of Trust
         へと移っていた事に私の理解が追いついて無かったからです。

         2通目の私の投稿はそれに対する愚痴です。
         読み流してください;;
         御詫びしても足らないですが、2つめの投稿は無視してください;;。
         文面、悪く申し訳ありませんでした。

         停止性問題からいきなりChain of Trustへと議論が変わていたので

         「停止性問題は何処に?」

         になてたのです。

         表の方達も同じだたのではないでしょうか。

        > さらに、既存のプログラムが「書ける」事と
        > 「あるプログラムP がある性質を持っている事を証明する」
        > 事とは話が違う、と言うこともわかっているか?!

         これも、心得ています。常日頃仕事で日々努力・意識してやています。
         あ、こう言い換えないと正確には当てはまらないですけど;

         「あるプログラム(関数・サブル~チン・クラス)P をある性質を持っている様に記述する」

        # なまじ、こな意識で書いていると上司とぶつかります;;
        # 考え無し人のソ~スのメンテを渡されると頭が割れそうになります;

         ところで、2点だけ質問させてください。
        1)
        |> http://ja.wikipedia.org/wiki/%E5%81%9C%E6%AD%A2%E6%80%A7%E5%95%8F%E9%A1%8C の
        |> 証明の部分を読めば判るが、
        |
        | ???。
        | このWikipediaの解説は"無限ル~プ"がミスリ~ドされてますので参考にはなりません。

        この点はどうお考えでしょうか?

        2)
        |> 停止性問題を常に正しく解くプログラムHは存在しないというこの証明は、
        |> プログラムHが「Hを含んだ系を正しく処理できる」と仮定すると自己矛盾を引き起こすことを利用している。
        |> 別に H が「全ての」処理系を正しく判断できるかどうかは関係なかったりする。 
        |
        | ???。
        | 数学用語での "∀全ての" "∀任意の" "∃在る" "¬否定" "⇒"  "∃存在する" etc
        | 解って言ってますか?。
         失言いぱいです;;

         上記Wikipediaの証明と記号が同じだとすると、Hは決定性を持ていると定義して議論していますが、
         この文の意図は何なになのでしょうか。

        最後に、表で纏めたものの私の投稿文で締めさせていただて終わりたいと思います。

        >>
         なんか、収集がつかなくなってそうなので個人的な意見も入れて整理をば。

          1)現状のプログラミング言語でのプログラムには停止性問題は適用出来ない。

          2)バグがあるかないかはTuring機械の停止性とは全く関係がない。

          3)停止性と第二不完全定理を混ぜて議論するのは意味が無い。

          4)第一不完全定理と第二不完全定理は"全くの"別物である。

         1)は、複雑すぎるのです。アセンブリ言語レベルまで落とせば出来そうです^^
         2)は、"バグ有り"のプログラムは停止もするかもだし、停止しないかもです。
          前提で間違っているので、議論の俎上には乗りません。

          お話が複雑になちゃうのは、「停止性問題の決定不能性定理」は存在定理であって
          証明の結果は「存在しない」となてる事です。

         3)は、目指す対象がまたく違います。分けて考えましょう。
         4)は、書いた通りです。別物です。

        <<
        --
        閑話休題
        親コメント
        • 横から茶々を入れますが、私自身は数学とは仲が良くなかったし、専門的な高等教育も受けてもいません。
          よってとんちんかんなことを言っていないとは限りません。知らない者ほど単純に考えるものですから。
          そこんとこ、割り引いて読んでいただきたい。

           1)現状のプログラミング言語でのプログラムには停止性問題は適用出来ない。
           1)は、複雑すぎるのです。アセンブリ言語レベルまで落とせば出来そうです^^

          単純系か複雑系かは関係ないと思いますが。
          入力したプログラムがどういう結果を返すか/返さないかを「完全に判定可能」である。という仮定はそのためでしょう?
          要点は「完全に判定可能」という仮定であって、入力されるプログラムは宇宙、人生、その全てを求めるモノでも構わない。
          なにせ、チューリングマシンは「完全に判定可能」なんですから。
          違いますか?

          親コメント
typodupeerror

「毎々お世話になっております。仕様書を頂きたく。」「拝承」 -- ある会社の日常

読み込み中...