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

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

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

Здравствуйте! Помогите пожалуйста доказать, используя аксиому структурной индукции справедливость: 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
1
(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 = ( : )

Новые блоги и статьи Все статьи Все блоги /
SDL3 для Web (WebAssembly): Реализация движения на Box2D v3 - трение и коллизии с повёрнутыми стенами 8Observer8 20.02.2026 Содержание блога Box2D позволяет легко создать главного героя, который не проходит сквозь стены и перемещается с заданным трением о препятствия, которые можно располагать под углом, как верхнее. . .	Конвертировать закладки radiotray-ng в m3u-плейлист damix 19.02.2026 Это можно сделать скриптом для PowerShell. Использование . \СonvertRadiotrayToM3U. ps1 <path_to_bookmarks. json> Рядом с файлом bookmarks. json появится файл bookmarks. m3u с результатом. # Check if. . .	Семь CDC на одном интерфейсе: 5 U[S]ARTов, 1 CAN и 1 SSI Eddy_Em 18.02.2026 Постепенно допиливаю свою "многоинтерфейсную плату". Выглядит вот так: https:/ / www. cyberforum. ru/ blog_attachment. php?attachmentid=11617&stc=1&d=1771445347 Основана на STM32F303RBT6. На борту пять. . .	Камера Toupcam IUA500KMA Eddy_Em 12.02.2026 Т. к. у всяких "хикроботов" слишком уж мелкий пиксель, для подсмотра в ESPriF они вообще плохо годятся: уже 14 величину можно рассмотреть еле-еле лишь на экспозициях под 3 секунды (а то и больше),. . .
И ясному Солнцу zbw 12.02.2026 И ясному Солнцу, и светлой Луне. В мире покоя нет и люди не могут жить в тишине. А жить им немного лет.	«Знание-Сила» zbw 12.02.2026 «Знание-Сила» «Время-Деньги» «Деньги -Пуля»	SDL3 для Web (WebAssembly): Подключение Box2D v3, физика и отрисовка коллайдеров 8Observer8 12.02.2026 Содержание блога Box2D - это библиотека для 2D физики для анимаций и игр. С её помощью можно определять были ли коллизии между конкретными объектами и вызывать обработчики событий столкновения. . . .	SDL3 для Web (WebAssembly): Загрузка PNG с прозрачным фоном с помощью SDL_LoadPNG (без SDL3_image) 8Observer8 11.02.2026 Содержание блога Библиотека SDL3 содержит встроенные инструменты для базовой работы с изображениями - без использования библиотеки SDL3_image. Пошагово создадим проект для загрузки изображения. . .

@Weronika 0 / 0 / 1 Регистрация: 01.03.2016 Сообщений: 64

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

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

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

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

Решение