H
They played us for absolute fools
Size: a a a
2021 May 27
gо
shaking my smh head
TK
Ограничением глубины?
TK
Или какое-то время ждёт?
TK
Раз не тьюринг-полный, было бы даже интереснее, будь решена проблема остановки
H
Анализом на тотальность, вестимо
H
Как это обычно делают в ассистентах
p
Тьюринг полный язык не означает тьюринг-полный рантайм
p
Тьюринг полных рантаймов нет
p
Значит и тьюринг полнота не нужна
p
End.
а
Не, прикол в том что он разешает только структурную рекурсию, то есть при каждом рекурсивном вызове функция должна структурно уменьшать 1 из аргументов
а
уточню что в Coq натуральные числа определены как рекурсивный тип (раст синтаксис)
enum nat {
O,
S(nat),
}
первый вариант означает что число равно нулю, вторая означает что число равно 1 + число внутриа
Например есть функция факториала, здесь match n матчит аргумент с двумя вариантами
O — n равно нулю, возврат результата 1
S n' — n равно n' плюс один. n' здесь очевидно меньше n
рекурсивный вызов (factorial n') вызывает эту же функцию с аргументом n' который меньше изначального n, значит в какой-то момент рекурсии аргумент n станет равен нулю и рекурсия закончится
O — n равно нулю, возврат результата 1
S n' — n равно n' плюс один. n' здесь очевидно меньше n
рекурсивный вызов (factorial n') вызывает эту же функцию с аргументом n' который меньше изначального n, значит в какой-то момент рекурсии аргумент n станет равен нулю и рекурсия закончится
p
ну это и в идрисе
а
да
а
я просто хз какой у kolsky бекграунд)
а
Если попробовать увеличить n, то будет ошибка
p
а если n' - 10 ?
