Доказать, что рекурсивные функции терминированы для всех целых чисел

@Kvintero · Регистрация: 21.04.2014

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

Всем привет.
Снова нужна ваша помощь.
По заданию, нужно доказать, что рекурсивные функции терминированы для всех целых чисел.

Haskell
1
2
3
4
5
barfoo :: Integer -> Integer
barfoo x
| x >= 123 = x - 666
| x <= 1, x >= 0 = 42
| otherwise = barfoo (x+1) * barfoo (x*x) * 3

Вот что я наваял. Очень надеюсь на конструктивную критику

g(x) :: Z*Z->Z
g(x) | x - 666, x>= 123
| 42 , x=0, x=1
| g(x+1)*g(x*x)*3, x<123, x/=0, x/=1

нужно показать, что рекурсивные функции завершаются (терминируются)

Можно предположить, что значение x будет расти до значения 123.

g(x)<g(x+1) | x<123, x/=0, x/=1
g(x)<g(x*x) | x<123, x/=0, x/=1

возьмем функцию спуска (descent function) g(x)= x - 1.

Очевидно, что

x-1<x

или

x-1<x²

Вывод: обе функции терминируются

@Araneo · 10.05.2014, 19:06

1. Если x >= 123 или x <= 1 или x >= 0 = 42 то g(x) терминируеться.
2. иначе g(x) выражаеться через g(x+1) и g(x^2) нетрудно видеть что не более чем за 123 - x шагов g(х) будет выражена через терминированые функции.
Следовательно для любого x g(x) терминирована.

както-так... но это очень грубо.

@Kvintero · 10.05.2014, 19:46 **[ТС]**

123 шага - это только для натуральных чисел или для всех реальных? с x^2 может быть еще меньше

Еще забыл добавить, что терминирование этих рекурсий нужно доказать при помощи так называемой функции спуска. Я мог это неправильно перевести. Есть такой термин?

@Araneo · 10.05.2014, 23:33

Глубина рекурсии для x от 1 до 123 равна 123 - x для всех реальных(x округляем вниз).
для всех отрицательных x глубина рекурсии равна abs (x) (x округляем вниз).
Я что называеться это просто вижу. Со строгими доказательствами у меня (буду честен )не очень. В данном случаи нормальный человек (а не тот что перед вами

) ) допелил бы рекурсивное доказательство... как доказывать используя спуск пока не вижу тут наверно Сatstail может помочь... я всё-же пока только студент...
---
Сatstail, я что так злобно нарушаю правила русского языка, и мои посты обязательно нужно поправлять

