История изменений

Вот fib₁-not-eq-1+fib₂ это то же самое.

Вот нашлось:

http://www.cs.bham.ac.uk/~mhe/.talks/popl2012/ -> http://www.cs.bham.ac.uk/~mhe/agda/ -> http://www.cs.bham.ac.uk/~mhe/agda/RicesTheoremForTheUniverse.html

We show that a Martin-Lof universe `a la Russell satisfies the conclusion of Rice's Theorem: it has no non-trivial, decidable, extensional properties. We derive this as a corollary of more general topological facts in type theory, which don't rely on Brouwerian continuity axioms.

Ну если он так работает, то ничего не выйдет, да.

Раз пишем программы в виде обычной записи с рекурсией общего вида, то решать нужно обычную проблему останова — получаем такой же код как и в любом другом языке с рекурсивными определениями общего вида, функции которые завершаются это ровно те функции которые решают проблемы из R (decidable), тогда как функция которая будет это детектировать строго частична, может виснуть и решает проблему из RE (semidecidable), то есть проблему останова, если мы хотим чтобы она решала эту проблему разрешимо и не висла, то это проблема из R, нам нужно искать тотальные функции которые решают проблемы из класса меньшего R, например, PR и соответствующие примитивно-рекурсивные программы легко детектируется, дальше можно добавить немного — структурная рекурсия, лексикографическая.

Это в лямбда кубе у нас нет рекурсивных определений, только термы и правила игры с ними, так что если им следовать, то всё будет завершаться, строгая нормализация это свойство, проверять ничего не нужно.

Ещё интересный вопрос — функция может быть тотальна «на самом деле», но отбрасываться TC, есть техника которая позволяет уговорить TC принять такую функцию — руками доказать что она завершается (уменьшаться будет не основной аргумент, а доказательство). Для всякой ли программы которая тотальна «на самом деле» и пишется в языке существует такое доказательство в языке?

Собственно, вопрос состоял в том, есть ли там по дефолту определения натуральных чисел и операций над ними?

Есть, конечно. http://www.csie.ntu.edu.tw/~b94087/ITT.pdf — тут про натуральные числа ближе к концу.

Вот fib₁-not-eq-1+fib₂ это то же самое.

Вот нашлось:

http://www.cs.bham.ac.uk/~mhe/.talks/popl2012/ -> http://www.cs.bham.ac.uk/~mhe/agda/ -> http://www.cs.bham.ac.uk/~mhe/agda/RicesTheoremForTheUniverse.html

We show that a Martin-Lof universe `a la Russell satisfies the conclusion of Rice's Theorem: it has no non-trivial, decidable, extensional properties. We derive this as a corollary of more general topological facts in type theory, which don't rely on Brouwerian continuity axioms.

Ну если он так работает, то ничего не выйдет, да.

Раз пишем программы в виде обычной записи с рекурсией общего вида, то решать нужно обычную проблему останова — получаем такой же код как и в любом другом языке с рекурсивными определениями общего вида, функции которые завершаются это ровно те функции которые решают проблемы из R (decidable), тогда как функция которая будет это детектировать строго частична, может виснуть (строго в случае отрицательных ответов) и решает проблему из RE (semidecidable), то есть проблему останова, если мы хотим чтобы она решала эту проблему разрешимо и не висла, то это проблема из R, нам нужно искать тотальные функции которые решают проблемы из класса меньшего R, например, PR и соответствующие примитивно-рекурсивные программы легко детектируется, дальше можно добавить немного — структурная рекурсия, лексикографическая.

Это в лямбда кубе у нас нет рекурсивных определений, только термы и правила игры с ними, так что если им следовать, то всё будет завершаться, строгая нормализация это свойство, проверять ничего не нужно.

Ещё интересный вопрос — функция может быть тотальна «на самом деле», но отбрасываться TC, есть техника которая позволяет уговорить TC принять такую функцию — руками доказать что она завершается (уменьшаться будет не основной аргумент, а доказательство). Для всякой ли программы которая тотальна «на самом деле» и пишется в языке существует такое доказательство в языке?

Собственно, вопрос состоял в том, есть ли там по дефолту определения натуральных чисел и операций над ними?

Есть, конечно. http://www.csie.ntu.edu.tw/~b94087/ITT.pdf — тут про натуральные числа ближе к концу.