Haskell - 최대 (xs ++ map (x +) xs)를 최대 (최대 xs) (x + 최대 xs)로 변환하는 방법

Question

"Thinking Functionally With Haskell"의 한 가지는 프로그램을보다 효율적으로 사용하는 것입니다. 융합 법. 나는 답을 되풀이하려고 애쓰는 데 어려움을 겪고있다.

계산의 일부는 등식 추론을 통해 maximum (xs ++ map (x+) xs)을 max (maximum xs) (x + maximum xs)으로 변환해야합니다.

maximum는 foldr1 max로 정의하고 내가 foldr1을 둘러싼 많은 규칙을 알고하지 않는 한 나는 foldr1 max (xs ++ map (x+) xs)max (foldr1 max xs) (foldr1 max (map (x+) xs))에 그래서 내가 이해하고자하는 첫 번째 일이 변환하는 경우에도 첫 번째 부분에 붙어있어.

일단 지나면 다음 부분이 더 복잡해집니다. 즉 foldr1 max (map (x+) xs)을 x + foldr1 max xs으로 변환합니다. 직관적으로 말이 되네. 모두 'x'가 추가 된 숫자 묶음의 최대 값을 찾으면 'x'가 추가되고 결과에 'x'가 추가되기 전에 모든 숫자의 최대 값을 찾는 것과 같습니다.

이 두 번째 단계에서 나를 돕기 위해 찾은 유일한 것은 this stack overflow answer 입니다. 여기서 평상시와 같이 이해할 수있는 개별 단계가 없기 때문에 대답은 기본적으로 주어집니다 (p = q라고 가정 할 경우). 추리.

그렇다면 변형을 수행하는 단계를 보여줄 수 있습니까?

Answer 1

이것은 유도에 의해 알 수 있습니다.

xs == []이라고 가정합니다. 양 표현은 모두 error이므로 모두 true입니다. 가정하자

, xs == [y]

maximum([y]++map(x+)[y]) == -- by definition of map 
         == maximum([y]++[x+y]) 
          -- by definition of ++ 
         == maximum([y,x+y]) 
          -- by definition of maximum 
         == foldr1 max [y,x+y] 
          -- by definition of foldr1 
         == max y (foldr1 max [x+y]) 
          -- by definition of foldr1 
         == max y (x+y) 
          -- by definition of foldr1 and maximum [y] 
         == max (maximum [y]) (x+maximum [y]) 

다음으로, 우리는 maximum의 교환 법칙을 증명해야합니다 maximum (xs++(y:ys)) == max y (maximum (xs++ys))을 - 당신이 증거를 생략하고 maximum (y:ys ++ map(x+)(y:ys))의 증거로 바로 갈 경우, 필요한이 알 - 하나 계단 중간에서 (x+y)을 이동해야합니다. ys++(x+y):map(x+)ys.

가정 xs==[] :

maximum ([]++(y:ys)) == maximum (y:ys) 
        -- by definition of foldr1 and maximum 
        == max y (maximum ys) 
        == max y (maximum ([]++ys)) 

가정 xs==x:xx :

maximum(x:xx++(y:ys)) == maximum (x:(xx++(y:ys))) 
        -- by definition of foldr1 and maximum 
         == max x (maximum (xx++(y:ys))) 
        -- by induction 
         == max x (max y (maximum (xx++ys))) 
-- by commutativity of max, max a (max b c) == max b (max a c) 
         == max y (max x (maximum (xx++ys))) 
        -- by definition of foldr1 and maximum 
         == max y (maximum (x:(xx++ys))) 
        -- by definition of ++ 
         == max y (maximum ((x:xx) ++ ys)) 

좋아, 지금은 원래의 문을 증명 다시 얻을. 당신은 유도에 의해 증명 될 수있는 유도하는 방법과 특정 일을 참조하는 방법에 대해도 요구하기 때문에 지금, xs == y:ys

maximum (y:ys ++ map(x+)(y:ys)) == 
-- by definition of map 
         == maximum(y:ys ++ (x+y):map(x+)ys) 
-- by definition of foldr1 and maximum 
         == max y (maximum(ys ++ (x+y):map(x+)ys) 
-- by commutativity of maximum 
         == max y (max (x+y) (maximum (ys++map(x+)ys))) 
-- by induction, (maximum (ys++map(x+)ys)) == max (maximum ys) (x+maximum ys)) 
         == max y (max (x+y) 
             (max (maximum ys) (x+maximum ys))) 
-- by commutativity of max (ie max a (max b c) == max b (max a c)) 
         == max y (max (maximum ys) 
             (max (x+y) (x+maximum ys))) 
-- by associativity of max (is max a (max b c) == max (max a b) c) 
         == max (max y (maximum ys)) 
             (max (x+y) (x+maximum ys))) 
         -- by definition of max, max (x+y) (x+z) == x+(max y z) 
         == max (max y (maximum ys)) 
             (x + max y (maximum ys))) 
         -- by definition of foldr1 and maximum 
         == max (maximum (y:ys)) (x + maximum (y:ys)) 

---

을 가정, 여기에 몇 가지 더.

"정의에 의한"단계 중 일부를 볼 수 있습니다. 함수가 작성된 방법을 보면 알 수 있습니다. 예를 들어 maximum = foldr1 max 및 foldr1 f (x:xs) = f x $ foldr1 f xs은 비어 있지 않은 경우 xs입니다. 다른 것들의 정의는 덜 명확합니다 - max y zmax의 정의는 표시되지 않습니다. 그러나 유도에 의해 그 숫자는 max (x+y)(x+z) == x+max y z 일 수 있습니다. 여기서는 max 0 y == y의 정의부터 시작하여 max을 해결하는 방법을 x이라고합니다. (마찬가지로 음수 인 경우 x과 y을 비슷한 방식으로 처리해야합니다.)

