Рекурсивная функция

[QuantumCoder]

Читаю книгу Terence Tao, Analysis I
В части 2.1 (The Peano axioms) было утверждение:


Далее по книге после части 3.5 (Cartesian products) есть упражнение:


Лемма 3.5.12


Я что-то вообще не догоняю, при чем тут 3.5.12?

[mihaild]

Доказательство аналогично: индукцией по $n$ доказываем существование единственной $a_n$. За счет единственности, в шаге индукции при построении $a_{n++}$ можно использовать конкретную $a_n$, и из неё строить $a_{n++}$.

[QuantumCoder]

mihaild в сообщении #1637861 писал(а):

Доказательство аналогично: индукцией по $n$ доказываем существование единственной $a_n$. За счет единственности, в шаге индукции при построении $a_{n++}$ можно использовать конкретную $a_n$, и из неё строить $a_{n++}$.

Я в общем так и делал, просто не очень понимаю при чем тут 3.5.12. Сбивает, что зачем-то автор ссылается на 3.5.12. Можно было просто сказать, что доказываем по индукции.
Мое доказательство следующее. Cначала по индукции докажем, что существует такая $a$. Для 0 значение этой функции определено, как $c$. По одной из аксиом Пеано не существует $n$ такого, что $n++ = 0$. Это значит, что ни одно $a(n++)$ не переопределяет $a(0)$ и значение определено однозначно. Теперь предположим, что для $n$ значение $a(n)$ определено однозначно. Докажем для $n++$. $a(n++) = f(n, a(n))$. По предположению индукции $a(n)$ определено однозначно, значит f(n, a(n)) тоже определено однозначно. По одной из аксиом Пеано $n \neq m => n++ \neq m++$. То есть ни один $m++$ не переопределяет значение $a(n++)$ и оно определено однозначно. Следовательно заключаем, что для всех натуральных чисел $n$ функция $a(n)$ определена однозначно.

Вот тут непонятно, разве из существования не следует ее единственность. Ну типо возьмем 2 функции $a$ и $a'$, где $a(0) = c$ и $a(n++) = f(n, a(n))$ и $a'(0) = c$ и $a'(n++) = f(n, a'(n))$. Они же одинаковые с точностью до обозначения. Или этого мало?

[mihaild]

QuantumCoder в сообщении #1637864 писал(а):

Cначала по индукции докажем, что существует такая $a$.

Какое в точности утверждение Вы тут доказываете по индукции? По индукции доказываются утверждения, начинающиеся с квантора всеобщности по $n$.
Обратите внимание, что Тао сначала для каждого $n$ доказывает существование функции, определенной на $\overline{0, n}$ - у каждой функции свой домен. И это не просто так.

[QuantumCoder]

mihaild в сообщении #1637865 писал(а):

QuantumCoder в сообщении #1637864 писал(а):

Cначала по индукции докажем, что существует такая $a$.

Какое в точности утверждение Вы тут доказываете по индукции? По индукции доказываются утверждения, начинающиеся с квантора всеобщности по $n$.
Обратите внимание, что Тао сначала для каждого $n$ доказывает существование функции, определенной на $\overline{0, n}$ - у каждой функции свой домен. И это не просто так.

Я доказываю тут, что $a(n)$ определена корректно для любого $n$.

[mihaild]

QuantumCoder в сообщении #1637867 писал(а):

Я доказываю тут, что $a(n)$ определена корректно для любого $n$.

А что это значит? Что такое "корректно определена", какая еще $a$? У нас еще нет никакой $a$ чтобы про неё что-то доказывать.
Попробуйте более подробно записать Ваше утверждение, чтобы было понятно где какие кванторы: "для любого $n$ существует [что?]" - это сделать не получится.

[QuantumCoder]

mihaild в сообщении #1637868 писал(а):

QuantumCoder в сообщении #1637867 писал(а):

Я доказываю тут, что $a(n)$ определена корректно для любого $n$.

А что это значит? Что такое "корректно определена", какая еще $a$? У нас еще нет никакой $a$ чтобы про неё что-то доказывать.
Попробуйте более подробно записать Ваше утверждение, чтобы было понятно где какие кванторы: "для любого $n$ существует [что?]" - это сделать не получится.

