Доказать, используя аксиому структурной индукции справедливость

@Weronika · Регистрация: 01.03.2016

Author24 — интернет-сервис помощи студентам

Здравствуйте! Помогите пожалуйста доказать, используя аксиому структурной индукции справедливость: minimum (map (+1) xs) = minimum xs + 1

@Catstail · 25.02.2018, 18:04

Попробуем так:

1) Возьмем за определение функции mininmum следующее:

Haskell

1 2	minimum [x] = x -- <1> minimum (x:xs) = min x (minimum xs) -- <2>

2) Рассмотрим выражение

Haskell

1	minimum (map (+1) [x])

, где [x] - произвольный одноэлементный список. Очевидно, что

Haskell

1	map (+1) [x] == [x+1]

. Таким образом, имеем:

Haskell

1	minimum (map (+1) [x]) == minimum [x+1] == x+1 -- (в соотв. с уравнением <1>)

С другой стороны:

Haskell

1	minimum [x] + 1 == x+1 -- т.к. minimum [x] == x в соотв. с уравнением <1>

Получаем, что для произвольного одноэлементного списка x имеет место равенство:

Haskell

1 2	minimum (map (+1) xs) == minimum xs + 1

Это - база индукции.

3) Теперь предположим, что это равенство имеет место для списка xs, и докажем, что отсюда следует справедливость для (x:xs) при произвольном х.

Haskell

1	minimum (map (+1) (x:xs)) == minimum ((x+1):(map (+1) xs)) -- просто применили (+1) к голове и хвосту

Теперь воспользуемся определением функции minimum (уравнение <2>). Получим:

Haskell

1	minimum (x+1):(map (+1) xs)) == min (x+1) $ minimum (map (+1) xs)

По предположению индукции

Haskell

1	minimum (map (+1) xs) == minimum xs + 1

И выражение

Haskell

1	min (x+1) $ minimum (map (+1) xs)

оказывается равным

Haskell

1	min (x+1) (minimum xs + 1)

Далее, возможно два случая:

a)

Haskell

1	minimum (x:xs) == x

. В этом случае

Haskell

1	x <= minimum xs

и

Haskell

1	min (x+1) (minimum xs + 1) == x+1 == minimum (x:xs) + 1

б)

Haskell

1	minimum (x:xs) <= x

. В этом случае

Haskell

1	min (x+1) (minimum xs + 1) == (minimum xs + 1) = minimum (x:xs) + 1

В обоих случаях из предположения истинности равенства для списка xs, следует истинность для списка (x:xs).
Это завершает доказательство.

@Weronika · 25.02.2018, 18:17 **[ТС]**

Спасибо большое

@_Ivana · 28.02.2018, 01:50

С этими индукциями есть один тонкий, но весьма суровый на поверку момент

Пирс в ТАПЛе его элегантно обходит за счет строгости семантики, хотя у него там 90% книги это такие вот индуктивные доказательства.

Собственно, о чем я. В известном курсе Дениса Москвина на степике тоже было пару задач на "доказательство", с приведением авторского эталонного. Пользуясь этой нехитрой технологией, я доказал, что в Хаскеле любой список имеет конечную длину

Ну ведь очевидно - пустой список нулевой длины = база индукции, далее из предположения конечной длины списка эль со всей пролетарской очевидностью следует конечность длины списка х:эль

Но ведь вы понимаете, что что-то здесь нечисто?

Вот то то и оно то. Поэтому такие наивные индукции в Хаскеле (да и вообще в теории) являются профанацией. А честно это решается через достаточно суровую теорию, которую я так и не нашел время осилить

@Curry · 28.02.2018, 08:24

Сообщение от _Ivana

я доказал, что в Хаскеле любой список имеет конечную длину

С помощью индукции доказывается истинность бесконечной последовательности утверждений. Вы доказываете что для любого n может существовать список длины n. И так для любого n до бесконечности. А ограничение про конечную длину никак в доказательстве не обыгрывается. Вот если бы вы взялись доказывать что всегда существует такое N дальше которого список не нарастить ...

@Mysterious Light · 28.02.2018, 13:43

Сообщение от KolodeznyDiver

Вы доказываете что для любого n может существовать список длины n. И так для любого n до бесконечности.

Ну почему же? Исходное доказуемое утвеждение: любой список имеет конечную длину. То есть для любого списка найдётся такое (конечное) число, что длина списка равна этому числу.

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

