関数
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)
つまり、
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:この記事は、
検索可能なデータ型の 「リテリング」によって少し補足されているため、翻訳としてマークされていません。