Доказательство закона слияния для раскрытия

Question

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

unfoldL p f g . h = unfoldL p' f' g'

если

p . h = p'
f . h = f'
g . h = h . g'

Функция unfoldLРазвернуть для списков, определяется следующим образом:

unfoldL :: (b -> Bool) -> (b -> a) -> (b -> b) -> b -> List a
unfoldL p f g b = if p b then Nil else Cons (f b) (unfoldL p f g (g b))

Вот моя текущая попытка доказательства:

(unfoldL p f g . h) b
=   { composition }
unfoldL p f g (h b)
=   { unfoldL }
if p (h b) then Nil else Cons (f (h b)) (unfoldL p f g (g (h b)))
=   { composition }
if (p . h) b then Nil else Cons ((f . h) b) (unfoldL p f g ((g . h) b))
=   { assumptions }
if p' b then Nil else Cons (f' b) (unfoldL p f g ((h . g') b))
=   { composition }
if p' b then Nil else Cons (f' b) ((unfoldL p f g . h) (g' b))
=   { ??? }
if p' b then Nil else Cons (f' b) (unfoldL p' f' g' (g' b))
=   { unFoldL }
unFoldL p' f' g'

Я не уверен, как оправдать шаг, отмеченный ???, Я должен, вероятно, использовать какую-то индукцию при применении функции на b? Смежный вопрос: каковы хорошие ресурсы, которые объясняют и мотивируют различные методы индукции, такие как структурная индукция?

Answer 1

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

Это хорошая интуиция, что вы ищете какую-то индукцию, потому что то, что вам нужно, очень похоже на то, что вы пытаетесь доказать. Но вам на самом деле нужна совместная скидка. Это потому что unfoldL может создавать бесконечные списки. В системах формального типа очень редко можно доказать, что две бесконечные структуры "равны" - формальное равенство слишком сильно, чтобы доказать большинство результатов. Вместо этого мы доказываем сходство, которое в неформальных обстоятельствах также может быть равенством.

Схожесть теоретически сложна, и я не буду вдаваться в подробности (частично потому, что не до конца понимаю основы), но работать с ней на практике не так уж сложно. По сути, чтобы доказать, что два списка не похожи друг на друга, нужно доказать, что оба Nil или что они оба Cons с одной и той же головой и их хвосты не похожи друг на друга, и вы можете использовать коиндуктивную гипотезу для доказательства двойственности хвостов (но не в других местах).

Таким образом, для вас мы докажем, что для всех b (потому что нам нужно использовать коиндуктивную гипотезу для разных b s):

(unfoldL p f g . h) b ~~ unfoldL p' f' g' b

Пока у нас есть

(unfoldL p f g . h) b
= { your reasoning }
if p' b then Nil else Cons (f' b) ((unfoldL p f g . h) (g' b))

Анализируя по случаям на p' b, если p' b верно тогда

if p' b then Nil else Cons (f' b) ((unfoldL p f g . h) (g' b))
= { p' b is True }
Nil
~~ { reflexivity }
Nil
= { p' b is True }
if p' b then Nil else Cons (f' b) (unfoldL p' f' g' (g' b))
= { unfoldL }
unfoldL p' f' g'

; если p' b тогда ложно

if p' b then Nil else Cons (f' b) ((unfoldL p f g . h) (g' b))
= { p' b is False }
Cons (f' b) ((unfoldL p f g . h) (g' b))
*** ~~ { bisimilarity Cons rule, coinductive hypothesis } ***
Cons (f' b) (unfoldL p' f' g' (g' b))
= { p' b is False }
if p' b then Nil else Cons (f' b) (unfoldL p' f' g' (g' b))
= { unfoldL }

Линия отмечена *** является ключевым. Во-первых, обратите внимание, что это ~~ вместо =, Кроме того, нам было разрешено использовать коиндуктивную гипотезу только под Cons конструктор Если бы нам было разрешено использовать его где-либо еще, то мы могли бы доказать, что любые два списка похожи друг на друга.

Answer 2

После некоторого поиска в Google я нашел статью того же Джереми Гиббона (и Грэма Хаттона), в которой представлены проверочные методы для основных программ; статья содержит раздел о бисимуляции и коиндукции, методе доказательства, используемой @luqui в принятом ответе. Раздел 6 имеет доказательство закона слияния с использованием универсального свойства развернуть. Для полноты я скопировал доказательство ниже.

---

Универсальное свойство unfoldL:

h = unfoldL p f g
<=>
∀ b . h b = if p b then Nil else Cons (f b) (h (g b))

Доказательство закона слияния:

unfoldL p f g . h = unfoldL p' f' g'
<=> { universal property }
∀ b . (unfoldL p f g . h) b = if p' b then Nil else Cons (f' b) ((unfoldL p f g . h) (g' b))
<=> { composition }
∀ b . unfoldL p f g (h b) = if p' b then Nil else Cons (f' b) (unfoldL p f g (h (g' b)))
<=> { unfoldL }
∀ b . if p (h b) then Nil else Cons (p (h b)) (unfoldL p f g (g (h b))) = if p' b then Nil else Cons (f' b) (unfoldL p f g (h (g' b)))
<=> { composition }
∀ b . if (p . h) b then Nil else Cons (p . h) b (unfoldL p f g ((g . h) b)) = if p' b then Nil else Cons (f' b) (unfoldL p f g ((h . g') b))
<=  { assumptions }
(p . h = p') ^ (f . h = f') ^ (g . h = h . g')