Haskell-不可能は可能ですか？

関数Integer -> Bool



が真であるかどうかを判断するタスクは、少なくとも1つの数値に対して計算上不溶性であることが知られています。 ただし、一見、このようなオラクル（つまり、関数(Integer -> Bool) -> Maybe Integer



）のように見えるものについては、この記事で説明します。



まず、自然数のタイプを設定します。ほとんど文字通り、通常の数学的定義に従います（これが将来必要になる理由）。

 data Nat = Zero | Succ Nat deriving (Eq, Ord, Show)
      
      

        
        
        
      

    
        
        
        
      
      

        
        
        
      

    
     

言い換えると、正の整数はゼロか、1だけ増加した正の整数のいずれかです（後続からのSucc



）。



また、便宜上、この表現の数値に基本操作（加算、乗算、 Integer



からの変換）を定義します。

 instance Num Nat where Zero + y = y Succ x + y = Succ (x + y) Zero * y = Zero Succ x * y = y + (x * y) fromInteger 0 = Zero fromInteger n = Succ (fromInteger (n-1))
      
      

        
        
        
      

    
        
        
        
      
      

        
        
        
      

    
     

これまでのところ、通常のInteger



とこのタイプの違いに関して特別なものはないようです。



(Nat -> Bool) -> Maybe Nat



の形式の関数が必要であることを思い出してください。その結果は、入力関数がTrue



返す数値、またはそのような数値がない場合はNothing



なります。 最初の近似は、たとえば、同様の関数です。

 lyingSearch :: (Nat -> Bool) -> Nat lyingSearch f | f Zero = Zero | otherwise = Succ (lyingSearch (f . Succ))
      
      

        
        
        
      

    
        
        
        
      
      

        
        
        
      

    
     

実際、目的の番号が存在する場合、この関数が正しい答えを返すことはほぼ明白です。 実際、 f Zero == True



場合、戻り値はZero



-trueになります。 それ以外の場合、関数はx+1



を返します。ここで、 x



は関数f(x+1)



が真である値です-これも真です。

ただし、この関数の名前はlyingSearch



ます：必要な数が存在しない場合、関数はすべてのステップで再帰に行き、実際には無限を返します： Succ (Succ (Succ (...



Haskell



怠Haskell



ため、これは通常の状況ですが、無限は望ましい答えではありません。したがって、この場合、関数は「嘘」になります。



興味深いことに、完全に機能するソリューションは、上記のlyingSearch



関数に基づいて作成できます。 次のように定義されたsearch



機能を検討してください。

 search f | f possibleMatch = Just possibleMatch | otherwise = Nothing where possibleMatch = lyingSearch f
      
      

        
        
        
      

    
        
        
        
      
      

        
        
        
      

    
     

一見したところ、これがどのように機能し、どのように機能するかは明らかではありません。 簡単な例を見てみましょう。

 ghci> search (\x -> x*x == 16) --     lyingSearch Just (Succ (Succ (Succ (Succ Zero)))) ghci> search (\x -> x*x == 15) Nothing
      
      

        
        
        
      

    
        
        
        
      
      

        
        
        
      

    
     

つまり、 search



関数は、15に等しい正方形の自然数は存在しないと正しく判断しました。



実際、見れば、すべてが簡単です。 lyingSearch



（これは常にNat



型の有効な値です）から可能な結果を​​受け取ったので、単純にf



の入力に送り、戻り値を確認します。 目的の番号が存在する場合、（既に説明したように） possibleMatch



はその番号であるため、チェックは成功します。 そうでなければ、なぜなら f



入力値f



終了し、 False



を取得してNothing



を返します。



search



関数は実際にすべての述語に対して機能し（ Nat->Bool



関数）、有限時間で終了します（もちろん、 f



Nat



型の値f



も終了する場合）。 ただし、渡された引数の終了条件f



は非常に強力であり、許容される述語のセットを強く制限します。たとえば、 fx = x*x + 1 == x



、無限ループが発生します。 そのような関数は任意の数で終了するため、これはそうではないように思われますか？ すでに述べた無益さ以外の人には、等号の左右に無限にネストされたSucc (Succ (Succ (...



、したがって、左右が等しいかどうかを判断することはできません。このため、この関数を使用することはできません。 Integer



同様のタイプを作成します。



これで、すべてが常に終了する関数である理由と方法を簡単な言葉で説明できます。 結局、 f



が渡された無限大で終わる場合、つまり、シーケンスSucc (Succ (Succ (...



、その後、いずれの場合も、固定数のSucc



コンストラクターを使用する（開く）だけです。



本質的に同じ方法で、他のタイプのsearch



などの関数を作成できます。 比較的単純な例も実数であり、それぞれが無限の数のリストとして表されます（「 一見不可能な機能プログラム」を参照）。 ハッキングには、適切なモナドと関連機能を提供する汎用パッケージinfinite-searchがあります。



PS：この記事は、 検索可能なデータ型の 「リテリング」によって少し補足されているため、翻訳としてマークされていません。