>>328
>//ja.m.wikipedia.org/wiki/%E5%BD%A2%E5%BC%8F%E8%A8%80%E8%AA%9E%E3%81%AE%E9%9A%8E%E5%B1%A4
(引用開始)
形式言語の階層

個々の言語クラスの解説
チョムスキー階層の言語クラスごとに解説する。

タイプ-0内
帰納的可算言語は、部分決定性言語またはチューリング受理性言語とも呼ばれ、対応するオートマトンであるチューリングマシンが受理しない文字列の入力で停止する事が保証されていない言語のクラスである。これを決定性のある、つまりチューリングマシンが常に停止する言語に限定したクラスが帰納言語で、決定性言語またはチューリング決定性言語とも呼ばれる。

これらの計算複雑性はそれぞれ複雑性クラスRとREに対応する。
(引用終り)

ありがとね

１）いま問題にしているのは、>>331にあるように、
　”結論:多くのプログラム言語に対して、その言語で書かれたプログラムの停止性は、決定可能ではない”
　という状況があって、それは”(型のない)ラムダ計算の体系帰納的関数の体系”であったり
　”(理想化された)C言語で書けるプログラム(理想化された)”であったり
　”Java言語で書けるプログラム”であったりすること
２）このような言語で書かれた証明支援プログラムがあったとして
　現在および未来の ”任意”の数学論文をインプットして、必ず正常に停止するとできるのか？
　>>331の答えは、No！
３）勿論、もし”任意の数学論文”→”決定可能の数学論文”に限定すれば、正常に停止するだろう
　でも、それって実質同義反復でしょ