( ?

Добавлено через 30 минут
А нет, для отрицательных мои рассуждения ошибочны... утром честно сяду с бумажкой... и ручкой расчитывать.

@Kvintero · 11.05.2014, 11:30 **[ТС]**

Я немного не понимаю принцип доказательства. Тем более при помощи функции спуска (нем. Abstiegsfunktion)

@Catstail · 11.05.2014, 12:10

Добавлено через 1 секунду
Kvintero, приведенный Вами код некорректен. Вместо запятой должно быть "&&" (и) или "||" (или). Поведение функций получается совершенно разным:

Haskell
1
2
3
4
5
6
7
8
9
10
11
12
barfoo :: Integer -> Integer
barfoo x | x >= 123 = x - 666
         | x <= 1 || x >= 0 = 42
         | otherwise = barfoo (x+1) * barfoo (x*x) * 3
 
 
Main> barfoo 2
42
Main> barfoo 100
42
Main> barfoo 1000
334

А с && все не так:

Haskell
1
2
3
4
5
6
7
8
barfoo :: Integer -> Integer
barfoo x | x >= 123 = x - 666
         | x <= 1 && x >= 0 = 42
         | otherwise = barfoo (x+1) * barfoo (x*x) * 3
 
Main> barfoo 1
42
Main> barfoo 2

Кликните здесь для просмотра всего текста

2123481053083346575622093794750191419450 8807706916888956977989469674945080446971 7727982020349253850026287266307081
1782890573029371074995785182761697017024 4004369874599477435078298889381278285342 5635178678688623995006540233472391
3414263856839313121214502123950796790561 0388170199296325350028334339883777892216 7348200031616026159657171465855975
....
0000000000000000000000000000000000000

@Kvintero · 11.05.2014, 12:54 **[ТС]**

В задании стоит как раз запятая. Это как-то влияет на терминирование функций?

@Catstail · 11.05.2014, 13:00

С запятой winhugs код не транслирует...

Добавлено через 2 минуты
А winGHCi транслирует. Поведение - как у "||".

@Kvintero · 11.05.2014, 19:00 **[ТС]**

Может быть нас пока на такие тонкости не натаскивают

Добавлено через 5 часов 57 минут
Так все-таки мое доказательство можно считать таковым или то что я написал чушь?

@Mysterious Light · 11.05.2014, 21:32

И я всуну пятак, хотя признаюсь, что совсем не знаю матчасть.

Я нахожу решение, о котором говорит ТС, необоснованным, потому что по его схеме можно доказать терминируемость очевидно нетерминируемой функции

Haskell
1
2
3
f x
  | -10 < x && x < 10 = f(x+1) * f(x-1)
  | otherwise = 0

Я не знаю, что такое функция спуска и буду рад, если кто-то объяснит.

@Kvintero · 12.05.2014, 20:30 **[ТС]**

Возможно вы правы, но как же сделать более обоснованей? Я же вроде бы показал рост значения x. На значении 123 рекурсия будет остановлена. Или не так?

Добавлено через 21 час 17 минут
Завтра сдаю свое творчество, посмотрим, что напишут.
Результаты скину сюда

@Kvintero · 14.05.2014, 18:53 **[ТС]**

Может у кого-то есть идеи?
Мой вариант некоректен. Нужно было показать, что, так называемая функция спада становиться меньше.

Новые блоги и статьи Все статьи Все блоги /
Owen Logic: О недопустимости использования связки «аналоговый ПИД» + RegKZR ФедосеевПавел 06.01.2026 Owen Logic: О недопустимости использования связки «аналоговый ПИД» + RegKZR ВВЕДЕНИЕ Введу сокращения: аналоговый ПИД — ПИД регулятор с управляющим выходом в виде числа в диапазоне от 0% до. . .	Модель микоризы: классовый агентный подход 2 anaschu 06.01.2026 репозиторий https:/ / github. com/ shumilovas/ fungi ветка по-частям. коммит Create переделка под биомассу. txt вход sc, но sm считается внутри мицелия. кстати, обьем тоже должен там считаться. . . .	Расчёт токов в цепи постоянного тока igorrr37 05.01.2026 / * Дана цепь постоянного тока с сопротивлениями и напряжениями. Надо найти токи в ветвях. Программа составляет систему уравнений по 1 и 2 законам Кирхгофа и решает её. Последовательность действий:. . .	Новый CodeBlocs. Версия 25.03 palva 04.01.2026 Оказывается, недавно вышла новая версия CodeBlocks за номером 25. 03. Когда-то давно я возился с только что вышедшей тогда версией 20. 03. С тех пор я давно снёс всё с компьютера и забыл. Теперь. . .
Модель микоризы: классовый агентный подход anaschu 02.01.2026 Раньше это было два гриба и бактерия. Теперь три гриба, растение. И на уровне агентов добавится между грибами или бактериями взаимодействий. До того я пробовал подход через многомерные массивы,. . .	Советы по крайней бережливости. Внимание, это ОЧЕНЬ длинный пост. Programma_Boinc 28.12.2025 Советы по крайней бережливости. Внимание, это ОЧЕНЬ длинный пост. Налог на собак: https:/ / ********/ gallery/ V06K53e Финансовый отчет в Excel: https:/ / ********/ gallery/ bKBkQFf Пост отсюда. . .	Кто-нибудь знает, где можно бесплатно получить настольный компьютер или ноутбук? США. Programma_Boinc 26.12.2025 Нашел на реддите интересную статью под названием Anyone know where to get a free Desktop or Laptop? Ниже её машинный перевод. После долгих разбирательств я наконец-то вернула себе. . .	Thinkpad X220 Tablet — это лучший бюджетный ноутбук для учёбы, точка. Programma_Boinc 23.12.2025 Рецензия / Мнение/ Перевод Нашел на реддите интересную статью под названием The Thinkpad X220 Tablet is the best budget school laptop period . Ниже её машинный перевод. Thinkpad X220 Tablet —. . .

@Araneo 650 / 260 / 16 Регистрация: 02.03.2014 Сообщений: 587
	10.05.2014, 19:06
	1. Если x >= 123 или x <= 1 или x >= 0 = 42 то g(x) терминируеться. 2. иначе g(x) выражаеться через g(x+1) и g(x^2) нетрудно видеть что не более чем за 123 - x шагов g(х) будет выражена через терминированые функции. Следовательно для любого x g(x) терминирована. както-так... но это очень грубо. 0

@Kvintero 1 / 1 / 0 Регистрация: 21.04.2014 Сообщений: 65
	10.05.2014, 19:46 [ТС]
	123 шага - это только для натуральных чисел или для всех реальных? с x^2 может быть еще меньше Еще забыл добавить, что терминирование этих рекурсий нужно доказать при помощи так называемой функции спуска. Я мог это неправильно перевести. Есть такой термин? 0

@Araneo 650 / 260 / 16 Регистрация: 02.03.2014 Сообщений: 587
	10.05.2014, 23:33
	Глубина рекурсии для x от 1 до 123 равна 123 - x для всех реальных(x округляем вниз). для всех отрицательных x глубина рекурсии равна abs (x) (x округляем вниз). Я что называеться это просто вижу. Со строгими доказательствами у меня (буду честен )не очень. В данном случаи нормальный человек (а не тот что перед вами ) ) допелил бы рекурсивное доказательство... как доказывать используя спуск пока не вижу тут наверно Сatstail может помочь... я всё-же пока только студент... --- Сatstail, я что так злобно нарушаю правила русского языка, и мои посты обязательно нужно поправлять ( ? Добавлено через 30 минут А нет, для отрицательных мои рассуждения ошибочны... утром честно сяду с бумажкой... и ручкой расчитывать. 0

@Kvintero 1 / 1 / 0 Регистрация: 21.04.2014 Сообщений: 65
	11.05.2014, 11:30 [ТС]
	Я немного не понимаю принцип доказательства. Тем более при помощи функции спуска (нем. Abstiegsfunktion) 0

@Kvintero 1 / 1 / 0 Регистрация: 21.04.2014 Сообщений: 65
	11.05.2014, 12:54 [ТС]
	В задании стоит как раз запятая. Это как-то влияет на терминирование функций? 0

@Catstail Супер-модератор 38164 / 21099 / 4306 Регистрация: 12.02.2012 Сообщений: 34,687 Записей в блоге: 14
	11.05.2014, 13:00
	С запятой winhugs код не транслирует... Добавлено через 2 минуты А winGHCi транслирует. Поведение - как у "\|\|". 0

@Kvintero 1 / 1 / 0 Регистрация: 21.04.2014 Сообщений: 65
	11.05.2014, 19:00 [ТС]
	Может быть нас пока на такие тонкости не натаскивают Добавлено через 5 часов 57 минут Так все-таки мое доказательство можно считать таковым или то что я написал чушь? 0

@Kvintero 1 / 1 / 0 Регистрация: 21.04.2014 Сообщений: 65
	12.05.2014, 20:30 [ТС]
	Возможно вы правы, но как же сделать более обоснованей? Я же вроде бы показал рост значения x. На значении 123 рекурсия будет остановлена. Или не так? Добавлено через 21 час 17 минут Завтра сдаю свое творчество, посмотрим, что напишут. Результаты скину сюда 1

@Kvintero 1 / 1 / 0 Регистрация: 21.04.2014 Сообщений: 65
	14.05.2014, 18:53 [ТС]
	Может у кого-то есть идеи? Мой вариант некоректен. Нужно было показать, что, так называемая функция спада становиться меньше. 0