Мы хотим доказать, что функция $a: N -> N$ такая что $a(0) = c$ и $a(n++) = f(n, a(n))$ существует и единственна. Тао определяет функцию, как:

Окей, нам ничего не мешает построить такую функцию. Зададим ее как:
$a(0) = c$ и $a(n++) = f(n, a(n))$
То есть соответствие мы задали. Осталось убедиться, что оно сопоставляет для любого элемента из domain единственный элемент из range. Это я и доказывал индуктивно, что для любого $n$ значение $a(n)$ определено и единственно. Например, если бы не было аксиомы о том, что successor любого натурального числа не равен 0, например 3++ = 0. То это соответствие задало бы для 0 два значения. $a(0) = c$ и $a(3++) = f(3, a(3))$. Что некорректно с точки зрения определения функции. То есть я доказал, что построенная функция сопоставляет каждому элементу из domain ровно один элемент из range.

[mihaild]

QuantumCoder в сообщении #1637873 писал(а):

Зададим ее как:
$a(0) = c$ и $a(n++) = f(n, a(n))$

Это не является корректным заданием свойства (property) - Вы ссылаетесь в нем на определяемый объект. А прежде чем доказывать функциональность, нужно собственно задать свойство.

[QuantumCoder]

Идем прям по определению функции:
$X = N$
$Y = N$
Определим свойство $P(x, y)$ следующим образом $P(x, y)$ верно исключительно в случае, когда $x = 0$ и $y = c$, а так же верно исключительно в случае, когда $x = n++$ и $y = f(n, a(n))$, где $a(n)$ - это такой $y \in Y$ для которого $P(n, y)$ верно.

Разве я не могу задать свойство таким образом?

[mihaild]

Свойства ничему ничего не сопоставляют, они истинны или ложны (сопоставляют только некоторые специальные свойства, задающие функцию).
Переписывая Вашу формулировку с учетом этого, получаем: $P(x, y)$ верно если $x = 0$ и $y = c$, или если $x = n++$ и (тут какой-то квантор, непонятно какой) $z$ такой что $y = f(n, z)$ и $P(n, z)$ выполнено. И тут очевидный вопрос - почему такое $P$ вообще существует?
Мы тут как раз доказываем возможность определений по рекурсии, их у нас пока нет. Так что в правой части определения на определяемую штуку ссылаться никак нельзя.

Сравните с доказательством у Тао: сначала доказываем, что для любого $n$ существует единственная нужная функция, определенная на начальном сегменте. Дальше из этого нужно будет построить нашу итоговую функцию, определенную на всех натуральных числах. Нигде в этом рассуждении мы не используем объект в процессе его построения.

[QuantumCoder]

А то, что он определяет $a_N(n++) = f(n, a(n))$ это опечатка получается? Должно было быть $a_N(n++) = f(n, a_N(n))$?

[mihaild]

Видимо так, да. У меня не получается придумать осмысленную интерпретацию в напечатанном варианте, а с таким исправлением как раз всё логично.

[QuantumCoder]

Окей, допустим. Тогда докажем индуктивно, что для любого натурального числа $N \in \mathbb {N}$ существует функция $a_N: \{n \in \mathbb {N}: n \leq N \} \to \mathbb {N}$, такая, что: $a_N(0) = c$ и $a_N(n++) = f(n, a_N(n))$. При чем такая функция уникальна.

