순수 함수형 언어에서 역함수를 얻는 알고리즘이 있습니까?

순수 함수형 언어에서 역함수를 얻는 알고리즘이 있습니까?

---

Haskell과 같은 순수 함수 언어에서 함수의 역수를 얻는 알고리즘이 있습니까? (편집) 그것이 bijective 일 때? 기능을 프로그래밍하는 특정 방법이 있습니까?

---

어떤 경우에는 그렇습니다! Bidirectionalization for Free 라는 아름다운 논문이 있습니다 ! 여기서는 함수가 충분히 다형성 인 경우에 대해 완전히 자동으로 역함수를 유도 할 수있는 몇 가지 경우를 설명합니다. (또한 함수가 다형성이 아닐 때 문제를 어렵게 만드는 요인에 대해서도 설명합니다.)

함수가 가역적 일 경우 얻을 수있는 것은 역 (스퓨리어스 입력)입니다. 다른 경우에는 이전 입력 값과 새 출력 값을 "병합"하려는 함수를 얻습니다.

---

아니요, 일반적으로 불가능합니다.

증명 : 유형의 bijective 함수 고려

type F = [Bit] -> [Bit]

와

data Bit = B0 | B1

다음 inv :: F -> F과 같은 인버터가 있다고 가정 합니다 inv f . f ≡ id. 우리가 함수를 테스트 한 말 f = id것을 확인하여,

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

B0출력의 첫 번째 값 은 일정 시간이 지나야하므로이 결과를 얻기 위해 테스트 입력을 실제로 평가 n한 깊이와 inv호출 할 수있는 횟수 에 대한 상한 이 있습니다 f. 이제 함수 제품군 정의

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

최대 그 시점에,의 적어도 하나 g j에서 구별 f하고 있기 때문에 inv f이러한 평가 중 하나 다하지 않았다, inv아마도 떨어져 말했다 수 없었다 -에서만 가능하다, 자신의 일부 런타임 측정을하는 짧은 IO Monad.

                                                                                                                                   ⬜

---

위키피디아에서 찾아 볼 수 있습니다 . 그것은 Reversible Computing 이라고 합니다.

일반적으로 당신은 그것을 할 수 없으며 기능적 언어에는 그 옵션이 없습니다. 예를 들면 :

f :: a -> Int
f _ = 1

이 함수에는 역이 없습니다.

---

대부분의 기능적 언어가 아니라 논리 프로그래밍 또는 관계형 프로그래밍에서 정의하는 대부분의 함수는 실제로 함수가 아니라 "관계"이며 양방향으로 사용할 수 있습니다. 예를 들어 프롤로그 또는 칸렌을 참조하십시오.

---

함수의 영역을 열거 할 수 있고 범위의 요소가 같은지 비교할 수 있다면 다소 간단한 방식으로 할 수 있습니다. 열거한다는 것은 사용 가능한 모든 요소의 목록을 갖는 것을 의미합니다. 나는 Ocaml을 모르기 때문에 Haskell을 고수 할 것입니다 (또는 그것을 적절하게 대문자로 쓰는 방법까지도 ;-)

원하는 것은 도메인의 요소를 통해 실행하고 반전하려는 범위의 요소와 동일한 지 확인하고 작동하는 첫 번째 요소를 가져 오는 것입니다.

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

그것이 fbijection 이라고 말 했으므로 그러한 요소는 단 하나뿐입니다. 물론 비결은 도메인 열거가 실제로 유한 한 시간 내에 모든 요소 에 도달하도록하는 것 입니다. 당신이에서 전단 사 함수를 반전하려는 경우 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의 패키지는 당신이 좋은 방법 튜플 등등의 목록을 통해 실행 도움이 될 수 있습니다; 그런 패키지가 더 많이있을 거라고 확신합니다.하지만 모르겠습니다.

---

물론,이 접근 방식은 추악하고 비효율적 인 것은 말할 것도없고 다소 낮은 편이고 무차별 적입니다! 그래서 나는 당신의 질문의 마지막 부분, bijections를 '쓰기'하는 방법에 대한 몇 가지 언급으로 끝낼 것입니다. Haskell의 타입 시스템은 함수가 bijection이라는 것을 증명하는 것이 아닙니다. 당신은 정말로 Agda와 같은 것을 원합니다. 그러나 그것은 당신을 기꺼이 신뢰합니다.

(경고 : 테스트되지 않은 코드는 다음과 같습니다)

따라서 Bijection유형 a과 사이 에 s 의 데이터 유형을 정의 할 수 있습니다 b.

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

다음과 같이 원하는만큼의 상수 ( 'I know they 're bijections!' 라고 말할 수 있음 )와 함께 :

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)

I think you could then do invert (mapBi add1Bi) [1,5,6] and get [0,4,5]. If you pick your combinators in a smart way, I think the number of times you'll have to write a Bi constant by hand could be quite limited.

