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 (... HaskellHaskellため、これは通常の状況ですが、無限は望ましい答えではありません。したがって、この場合、関数は「嘘」になります。

興味深いことに、完全に機能するソリューションは、上記の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:この記事は、 検索可能なデータ型の 「リテリング」によって少し補足されているため、翻訳としてマークされていません。

Source: https://habr.com/ru/post/J201446/


All Articles