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

함수의 영역을 열거 할 수 있고 범위의 요소가 같은지 비교할 수 있다면 다소 간단한 방식으로 할 수 있습니다. 열거한다는 것은 사용 가능한 모든 요소의 목록을 갖는 것을 의미합니다. 나는 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)

나는 당신이 할 수 invert (mapBi add1Bi) [1,5,6]있고 얻을 수 있다고 생각합니다 [0,4,5]. 콤비 네이터를 현명하게 선택한다면 Bi손 으로 상수 를 작성해야하는 횟수 가 상당히 제한 될 수 있다고 생각합니다 .

결국, 함수가 bijection이라는 것을 안다면, Curry-Howard 동형이 프로그램으로 바뀔 수있는 그 사실에 대한 증명 스케치가 머릿속에 있기를 바랍니다. 🙂

답변

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

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

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