構成的でないが計算可能

[仕事の話なので、いずれ、加筆修正の上、本業のページに移動の予定]

最近の論文[1]から数年前の私の仕事[2]がやや唐突に参照されているのをみつけた。[1]では、Bishop流構成的数学でDiniの定理はBrouerの fan theorem （日本語はなんだろう）と同値であり、つまり、Diniの定理は構成的でないことを示している。そこの注釈で、にもかかわらず、計算可能性解析学でDiniの定理の実効的版が示されたとして、[2]が参照されている。

どうやら、構成的でないが計算可能な例をみつけてしまったらしい。中間値の定理もそういうものだとすでに知られているので、特に不思議なことではないが、微妙なことには違いない。ちょっと追いかけてみたほうがよいかな。

というか、BergerさんとSchusterさんが追いかけてくださると、私は楽なんだけど。

[1] Josef Berger and Peter Schuster: Classifying Dini's Theorem, Notre Dame J. Formal Logic 47, no. 2 (2006), 253-262.
[2] Hiroyasu Kamo: Effective Dini's Theorem on Effectively Compact Metric Spaces, Proceedings of the 6th Workshop on Computability and Complexity in Analysis (CCA 2004), Electronic Notes in Theoretical Computer Science, 120, (2005), 73-82.