【シプサ】5 帰着可能性 (その3)

こつこつ。E[LBA]の判定可能性から。丁寧に追ってみる。

• 「E[LBA]は判定不可能である」
  
  
  
  • A[TM]からの帰着で確認する。E[LBA]が判定可能 -> A[TM]が判定可能。どう帰着できるか。
    
  • 「TM Mと入力 w に対してあるLBA B を構成する。LBA Bの空性検査をすると、Mがwを受理できるかどうか判定できる」ということを実現できればよさげ。しかしBはどんなものか?
    
    
    
    • Bは、「wに対するMの計算履歴の表現」を入力として受け取る。
      
    • そして、それが受理計算履歴なときにそれを受理する。ちょっとメタ。
      
    • するとL(B)は、たったひとつの文字列を含むか、空集合かである。
      
    • こんな方針。
      
    
    
  • 整理して書いてみる。
    
    
    
    • E[LBA]を判定するTM R が存在するとする。
      
    • TM Mとwがある。
      
    • TM Sがあり、それはMとwに応じて動作(自己構成?)する次のような機構をもっている。
      
      
      
      • TM S は、Mとwから上で述べたLBA Bを構成する。
        
        
        
        • LBA Bの概要。
          
        • LBA Bの入力は計算状態を"#"で区切って連結したものとする。
          
        • C1が開始状態であり、Clが受理状態であり、CiからCi+1がMの遷移関数によって導出されることを確認する。
          
        
        
      • LBA Bから表現<B>を作る。
        
      • それをRに入力する。
        
      • Rがそれを受理するならば、Sは拒否する。Rがそれを拒否するならば、Sは受理する。
        
      
      
      
    • このTM Sは、A[TM]を判定する。
      
    • A[TM]は判定不可能だから矛盾が発生しており、仮定したTM Rは存在しない。
      
    • ゆえにE[LBA]は判定不可能である。■
      
    
    
  
  

これ結構複雑だよなぁ。