Докажем для $N = 0$. В этом случае очевидно, что существует одна единственная функция $a_0$, такая, что $a_0(0) = c$.
Пусть для $N = k$ существует функция $a_k: \{n \in \mathbb {N}: n \leq k \} \to \mathbb {N}$, такая, что: $a_k(0) = c$ и $a_k(n++) = f(n, a_k(n))$. При чем такая функция уникальна.
Докажем для $N = k++$. Построим $a_{k++}: \{n \in \mathbb {N}: n \leq k++ \} \to \mathbb {N}$. Пусть $a_{k++}(0) = c$ и $a_{k++}(n++) = f(n, a_k(n))$. В силу построения $a_{k++}(n++) = a_k(n++)$ для всех $n < k$. А значит определение функции можно переписать в виде $a_{k++}(n++) = f(n, a_ {k++}(n))$. Остается доказать, что она уникальна. Предположим, что это не так и существует функция $a_{k++}': \{n \in \mathbb {N}: n \leq k++ \} \to \mathbb {N}$ такая, что $a_{k++}'(0) = c$ и $a_{k++}'(n++) = f(n, a_{k++}'(n))$. Очевидно, что $a_{k++}'(n++) = a_k(n++)$ для всех $n < k$. Потому что иначе мы могли бы взять ограничение функции $a_{k++}'$ на domain $\{n \in \mathbb {N}: n \leq k \} \to \mathbb {N}$ и получили бы функцию $a_k'$ отличную от $a_k$, что невозможно, так как она уникальна. Из $a_{k++}'(n++) = a_k(n++)$ для всех $n < k$ так же следует, что $a_{k++}'(k++) = f(k, a_{k++}'(k)) = f(k, a_k(k))$. Получается, что $a_{k++} = a_{k++}'$, а значит такая функция уникальна. Что закрывает индукцию.

Теперь построим $a: \mathbb {N} \to \mathbb {N}$ следующим образом: $a(0) = c$ и $a(n++) = a_{n++}(n++) = f(n, a_{n++}(n)) = f(n, a_n(n)) = f(n, a(n))$. Очевидно, что она уникальна, так как для любого $N$ ограничение этой функции на domain \{n \in \mathbb {N}: n \leq N \} \to \mathbb {N}$ совпадает с уникальной функцией $a_N$.

Ничего не напутал?

[mihaild]

Почти правильно.

QuantumCoder в сообщении #1638350 писал(а):

Теперь построим $a: \mathbb {N} \to \mathbb {N}$ следующим образом: $a(0) = c$ и $a(n++) = a_{n++}(n++) = f(n, a_{n++}(n)) = f(n, a_n(n)) = f(n, a(n))$.

Вот тут нужно чуть-чуть больше работы, потому что пока что у вас для каждого $n$ есть функция $a_n$, но нет общей функции $b$, определенной на $\mathbb N$, такой что $b(n) = a_n$. Тут тонкий момент, потому что в доказательстве леммы в $a_n$, $n$ - это просто индекс, а в построении $a$ становится полноценным аргументом. Как раз здесь понадобится уникальность $a_n$.

(Оффтоп)

Бывают похожие ситуации, когда для произвольного $n$ есть функции на начальном отрезке длины $n$, но из-за неуникальности в одну общую они не собираются - например, носки Расселла (набор пар носков, можно взять по одному носку из произвольного конечного количества пар, но невозможно взять по одному носку из каждой пары). Это довольно сложная конструкция, но ИМХО просто помнить о том, что вот так бывает полезно для отслеживания тонкостей.

Еще для доказательства уникальности даже предположения индукции не нужно: если есть две разных функции, то есть минимальное число, на котором они отличаются, и на этом числе для одной из них не выполнено рекуррентное соотношение.

[QuantumCoder]

Окей, поправил.

Согласно доказанной выше лемме мы можем сопоставить для каждого $n$ уникальную функцию $a_n$. Теперь построим $a: \mathbb {N} \to \mathbb {N}$ следующим образом: $a(0) = c$ и $a(n++) = a_{n++}(n++) = f(n, a_{n++}(n)) = f(n, a_n(n)) = f(n, a(n))$. Очевидно, что она уникальна, так как для любого $N$ ограничение этой функции на domain $\{n \in \mathbb {N}: n \leq N \} \to \mathbb {N}$ совпадает с уникальной функцией $a_N$.

mihaild в сообщении #1638351 писал(а):

Еще для доказательства уникальности даже предположения индукции не нужно: если есть две разных функции, то есть минимальное число, на котором они отличаются, и на этом числе для одной из них не выполнено рекуррентное соотношение.

Мне показалось, что я пока не могу использовать минимальный элемент, так как пока что не вводилось данное понятие.