106

Haskell のような純粋な関数型言語では、全単射の関数の逆関数 (編集) を取得するアルゴリズムはありますか? そして、あなたの機能をプログラムする特定の方法はありますか?

4

10 に答える 10

105

場合によっては、はい！Bidirectionalization for Free!という美しい論文があります。これは、関数が十分に多相的である場合に、逆関数を完全に自動的に導出できるいくつかのケースについて説明します。(関数がポリモーフィックでない場合に何が問題を難しくするかについても説明します。)

関数が可逆である場合に得られるのは、(偽の入力による) 逆です。それ以外の場合は、古い入力値と新しい出力値を「マージ」しようとする関数が得られます。

于 2012-11-15T19:25:47.090 に答える
37

いいえ、一般的にはありえません。

証明: 型の全単射関数を考える

type F = [Bit] -> [Bit]

と

data Bit = B0 | B1

inv :: F -> Fのようなインバータがあると仮定しinv f . f ≡ idます。関数 についてテストしたとしますf = id。

inv f (repeat B0) -> (B0 : ls)

この最初の出力はある有限時間の後に来たに違いないため、この結果を取得するためにテスト入力を実際に評価した深さと、呼び出し可能な回数の両方にB0上限があります。関数ファミリを定義するninvf

g j (B1 : B0 : ... (n+j times) ... B0 : ls)
   = B0 : ... (n+j times) ... B0 : B1 : ls
g j (B0 : ... (n+j times) ... B0 : B1 : ls)
   = B1 : B0 : ... (n+j times) ... B0 : ls
g j l = l

明らかに、すべて0<j≤nのg jは全単射であり、実際には自己逆です。だから確認できるはず

inv (g j) (replicate (n+j) B0 ++ B1 : repeat B0) -> (B1 : ls)

しかし、これを満たすには、次のinv (g j)いずれかが必要でした

  • g j (B1 : repeat B0)の深さまで評価するn+j > n
  • head $ g j l一致する少なくともn異なるリストを評価するreplicate (n+j) B0 ++ B1 : ls

その時点まで、 の少なくとも 1 つはg jと見分けがつかず、これらの評価のいずれも行っていないfため、それを区別することはできませんでした。.inv finvIO Monad

                                                                                                                                   ⬜</p>

于 2012-11-15T20:21:34.437 に答える
19

ウィキペディアで調べることができます。これはReversible Computingと呼ばれています。

ただし、一般的にはそれを行うことはできず、関数型言語にはそのオプションがありません。例えば：

f :: a -> Int
f _ = 1

この関数には逆関数がありません。

于 2012-11-15T18:58:26.543 に答える
16

ほとんどの関数型言語ではなく、ロジック プログラミングまたはリレーショナル プログラミングでは、定義するほとんどの関数は実際には関数ではなく「関係」であり、これらは双方向で使用できます。たとえば、prolog または kanren を参照してください。

于 2012-11-16T03:54:02.187 に答える
11

このようなタスクは、ほとんどの場合決定不能です。いくつかの特定の機能に対する解決策はありますが、一般にはありません。

ここでは、どの関数に逆関数があるかさえ認識できません。Barendregt、HP The Lambda Calculus: Its Syntax and Semanticsを引用。北オランダ、アムステルダム (1984) :

ラムダ項のセットは、それが空でも完全なセットでもない場合、自明ではありません。A と B が (ベータ) 等式で閉じた 2 つの非自明な互いに素なラムダ項の集合である場合、A と B は再帰的に分離できません。

A を可逆関数を表すラムダ項の集合とし、残りを B とします。両方とも空ではなく、ベータ等価で閉じています。したがって、関数が可逆かどうかを判断することはできません。