Сообщение от _Ivana

А честно это решается через достаточно суровую теорию, которую я так и не нашел время осилить

Я тоже. Какую литературу используешь?
Как-то открыл Bart Jacobs, Jan Butten A tutorial on (Co)Algebras and (Co)Induction (кажется, по рекомендации Joker_vD), но отвлёкся на более насущие задачи. Увы.

Добавлено через 2 минуты
Так, вижу ты уже этим вопрос задавался.
Хаосит предложил Фиоре "Принцип коиндукции для корекурсивных типов, основанный на бисимуляции".

@Curry · 28.02.2018, 14:49

Сообщение от Mysterious Light

Ну почему же? Исходное доказуемое утвеждение: любой список имеет конечную длину. То есть для любого списка найдётся такое (конечное) число, что длина списка равна этому числу.

Зависит от формулировки, что же такое список.

Добавлено через 39 минут
Исходное утвеждение:

Сообщение от _Ivana

в Хаскеле любой список имеет конечную длину

Для списков Haskell это не так.

XRuZzz · 28.06.2018, 07:39

Плохо даётся метод структурной индукции(как и разборы доказательств), решил попробовать, не знаю правильно или нет:
Доказать:

Haskell

1	minimum (map (+1) xs) = minimum xs + 1 -- (1)

Определения:

Haskell

1 2	minimum [x] = x -- (2) minimum (x:xs) = min x (minimum xs) -- (3)

База:

Haskell

1 2	minimum (map (+1) [x]) = minimum [x] + 1 -- (4) x + 1 == x + 1

(*)
Леввая часть:

Haskell

1 2	minimum (map (+1) (x:xs)) = minimum ((x+1): map (+1) xs) = min (x + 1) (minimum (map (+1) xs)) -- (5)

Правая часть:

Haskell

1 2	minimum (x:xs) + 1 = (min x (minimum xs)) + 1 -- (6)

Ситуации
I Когда левая часть

Haskell

1	min (x + 1) (minimum (map (+1) xs))

вернёт первый аргумент:

Haskell

(x + 1)

То есть минимумом окажется первый элемент списка.
(Далее скользкий момент)
Докажем, что если в правой части минимумом будет первый элемент списка x, то и в левой части минимумом будет (x + 1), и что другие ситуации невозможны.
Отнимем от каждого элемента списка в левой части 1 и получим:
min x (minimum xs)
Это означает, что это выражение вернёт, как и в правой части x.
Значит если

Haskell

1	min x (minimum xs)) + 1 = x + 1

то и

Haskell

1	min (x + 1) (minimum (map (+1) xs)) = x + 1

верно и обратное утверждение.

То есть для ситуации когда минимумом окажется первый элемент списка утверждение (1) доказано.

II Когда правая и левая части вернут второй аргумент функции min:
Тогда нужно доказать, что

Haskell

1	minimum (map (+1) xs) = minimum xs + 1

для хвоста списка.
Таким образом повторяем доказательтство для каждого элемента списка, начиная с (*)
до тех пор пока список не превратиться в [x], для которого уже равенство доказано.
Конец.

То есть выражение (1) верно, потому что оно обращается в верное на каждом шаге рекурсии.

@Mysterious Light · 28.06.2018, 13:10

Если рассматриваются конечные структуры (т.е. инициальные коалгебры в категории типов), то в (5) уже можно пользоваться (1) для хвоста xs исходного списка x:xs.

Посмотрите диаграммы, чтобы схематично понять, что получилось бы в случае прямой подстановки.
На первой диаграмме левый квадрат - определение map, правый нижний - определение minimum, правый верхний является свойством прямого произведения.
На второй диаграмме левый квадрат - определение minimum, а правый квадрат является деформированным квадратом
$https://www.cyberforum.ru/cgi-bin/latex.cgi?\textrm{min}\circ i^2 = i\circ \textrm{min}$
то есть

Haskell

1	min (x+1) (y+1) = (min x y) + 1

с расщеплением прямого произведения на компоненты, аналогичным правому верхнему квадрату первой диаграммы.

Как видно, правая грань $https://www.cyberforum.ru/cgi-bin/latex.cgi?\textrm{min}\circ [i\times id]$ одинакова, следовательно, по универсальному свойству нижние грани должны совпадать, что является содержанием доказываемого утверждения.

