Изменения

Перейти к: навигация, поиск

Примитивно рекурсивные функции

281 байт добавлено, 22:50, 13 января 2012
Нет описания правки
* Согласно китайской теореме об остатках, если некоторые натуральные числа <tex>k_0, \dots k_n</tex> попарно взаимно просты, то для любых целых чисел <tex>u_0, \dots u_n</tex>, таких, что <tex>0 \le k_i < u_i</tex>, найдется такое целое число <tex>b</tex>, для которого выполнено <tex>k_i = b \% u_i</tex>. Возьмем <tex>b</tex>, подсказываемое теоремой об остатках.
}}
 
{{Теорема
|statement=Всякая рекурсивная функция представима в арифметике.
|proof=
Представимость первых четырех примитивов уже показана. Покажем представимость примитивной рекурсии и операции минимизации.
Пусть есть некоторый <tex>R \langle{} f,g \rangle</tex>. Соответственно, <tex>f</tex> и <tex>g</tex> уже представлены как некоторые формулы <tex>F</tex> и <tex>G</tex>. Из определения <tex>R\langle{}f,g\rangle</tex> мы знаем, что для значения <tex>R \langle{} f,g \rangle (x_1,...x_{n+1})</tex> должна существовать последовательность <tex>a_0 ... a_{x_{n+1}}</tex> результатов применения функций f и g &mdash; значений на одно больше, чем итераций в цикле примитивной рекурсии, а это количество определяется последним параметром функции <tex>R \langle{}f,g\rangle</tex>. При этом:
Значит, по лемме, должны существовать такие числа <tex>b</tex> и <tex>c</tex>, что <tex>\beta (b,c,i) = a_i</tex> для <tex>0 \le i \le x_{n+1}</tex>.
Приведенные рассуждения позволяют построить следующую формулу, представляющую <tex>R\langle{}f,g\rangle (x_1, ... x_{n+1})</tex>:
 
<tex>R(x_1, \dots x_{n+1}, a) := \exists b \exists c (\exists k (B (b,c,0,k) \& F (x_1,...x_n, k))</tex> <tex>\;\;\;\& B (b,c,x_{n+1},a)</tex> <tex>\;\;\;\& \forall k (k < x_{n+1} \rightarrow \exists d \exists e (B (b,c,k,d) \& B (b,c,k',e) \& G (x_1,..x_n,k,d,e)))</tex>
Рассмотрим конструкцию <tex>\mu\langle{}f\rangle</tex>. <tex>f</tex> уже представлено как некоторая формула <tex>F</tex>. Тогда формула <tex>M (x_1, \dots x_n,y) := F(x_1, \dots x_n,y,0) \& \forall z (z < y \rightarrow \neg F (x_1, \dots x_n,z,0))</tex> представит <tex>\mu\langle{}f\rangle</tex>.
}}
Анонимный участник

Навигация