After all, if you know a function is a bijection, you'll hopefully have a proof-sketch of that fact in your head, which the Curry-Howard isomorphism should be able to turn into a program :-)

---

Tasks like this are almost always undecidable. You can have a solution for some specific functions, but not in general.

Here, you cannot even recognize which functions have an inverse. Quoting Barendregt, H. P. The Lambda Calculus: Its Syntax and Semantics. North Holland, Amsterdam (1984):

A set of lambda-terms is nontrivial if it is neither the empty nor the full set. If A and B are two nontrivial, disjoint sets of lambda-terms closed under (beta) equality, then A and B are recursively inseparable.

Let's take A to be the set of lambda terms that represent invertible functions and B the rest. Both are non-empty and closed under beta equality. So it's not possible to decide whether a function is invertible or not.

(This applies to the untyped lambda calculus. TBH I don't know if the argument can be directly adapted to a typed lambda calculus when we know the type of a function that we want to invert. But I'm pretty sure it will be similar.)

---

I've recently been dealing with issues like this, and no, I'd say that (a) it's not difficult in many case, but (b) it's not efficient at all.

Basically, suppose you have f :: a -> b, and that f is indeed a bjiection. You can compute the inverse f' :: b -> a in a really dumb way:

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

If f is a bijection and enumerate truly produces all values of a, then you will eventually hit an a such that f a == b.

Types that have a Bounded and an Enum instance can be trivially made RecursivelyEnumerable. Pairs of Enumerable types can also be made 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

Same goes for disjunctions of Enumerable types:

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

The fact that we can do this both for (,) and Either probably means that we can do it for any algebraic data type.

---

Not every function has an inverse. If you limit the discussion to one-to-one functions, the ability to invert an arbitrary function grants the ability to crack any cryptosystem. We kind of have to hope this isn't feasible, even in theory!

---

No, not all functions even have inverses. For instance, what would the inverse of this function be?

f x = 1

---

In some cases, it is possible to find the inverse of a bijective function by converting it into a symbolic representation. Based on this example, I wrote this Haskell program to find inverses of some simple polynomial functions:

bijective_function x = x*2+1

main = do
    print $ bijective_function 3
    print $ inverse_function bijective_function 3

data Expr = X | Const Double |
            Plus Expr Expr | Subtract Expr Expr | Mult Expr Expr | Div Expr Expr |
            Negate Expr | Inverse Expr |
            Exp Expr | Log Expr | Sin Expr | Atanh Expr | Sinh Expr | Acosh Expr | Cosh Expr | Tan Expr | Cos Expr |Asinh Expr|Atan Expr|Acos Expr|Asin Expr|Abs Expr|Signum Expr|Integer
       deriving (Show, Eq)

instance Num Expr where
    (+) = Plus
    (-) = Subtract
    (*) = Mult
    abs = Abs
    signum = Signum
    negate = Negate
    fromInteger a = Const $ fromIntegral a

instance Fractional Expr where
    recip = Inverse
    fromRational a = Const $ realToFrac a
    (/) = Div

instance Floating Expr where
    pi = Const pi
    exp = Exp
    log = Log
    sin = Sin
    atanh = Atanh
    sinh = Sinh
    cosh = Cosh
    acosh = Acosh
    cos = Cos
    tan = Tan
    asin = Asin
    acos = Acos
    atan = Atan
    asinh = Asinh

fromFunction f = f X

toFunction :: Expr -> (Double -> Double)
toFunction X = \x -> x
toFunction (Negate a) = \a -> (negate a)
toFunction (Const a) = const a
toFunction (Plus a b) = \x -> (toFunction a x) + (toFunction b x)
toFunction (Subtract a b) = \x -> (toFunction a x) - (toFunction b x)
toFunction (Mult a b) = \x -> (toFunction a x) * (toFunction b x)
toFunction (Div a b) = \x -> (toFunction a x) / (toFunction b x)


with_function func x = toFunction $ func $ fromFunction x

inverse X = X
inverse (Const a) = Const a
inverse (Plus (Const a) b) = (Subtract (inverse b) (Const a))
inverse (Plus b (Const a)) = inverse (Plus (Const a) b)
inverse (Mult (Const a) b) = (Div (inverse b) (Const a))
inverse (Mult b (Const a)) = inverse (Mult (Const a) b)
inverse (Negate a) = Negate $ inverse a
inverse (Asin x) = Sin $ inverse x
inverse (Acos x) = Cos $ inverse x
inverse (Atan x) = Tan $ inverse x
inverse_function x = with_function inverse x

This example only works with arithmetic expressions, but it could probably be generalized to work with lists as well.

참고URL : https://stackoverflow.com/questions/13404208/in-pure-functional-languages-is-there-an-algorithm-to-get-the-inverse-function