(no subject)

Конструктивные зависимые теории типов являются очень заманчивым кандидатом на роль основания математики следующего поколения (вместо теории множеств) по двум причинам:
1) они интернализуют понятия утверждения и доказательства, т.е. и утверждения и доказательства сами являются объектами теории, любые синтаксические манипуляции над ними и даже проверка верности доказательств тоже являются понятиями, формулируемыми на языке теории;
2) они имеют вычислительную интерпретацию: естественную синтаксическую модель, которая весьма надёжно обосновывает их состоятельность.

Типовым неудобством конструктивных зависимых теорий типов (непротиворечивых типизированных лямбда-исчислений) является их неполнота по Тьюрингу в том смысле, что невозможно определить тип Nat ->* Nat, содержащий все тотальные вычислимые функции на натуральных числах.

Это неудобство можно было бы обойти в КЗТТ, в которой реализуем тип ординальных символов KleeneO (http://akuklev.livejournal.com/1127115.html) и тип Nat -> Nat содержит все функции обратные функции Харди, т.е. функции

  R_o(n: Nat) = max{m: Nat. H_o(m) < n}.

Для любого ординального символа о функция R_o тотальна и возрастает (нестрого) монотонно, однако утверждение, что R_o сюрьективна, эквивалентно утверждению о том, что ординальный символ действительно кодирует ординал.

Предположительно, для этого достаточно чтобы в тип Nat -> Nat входили функции, получаемые при помощи нисходящей рекурсии. Такие функции задаются типом тройкой

  t: (State: Type, initialState: State, step: (Nat, State) -> Optional[State]),

где step элементарная (нерекурсивная) функция. Применение тройки к натуральному числу n осуществляется по следующему алгоритму:

var state = initialState
for (var i = n; i > 0; i--):
   step(i, state) match:
      Nothing => break
      Value(newState) => state = newState
   end
return i;

С одной стороны, функции, вычисляемые данным алгоритмом заведомо завершаются, с другой стороны при достаточном богатстве возможных типов State, таким образом должно быть возможно представить все функции R_o.

Для всякой тотальной функции f существует рекурсивный счётный ординал из фундированности которого следует тотальность f, всякая тотальная функция из X в Y может быть представлена как

  (x: X) -> (r: Nat, R_o(r) = |x|) -> Y,

для какого-то ординального символа о.

В минималистичной КЗТТ простые функциональные типы X -> Y должны включать только функции, нисходяще-рекурсивные по размеру |x| аргумента x, чтобы тип любой невычислимой INPLACE функции отражал её вычислительную сложность, а тип всякого доказательства отражал потребную для этого доказательства proof theoretic strength. Cогласно результатам Уилларда, к такой логической системе неприменима вторая теорема Гёделя о неполноте, т.е. при удачной аксиоматизации такая КЗТТ может оказаться способна доказать собственную непротиворечивость*. Это делает такую минималистичную КЗТТ особенно интересным кандидатом на роль базовой метаматематической теории, добавляя в которую аксиомы о фундированности тех или иных ординалов доказывают непротиворечивость более сложных теорий.

______
* В том смысле, что из нулевого контекста никогда невозможно вывести одновременно суждение и его отрицание.