Барная рекурсия

Барная рекурсия — это обобщенная форма рекурсии, разработанная К. Спектором в его статье 1962 года. Она связана с индукцией бара таким же образом, как примитивная рекурсия связана с обычной индукцией , или трансфинитная рекурсия связана с трансфинитной индукцией .

Техническое определение

Пусть V , R и O — типы , а i — любое натуральное число, представляющее последовательность параметров, взятых V. из Тогда функциональная последовательность f функций f _n из V ^{я + н} → R в O определяется барной рекурсией из функций L _n : R → O и B с B _n : (( V ^{я + н} → р ) x ( V ^н → R )) → O, если:

• ж _н ((ла: В ^{я + н} ) r ) = L _n ( r ) для любого r достаточно долгого, чтобы L _{n + k} на любом расширении r равнялось L _n . Предполагая, что L — непрерывная последовательность, такой r должен существовать , поскольку непрерывная функция может использовать только конечное количество данных.
• f _n ( p ) = B _n ( p , (λ x : V ) f _{n +1} (cat( p , x ))) для любого p в V ^{я + н} → Р .

Здесь «cat» — это функция конкатенации , отправляющая p , x в последовательность, которая начинается с p и имеет x в качестве последнего члена.

(Это определение основано на определении Эскардо и Оливы. )

При условии, что для любой достаточно длинной функции (λα) r типа V ^я → R существует некоторое n такое, что L _n ( r ) = B _n ((λα) r , (λ x : V ) L _{n +1} ( r )), правило индукции бруска гарантирует, что f корректно определен.

Идея состоит в том, что последовательность расширяется произвольно, используя член рекурсии B достаточно длинный узел дерева последовательностей над V для определения эффекта, пока не будет достигнут ; тогда базовый термин L определяет окончательное значение f . Условие четкости соответствует требованию, чтобы каждый бесконечный путь в конечном итоге проходил через достаточно длинный узел: то же самое требование, которое необходимо для вызова индукции перемычки.

Принципы индукции бара и рекурсии бара являются интуиционистскими эквивалентами аксиомы зависимого выбора .