ライス=シャピロの定理

計算可能性理論において、ライス=シャピロの定理: Rice-Shapiro theorem)とはライスの定理の一般化した定理である。名称は Henry Gordon Rice と Norman Shapiro に因む。[1]

非形式的な言明 編集

定理の主張は非形式的には次のように述べられる: 計算可能関数の半決定可能な述語 A と、計算可能関数 f が与えられたとき、 fA を満たす為には、f の有限部分で A を満たすものが存在することが必要十分である。いま fA を満たしていると仮定しよう。するとライス=シャピロの定理より f の有限部分 g が存在して A を満たす。このとき g の任意の計算可能な延長関数もまた A を満たす。したがって計算可能関数の無限個の入出力が真偽の決定に関与するような述語は帰納的可算ではありえない。

形式的な言明 編集

いま A を(1変数)部分帰納的関数の集合で、指標の集合  帰納的可算であるものとする。ここに   は部分帰納的関数のアクセプタブル・ナンバリングである。

このとき任意の部分帰納的関数   について、次は同値:

  •  ;
  • 有限関数    かつ   なるものが存在する。

ここで有限関数とは有限な定義域を持つ部分関数をいう。また   とは   の定義域で   が成り立つこと(   の制限であること)をいう。

一般に、次の主張が成り立つ: 集合   が帰納的可算であることと、次の2つの条件を満たすこととは同値である:

  •   は帰納的可算;
  •   であることと、有限関数    かつ   なるものが存在することとは同値。ここで    の標準的な指標である。

証明 編集

A を部分帰納的関数の集合で、指標の集合   が帰納的可算であるものとする。

まず fA に属す部分帰納的関数で、f のいかなる有限部分関数も A に属さないと仮定する。帰納的でない帰納的可算集合   を取る(例えば   として停止性問題の対角線を取ればよい)。次の部分帰納的関数を考える:

 

ここで   は有限集合の帰納的な増大列で   が成り立つようなものとする。smn定理より   なる全域帰納的関数 h が存在する。明らかに   が成り立つ。次の2つの場合が考えられる:

  •    に属すとき:   が成り立つ。したがって   の定義域は有限である。仮定より f のいかなる有限部分も A に属さないから、  が成り立つ。
  •    に属さないとき:   が任意の y で成り立つ。したがって   が成り立つ。仮定より fA に属すから、  が成り立つ。

したがって   多対一還元可能である。   は帰納的可算であるから、   も帰納的可算である。これは   の取り方に反する。

次に fA に属さない部分帰納的関数で、 f の有限部分 gA に属すものが存在すると仮定する。帰納的でない帰納的可算集合   を取る。次の部分帰納的関数を考える:

 

smn定理より   なる全域帰納的関数 k が存在する。明らかに   が成り立つ。次の2つの場合が考えられる:

  •    に属すとき:   が成り立つ。仮定より fA に属さないから、   が成り立つ。
  •    に属さないとき:   が成り立つ。仮定より gA に属すから、   が成り立つ。

したがって    に多対一還元可能である。   は帰納的可算であるから、   も帰納的可算である。これは   の取り方に反する。

ライスの定理の導出 編集

ライス=シャピロの定理はライスの定理の一般化となっている。 A を部分帰納的関数の集合で、指標の集合  帰納的であるものとする。A が空な関数を含むならば、ライス=シャピロの定理より A は部分帰納的関数全体に一致する。 A が空な関数を含まないならば、補集合がそれを含むから、ライス=シャピロの定理より A の補集合が部分帰納的関数全体に一致する。これはライスの定理の主張にほかならない。

注釈 編集

  1. ^ Rogers Jr., Hartley (1987). Theory of Recursive Functions and Effective Computability. MIT Press. ISBN 0-262-68052-1 

参考文献 編集

  • Cutland, Nigel (1980). Computability: an introduction to recursive function theory. Cambridge University Press ; Theorem 7-2.16.
  • Rogers Jr., Hartley (1987). Theory of Recursive Functions and Effective Computability. MIT Press. pp. 482. ISBN 0-262-68052-1 
  • Odifreddi, Piergiorgio (1989). Classical Recursion Theory. North Holland 

関連項目 編集