Трудно понять, как преобразовать складку в декартово произведение - PullRequest
Новая
       55

Трудно понять, как преобразовать складку в декартово произведение

0 голосов
/ 21 мая 2018

Я следую О функции декартового произведения Баррона и Стрейчи , чтобы понять комбинацию функции высокого порядка.

Я получил важное преобразование, и я думаю, что это нелегко понятьпросто: 

h [] xss = []
h (x : xs) xss =
 foldr f (h xs xss) xss where 
    f xs ys = (x: xs) : ys

, чтобы равняться этому: 

h'' xs xss = 
foldr g [] xs where
    g x zss = foldr f zss xss where 
        f xs ys = (x : xs) : ys

Даже у меня есть эти помощники: 

foldr :: (a -> b -> b) -> b -> [a] -> b
foldr f z [] = z
foldr f z (a:as) = f a (foldr f z as) 

-- change the name
h' :: (a -> b -> b) -> b -> [a] -> b
h' f z [] = z
h' f z (a:as) = f a (h' f z as)

Итак, мой вопрос: легко ли объяснитьпреобразование

Ответы [ 2 ]

0 голосов
/ 21 мая 2018

Начнем с создания внутренней функции без второго аргумента xss, которая выполняет только стандартную рекурсию списка: 

h []     xss = []
h (x:xs) xss = foldr f (h xs xss) xss
  where 
    f xs ys = (x:xs) : ys

  -->

h xs xss = h' xs
  where
    h' []     = []
    h' (x:xs) = foldr f (h' xs) xss
      where
        f xs ys = (x:xs) : ys

Затем посмотрим, как мы абстрагируем шаблон рекурсии в h' с помощью другого помощника.функция, которая действует на x и результат рекурсивного вызова только h' xs: 

h xs xss = h' xs
  where
    h' []     = []
    h' (x:xs) = g x (h' xs)
    g x zss = foldr f zss xss
      where 
        f xs ys = (x:xs) : ys

, который является просто той вспомогательной функцией, которую мы передали бы foldr, если бы мы не хотели явно выписыватьсписок рекурсии в h': 

h xs xss = foldr g [] xs
  where
    g x zss = foldr f zss xss
      where 
        f xs ys = (x:xs) : ys
0 голосов
/ 21 мая 2018

По сути, это сводится к тому, что h является рекурсивной функцией в xs и что foldr обобщает рекурсию в списках.Обратите внимание, как h вызывает себя на хвосте xs, так же, как foldr вызывает себя на хвосте as.

По индукции на ws докажите, что h ws xss = h'' ws xss.Рассуждая по индукции, нужно рассмотреть два случая.

Базовый случай , ws = []

h [] xss = []  -- by definition of h

h'' [] xss
= foldr g [] xss  -- by definition of h''
= []              -- by definition of foldr

Шаг индукции , ws = x : xs, предполагая h xs xss = h'' xs xss (индукционная гипотеза) 

h (x : xs) xss
= foldr f (h xs xss) xss    -- by definition of h (N.B. f depends on x)
= foldr f (h'' xs xss) xss  -- by induction hypothesis
= g x (h'' xs xss)          -- by definition of g (N.B. g depends on xss)
= g x (foldr g [] xs)       -- by definition of h''
= foldr g [] (x : xs)       -- by definition of foldr
= h'' (x : xs) xss          -- by definition of h''
...