(これは、型指定されていないラムダ計算に適用されます。TBH 反転したい関数の型がわかっている場合に、引数を型指定されたラムダ計算に直接適用できるかどうかはわかりません。しかし、そうなることはかなり確信しています。似ている。）

于 2012-11-15T20:52:24.987 に答える
11

関数のドメインを列挙でき、範囲の要素が等しいかどうかを比較できる場合は、かなり簡単な方法でできます。列挙とは、利用可能なすべての要素のリストを持つことを意味します。私は Ocaml を知らないので、Haskell に固執します (または、適切に大文字にする方法さえも ;-)

あなたがしたいことは、ドメインの要素を実行し、それらが反転しようとしている範囲の要素と等しいかどうかを確認し、機能する最初のものを取得することです:

inv :: Eq b => [a] -> (a -> b) -> (b -> a)
inv domain f b = head [ a | a <- domain, f a == b ]

あなたはそれfが全単射であると述べたので、そのような要素は1つだけ存在するはずです. もちろん、秘訣は、ドメインの列挙が実際に有限時間内にすべての要素に到達するようにすることです。Integerからへの全単射を反転しようとしている場合、負の数にはならないためInteger、 を使用して[0,1 ..] ++ [-1,-2 ..]も機能しません。具体的にinv ([0,1 ..] ++ [-1,-2 ..]) (+1) (-3)は、決して値を生成しません。

ただし、0 : concatMap (\x -> [x,-x]) [1..]これは次の順序で整数を実行するため、機能します[0,1,-1,2,-2,3,-3, and so on]。確かinv (0 : concatMap (\x -> [x,-x]) [1..]) (+1) (-3)にすぐに戻ります-4！

Control.Monad.Omegaパッケージは、タプルなどのリストを良い方法で実行するのに役立ちます。そのようなパッケージは他にもあると思いますが、私はそれらを知りません。

もちろん、このアプローチは、見苦しく非効率的であることは言うまでもなく、かなり控えめで力ずくの方法です。それで、あなたの質問の最後の部分、全単射を「書く」方法についてのいくつかの発言で終わります。Haskell の型システムは、関数が全単射であることを証明するまでには至っていません - そのために Agda のようなものが本当に必要です - しかし、それは喜んであなたを信頼します。

(警告: テストされていないコードが続きます)

したがって、型と型Bijectionの間に s のデータ型を定義できますか:ab

data Bi a b = Bi {
    apply :: a -> b,
    invert :: b -> a 
}

次のように、好きなだけ多くの定数 (「私はそれらが全単射であることを知っています!」と言うことができます) とともに:

notBi :: Bi Bool Bool
notBi = Bi not not

add1Bi :: Bi Integer Integer
add1Bi = Bi (+1) (subtract 1)

そして、次のようないくつかのスマートコンビネータ:

idBi :: Bi a a 
idBi = Bi id id

invertBi :: Bi a b -> Bi b a
invertBi (Bi a i) = (Bi i a)

composeBi :: Bi a b -> Bi b c -> Bi a c
composeBi (Bi a1 i1) (Bi a2 i2) = Bi (a2 . a1) (i1 . i2)

mapBi :: Bi a b -> Bi [a] [b]
mapBi (Bi a i) = Bi (map a) (map i)

bruteForceBi :: Eq b => [a] -> (a -> b) -> Bi a b
bruteForceBi domain f = Bi f (inv domain f)

invert (mapBi add1Bi) [1,5,6]その後、実行して取得できると思います[0,4,5]。コンビネータを賢く選択すれば、定数を手で書かなければならない回数はBiかなり減ると思います。

結局のところ、関数が全単射であることがわかっている場合は、その事実の証明スケッチが頭の中にあることを願っています.Curry-Howard同型はプログラムに変換できるはずです:-)

于 2012-11-15T21:59:04.667 に答える
6

私は最近このような問題に取り組んでいますが、いいえ、(a) 多くの場合は難しくありませんが、(b) まったく効率的ではありません。

基本的に、あなたが を持っていると仮定するとf :: a -> b、それfは確かに bjiection です。f' :: b -> a逆数は非常にばかげた方法で計算できます。

import Data.List

-- | Class for types whose values are recursively enumerable.
class Enumerable a where
    -- | Produce the list of all values of type @a@.
    enumerate :: [a]

 -- | Note, this is only guaranteed to terminate if @f@ is a bijection!
invert :: (Enumerable a, Eq b) => (a -> b) -> b -> Maybe a
invert f b = find (\a -> f a == b) enumerate

fが全単射であり、enumerate真に のすべての値を生成する場合、最終的にそのようなものaにヒットします。af a == b

Boundedとインスタンスを持つ型はEnum簡単に作成できRecursivelyEnumerableます。タイプのペアEnumerableも作成できEnumerableます。

instance (Enumerable a, Enumerable b) => Enumerable (a, b) where
    enumerate = crossWith (,) enumerate enumerate

crossWith :: (a -> b -> c) -> [a] -> [b] -> [c]
crossWith f _ [] = []
crossWith f [] _ = []
crossWith f (x0:xs) (y0:ys) =
    f x0 y0 : interleave (map (f x0) ys) 
                         (interleave (map (flip f y0) xs)
                                     (crossWith f xs ys))

interleave :: [a] -> [a] -> [a]
interleave xs [] = xs
interleave [] ys = []
interleave (x:xs) ys = x : interleave ys xs

型の論理和についても同じことが言えEnumerableます:

instance (Enumerable a, Enumerable b) => Enumerable (Either a b) where
    enumerate = enumerateEither enumerate enumerate

enumerateEither :: [a] -> [b] -> [Either a b]
enumerateEither [] ys = map Right ys
enumerateEither xs [] = map Left xs
enumerateEither (x:xs) (y:ys) = Left x : Right y : enumerateEither xs ys

との両方でこれを行うことができるという事実は(,)、Either任意の代数データ型に対して行うことができることを意味します。

于 2012-11-15T21:58:11.353 に答える
5

すべての関数に逆関数があるわけではありません。議論を 1 対 1 の関数に限定すると、任意の関数を逆にする機能により、任意の暗号システムをクラックする機能が付与されます。理論上でも、これが実現可能ではないことを願っています。

于 2012-11-15T19:00:13.763 に答える
4

いいえ、すべての関数に逆数があるわけではありません。たとえば、この関数の逆はどうなるでしょうか?

f x = 1
于 2012-11-15T18:57:04.360 に答える