История изменений
Исправление AndreyKl, (текущая версия) :
Функция гарантированно завершается. Сможет Coq её скомпилировать?
https://en.wikipedia.org/wiki/Collatz_conjecture
As proven by Riho Terras, almost every positive integer has a finite stopping time
almost every
alysnix
Не, народ. Это не подходит. Если вы не имеете доказательства завершения, то Кок его конечно же волшебным образом найти не сможет, это не серьёзно.
Приведённая выше функция на коке легко формулируется, но придётся откючить проверку завершаемости.
Исходная версия AndreyKl, :
Функция гарантированно завершается. Сможет Coq её скомпилировать?
https://en.wikipedia.org/wiki/Collatz_conjecture
As proven by Riho Terras, almost every positive integer has a finite stopping time
almost every
alysnix
Не, народ. Это не подходит. Если вы не имеете доказательства завершения, то Кок его конечно же волшебным образом найти не сможет, это не серьёзно.