ごとけんです

In message "[ruby-math:00393] Re: [ruby-list:28415] class Real"
    on 01/03/05, Shin-ichiro HARA <sinara / blade.nagaokaut.ac.jp> writes:
>>無限数列で実数を表す方法は 整数列を小数表現とみなす方法
>>、連分数表現等色々ありますが 有理数の Cauchy 列で
>>表現したものを idea が分かる程度に省略して書いておきます。
>>下手に書き直すと bug が入りますので、元の形のままで書きます。
>>
>>Real.rb

これは、Pour-El & Richards の computable real の枠組が与える
モノとほぼ同等ですね。もとの枠組は実数というか Banach space
で定義されていますが Frech\'et space でも構成できることが分
かっています。

Rubyでやる場合の問題点は、みなさんがおっしゃるように精度保証
をどう書くかにあると思います。証明系だけをMLなんかで実装するっ
てのは面白いかも。ブロックを駆使して method signature に凝る
のも、まぁ面白いんですがやっぱり本質的な部分が解決されないと
いま一つという感が強いです。

-- Gotoken
# 参考までに、もとの定義のさわりを抜粋します。

# Marian B. Pour-El and Jonathan I. Richards, # ``Computability in analysis and physics'', # Springer-Verlag, Berlin (1989) より :有理数列 <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) がなりたつことをいう. :実数列 <x_n> が計算可能である とは k->∞ のとき x_n にeffectiveに収束する有理2重数列 <r_{n,k}> が存在することをいう. 有理2重数列が「effectiveに収 束する」とは, ある帰納的関数 e:N×N->N が存在して, k >= e(n,m) ならば |r_{n,k} - x{n}| <= 2**(-m) がなりたつことをいう. :実関数 f:I^q->R (ただしIは実区間)が計算可能である とは, 一様ノルムのもとで f にeffective に収束する計算可能な 有理多項式列 <p_m(x)> が存在する, すなわち, ある帰納的関数 e: N->N が存在して, m >= e(n) ならば |f(x) - p_m(x)| <= 2**(-n) がなりたつことをいう. 結局、関数合成に関しては、必要な精度を与える項数 e() をどう 合成するかが問題になります。ただし、初等関数については特に難 しいわけではありません。なお、このような e() を持たなければ 必要な精度をどれだけ待てば得ることが出来るのかが分からないと いう意味で実効的(effective)ではないというのがこの理論の骨子 です. かなり広く認知されている考え方だと思います.