Условные обозначения:
i = ( 1 + )
m = minimum
box = ( : )

@Weronika 0 / 0 / 1 Регистрация: 01.03.2016 Сообщений: 64
		1
	Доказать, используя аксиому структурной индукции справедливость 25.02.2018, 16:13. Показов 1942. Ответов 8 Метки нет (Все метки) Здравствуйте! Помогите пожалуйста доказать, используя аксиому структурной индукции справедливость: minimum (map (+1) xs) = minimum xs + 1 0

@Weronika 0 / 0 / 1 Регистрация: 01.03.2016 Сообщений: 64
	25.02.2018, 18:17 [ТС]	3
	Спасибо большое 0

@_Ivana 4817 / 2278 / 287 Регистрация: 01.03.2013 Сообщений: 5,947 Записей в блоге: 28
	28.02.2018, 01:50	4
	С этими индукциями есть один тонкий, но весьма суровый на поверку момент Пирс в ТАПЛе его элегантно обходит за счет строгости семантики, хотя у него там 90% книги это такие вот индуктивные доказательства. Собственно, о чем я. В известном курсе Дениса Москвина на степике тоже было пару задач на "доказательство", с приведением авторского эталонного. Пользуясь этой нехитрой технологией, я доказал, что в Хаскеле любой список имеет конечную длину Ну ведь очевидно - пустой список нулевой длины = база индукции, далее из предположения конечной длины списка эль со всей пролетарской очевидностью следует конечность длины списка х:эль Но ведь вы понимаете, что что-то здесь нечисто? Вот то то и оно то. Поэтому такие наивные индукции в Хаскеле (да и вообще в теории) являются профанацией. А честно это решается через достаточно суровую теорию, которую я так и не нашел время осилить 0

@Curry Модератор 5047 / 3276 / 526 Регистрация: 01.06.2013 Сообщений: 6,806 Записей в блоге: 9
	28.02.2018, 08:24	5
	Сообщение от _Ivana я доказал, что в Хаскеле любой список имеет конечную длину С помощью индукции доказывается истинность бесконечной последовательности утверждений. Вы доказываете что для любого n может существовать список длины n. И так для любого n до бесконечности. А ограничение про конечную длину никак в доказательстве не обыгрывается. Вот если бы вы взялись доказывать что всегда существует такое N дальше которого список не нарастить ... 0

@Mysterious Light $Эксперт по математике/физике$ 4300 / 2091 / 431 Регистрация: 19.07.2009 Сообщений: 3,162 Записей в блоге: 24
	28.02.2018, 13:43	6
	Сообщение от KolodeznyDiver Вы доказываете что для любого n может существовать список длины n. И так для любого n до бесконечности. Ну почему же? Исходное доказуемое утвеждение: любой список имеет конечную длину. То есть для любого списка найдётся такое (конечное) число, что длина списка равна этому числу. Как я это вижу, когда так, играючись, предлагаются некоторые доказательства, они рассматривают только конечные (индуктивные) рекурсивные типы. С бесконечными (коиндуктивными) такие доказательства (по крайней мере, в таких формулировках) не обязательно будут работать. Сообщение от _Ivana А честно это решается через достаточно суровую теорию, которую я так и не нашел время осилить Я тоже. Какую литературу используешь? Как-то открыл Bart Jacobs, Jan Butten A tutorial on (Co)Algebras and (Co)Induction (кажется, по рекомендации Joker_vD), но отвлёкся на более насущие задачи. Увы. Добавлено через 2 минуты Так, вижу ты уже этим вопрос задавался. Хаосит предложил Фиоре "Принцип коиндукции для корекурсивных типов, основанный на бисимуляции". 0

@Curry Модератор 5047 / 3276 / 526 Регистрация: 01.06.2013 Сообщений: 6,806 Записей в блоге: 9
	28.02.2018, 14:49	7
	Сообщение от Mysterious Light Ну почему же? Исходное доказуемое утвеждение: любой список имеет конечную длину. То есть для любого списка найдётся такое (конечное) число, что длина списка равна этому числу. Зависит от формулировки, что же такое список. Добавлено через 39 минут Исходное утвеждение: Сообщение от _Ivana в Хаскеле любой список имеет конечную длину Для списков Haskell это не так. 0

Доказать, используя аксиому структурной индукции справедливость

Решение