From: gotoken@... (GOTO Kentaro)
Date: 1999-02-18T19:49:38+09:00
Subject: [ruby-dev:5281] Re: a genericity

ごとけんです

In message "[ruby-dev:5272] Re: a genericity"
    on 99/02/18, 石塚圭樹 <keiju@Rational.Com> writes:

>けいじゅ＠日本ラショナルソフトウェアです.
>
>面白かったのでちょっとだけ(^^;;;
># 私を悪の道に引きづり込まないで下さい(^^;;;

# どうも何かが共鳴してしまうようで(^^;;

>計算可能な実数というのは, プログラムが有限時間内で停止し, その時点で確
>定する数ですよね?  
>
>今回のばあいは, プログラムは必ずしも値を確定して停止しなくて良くて, 数
>そのものがだんだんとあるところに近付けば良いだけですよね? この場合でも
>やはり, 計算可能な実数にしか到達できないんでしょうかね? 

その定義では，近付いていることをどうやって知れば良いのかが
わからないのでナイーヴに過ぎると思います．
どっちにしろプログラムの濃度の可算性から逃れることが出来ないし，
結論から言うと得ることが出来るのは計算可能な実数だけです．
ちゃんとした定義は次のようになります．

  「有理数列 {r_n} が計算可能である」とは帰納的な関数
   a,b,s: N->N が存在して，
      r_n = (-1)**s(n) * a(n) / b(n) 
  と書けることをいう．

  「実数 x が計算可能である」とは x に effective に収束
  する計算可能な有理数列 {r_n} が存在することをいう．
  ここで「effective に収束する」とは，帰納的関数 e:N->N
  が存在して，
      k >= e(n) ならば |x - r_k| <= 2**n
  がなりたつことをいう．

effective な収束という制限をいれておくことで，どれだけ
計算すれば必要な桁が得られるかがわかるのでこれは本質的
です．ただ，この制限が計算可能性にどれほどの制限を与え
てるのか，もしくは制限を与えているのかは不明です．

>>実際は，列や関数を収束に基づいて定義することが出来るので
>>その上での演算も定義されます．
>
>そうです. これが重要なんですね.

なんですよね．
これらも上の定義と同様に，計算可能な二重有理数列などを
定義することで得られます．これらの結果は Grzegorczyk 
により50年代にはじめられ，Poul-El と Richards によって
80年代に確立されました．

>PS.
>なんかRubyの話しから飛んでいますね(^^;;;

こんな話ばっかりに反応するのはナニですね(^^;;;

-- gotoken