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
이 함수에는 역이 없습니다.
답변
대부분의 기능적 언어가 아니라 논리 프로그래밍 또는 관계형 프로그래밍에서 정의하는 대부분의 함수는 실제로 함수가 아니라 “관계”이며 양방향으로 사용할 수 있습니다. 예를 들어 프롤로그 또는 칸렌을 참조하십시오.
답변
이와 같은 작업은 거의 항상 결정할 수 없습니다. 일부 특정 기능에 대한 솔루션을 가질 수 있지만 일반적이지 않습니다.
여기에서는 어떤 함수에 역이 있는지조차 인식 할 수 없습니다. Barendregt, HP Lambda 미적분 : 구문 및 의미론을 인용 합니다. 노스 홀랜드, 암스테르담 (1984) :
람다 용어 집합은 비어 있거나 전체 집합이 아니면 중요하지 않습니다. A와 B가 (베타) 평등으로 닫힌 두 개의 사소하고 분리 된 람다 용어 집합이면 A와 B는 재귀 적으로 분리 할 수 없습니다.
A를 가역 함수를 나타내는 람다 항의 집합으로, 나머지 B를 취합시다. 둘 다 비어 있지 않으며 베타 평등하에 닫힙니다. 따라서 함수가 반전 가능한지 여부를 결정할 수 없습니다.
(이것은 유형이 지정되지 않은 람다 미적분에 적용됩니다. TBH 우리가 반전하려는 함수의 유형을 알고있을 때 인수가 유형이 지정된 람다 미적분에 직접 적용될 수 있는지 여부는 알 수 없습니다.하지만 그럴 것이라고 확신합니다. 비슷한.)
답변
함수의 영역을 열거 할 수 있고 범위의 요소가 같은지 비교할 수 있다면 다소 간단한 방식으로 할 수 있습니다. 열거한다는 것은 사용 가능한 모든 요소의 목록을 갖는 것을 의미합니다. 나는 Ocaml을 모르기 때문에 Haskell을 고수 할 것입니다 (또는 그것을 적절하게 대문자로 쓰는 방법까지도 😉
원하는 것은 도메인의 요소를 통해 실행하고 반전하려는 범위의 요소와 동일한 지 확인하고 작동하는 첫 번째 요소를 가져 오는 것입니다.
inv :: Eq b => [a] -> (a -> b) -> (b -> a)
inv domain f b = head [ a | a <- domain, f a == b ]
그것이 f
bijection 이라고 말 했으므로 그러한 요소는 단 하나뿐입니다. 물론 비결은 도메인 열거가 실제로 유한 한 시간 내에 모든 요소 에 도달하도록하는 것 입니다. 당신이에서 전단 사 함수를 반전하려는 경우 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 동형이 프로그램으로 바뀔 수있는 그 사실에 대한 증명 스케치가 머릿속에 있기를 바랍니다. 🙂
답변
나는 최근에 이와 같은 문제를 다루고 있으며, 아니오, (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
, 당신은 결국 공격 할 것이다 a
그러한를 f 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
우리가 어떤 대수 데이터 형식을 위해 그것을 할 수 있다는 것을 아마 의미합니다.