예를 들어 자연수는 0이고 자연수의 후속어입니다. 여기서 우리는 정의 된 비교가없는 것을 볼 수 있습니다. 우리가 아직 나체의 비교가 없기 때문에,

data Nat = Z | S Nat -- zero and any successor of a natural number 
(+) :: Nat -> Nat -> Nat -- addition is... 
Z + x = x -- adding zero is neutral 
(S x) + y = S (x + y) -- recursive definition of (1+x)+y = 1+(x+y) 
-- here unwittingly we introduced associativity of addition: 
-- (x+y)+z=x+(y+z) 
-- so, let's see the simplest case: 
-- x == Z 
-- (Z+y)+z == -- by definition, Z+y=y -- see the first line of (+) 
--   == y+z 
--   == Z+(y+z) -- by definition, Z+(y+z)=(y+z) 
-- 
-- ok, now try x == S m 
-- (S m + y) + z == -- by definition, (S m)+y=S(m+y) -- see the second line of(+) 
--    == S (m+y) + z 
--    == S ((m+y)+z) -- see the second line of (+) 
--         - S (m+y) + z = S ((m+y)+z) 
--    == S (m+(y+z)) -- by induction, the simpler 
--         case of (m+y)+z=m+(y+z) 
--         is known to be true 
--    == (S m)+(y+z) -- by definition, see second line of (+) 
-- proven 

그런 다음 특히 max을 정의해야합니다 : 그래서, 추가의 특성, 빼기, 최대, 등등, 정의 기능의에서 줄기 방법.

max :: Nat -> Nat -> Nat 
max Z y = y -- we know Z is not the max 
max x Z = x -- and the other way around, too 
-- this inadvertently introduced commutativity of max already 

max (S x) (S y) = S (max x y) -- this inadvertently introduces the law 
-- that max (x+y) (x+z) == x + (max y z) 

우리는 후자를 증명하고 싶다고 가정합니다. 지금 그래서 x == S m

max ((S m) + y) ((S m)+z) == -- by definition of (+) 
       == max (S(m+y)) (S(m+z)) 
       -- by definition of max 
       == S (max (m+y) (m+z)) 
       -- by induction 
       == S (m+(max y z)) 
       -- by definition of (+) 
       == (S m)+(max y z) 

가정, x == Z

max (Z+y) (Z+z) == -- by definition of (+) 
       == max y z 
       == Z + (max y z) -- by definition of (+) 

확인 가정, 당신이 볼,에 대한 증거를 사용하기 위해, 정의를 알고 간단한 경우를 증명하는 것이 중요하고 중요 중요하다 약간 더 복잡한 경우에는 더 간단한 경우.

Answer 2

스케치 :

maximum (xs ++ map (x+) xs) 
foldr1 max (xs ++ map (x+) xs) 
foldr max (foldr1 max xs) (map (x+) xs) 
foldr max (maximum xs) (map (x+) xs) 
max (maximum xs) (foldr1 max (map (x+) xs)) 
max (maximum xs) (x + foldr1 max xs) 
max (maximum xs) (x + maximum xs) 

사용

가 유도에 의해 수행 lemmata의

0. xs, ys are nonempty 
1. f is commutative and associative 
A. foldr1 f (xs ++ ys) == foldr f (foldr1 f xs) ys 
B. foldr f s xs = f s (foldr1 f xs) 
C. foldr1 f (map g xs) = g (foldr1 f xs) 
    if f (g x) (g y) == g (f x y) 

교정쇄를 (약한 가정이있을 수 있습니다, 나는 일을 어떻게 포착). 첫째, 우리의 정의를 기억합시다 : A의 다음

foldr k z [] = z 
foldr k z (x:xs) = k x (foldr k z xs) 

foldr1 k [z] = z 
foldr1 k (x:xs) = k x (foldr1 k xs) 

map k [] = [] 
map k (x:xs) = k x : map k xs 

을 :

등

To show: foldr1 f (xs ++ ys) == foldr f (foldr1 f xs) ys 
Induction on xs. 
Base case: xs = [x] 
    foldr1 f ([x] ++ ys) == f x (foldr1 f ys) 
    Induction on ys: ys = [y] 
     == f x (foldr f [y]) = f x y = f y x 
     == foldr f x [y] = foldr f (foldr1 f [x]) [y] 
    Step. ys = (y:yy) 
     == f x (foldr1 f (y:yy)) 
     == f x (f y (foldr1 f yy)) -> associativity and commutativity 
     == f y (f x (foldr1 f yy)) -> induction assumption 
     == f y (foldr f x yy) 
     == foldr f (foldr1 f [x]) (y:yy) 
Step: xs = (x:xx) 
    foldr1 f (x:xx ++ ys) = f x (foldr1 f (xx ++ yy)) 
     == f x (fold f (foldr1 f xx) yy) 
     == fold f (foldr1 f xx) (x:yy) 
    Induction on ys. 
    Base case ys = [y] 
     == f x (f y (foldr1 f xx)) == f y (f x (foldr1 f (x:xx)) 
     == fold f (foldr1 f xs) [y] 
    Step. ys = (y:yy) 
     == f x (f y (fold f (foldr1 f xx) yy) -> associativity, commutativity 
     == f y (f x (fold f (foldr1 f xx) yy) -> induction assumption 
     == f y (fold f (foldr1 f (x:xx) yy) 
     == fold f (foldr1 f xs) ys 

그리고, 그것을 자신을 시도합니다.