Определение функции

[EminentVictorians]

Насколько я знаю, в любой теории множеств определение функции более менее одно и то же: либо как график, либо как тройка (домен, график, кодомен) либо как-нибудь еще подобным образом (например, можно выкинуть кодомен). График определяется как функциональное отношение.

Я бы хотел узнать, существуют ли более "синтаксические" подходы к определению функции. Хочется, чтобы выражение "переменная $y$ зависит от переменной $x$" было базовой конструкцией, не таскающей семантику множеств, декартовых произведений, подмножеств, отношений и т.д. Другими словами, хочется сместить акцент с функций (желательно полностью убрать их в их теоретико-множественном понимании) на переменные, зависящие друг от друга. Как вариант - сводить функцию буквально к корректной записи на бумаге с участием одной или нескольких свободных переменных.

Т.е. надо чтобы вместо классических множеств разговор шел о переменных, их именах, свободных и связанных вхождениях, правилах подстановки и т.д. Композиция - это не множество, а подстановка. Интересно бы понять, чем окажется область определения. Фрэймворк теории множеств слишком статичный, в ней область определения - это заранее зафиксированное множество. А в синтаксическом подходе есть шанс, что получится говорить о функции, не зная точно её область определения. Наивный вариант - определять область определения как элементы, при которых выражение имеет смысл, и при этом не различать функцию и её сужение. Но вдруг можно как-то поинтереснее.

[dgwuqtj]

Бестиповое лямбда-исчисление подойдёт?

[Geen]

EminentVictorians в сообщении #1650765 писал(а):

Но вдруг можно как-то поинтереснее.

Синус на октанионах? это достаточно интересно?

-- 19.08.2024, 23:09 --

А функция Дирихле, например, непрерывна будет?

[EminentVictorians]

dgwuqtj в сообщении #1650766 писал(а):

Бестиповое лямбда-исчисление подойдёт?

Да, это одно из направлений, в которые я смотрю. Точнее, мне это все интересно с точки зрения матанализа, поэтому сразу есть смысл смотреть в сторону дифференциального лямбда исчисления (расширение просто типизированного лямбда исчисления). Но это больше про компьютерное дифференцирование. А хотелось бы ориентированное на обычное использование человеком, что-то типа "матанализ, основанный на переменных количествах". Но не учебник Эйлера конечно, а нормальный уровень строгости с переменными, подстановками, свободными вхождениями и т.д.

Geen в сообщении #1650767 писал(а):

Синус на октанионах? это достаточно интересно?

А поподробнее можно? Пока не очень понимаю, о чем речь.

Geen в сообщении #1650767 писал(а):

А функция Дирихле, например, непрерывна будет?

Функцию Дирихле, в идеале, вообще не должно быть возможности определить. Но это немного смежная тема. В этой теме хотелось бы поговорить про синтаксический подход к функциям вообще.

[dgwuqtj]

EminentVictorians, вы же понимаете разницу между синтаксисом и семантикой у формальной теории? В классическом матанализе одной переменной можно выкинуть все теоретико-множественные средства и оставить синтаксис в виде языка первого порядка. Есть два сорта переменных (для значений и для функций), есть функциональные символы для применения функции к аргументу и для композиции, есть также функциональные символы для арифметических операций и дифференцирования. И есть куча констант для с стандартных чисел и функций. А множества появляются уже в семантике.

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

[EminentVictorians]

dgwuqtj в сообщении #1650773 писал(а):

вы же понимаете разницу между синтаксисом и семантикой у формальной теории?

Я думаю да. Формальная система - чисто синтаксическая конструкция. Значки и правила по которым они преобразуются. Семантика - это когда мы хотим наделить их смыслом, т.е. поставить в соответствие функциональным символам - функции, а предикатным символам - отношения. При таком определении семантика - всегда теоретико-множественная штука. Для безтипового лямбда исчисления в качестве семантики берут конкретную категорию с объектами - полными ч.у.м, наделенными конкретной топологией (Скотта) и стрелками - непрерывными в этой топологии отображениями. И эта категория декартово замкнута. Вроде все понятно.

dgwuqtj в сообщении #1650773 писал(а):

В классическом матанализе одной переменной можно выкинуть все теоретико-множественные средства и оставить синтаксис в виде языка первого порядка. Есть два сорта переменных (для значений и для функций), есть функциональные символы для применения функции к аргументу и для композиции, есть также функциональные символы для арифметических операций и дифференцирования. И есть куча констант для с стандартных чисел и функций. А множества появляются уже в семантике.

Я просто хочу не совсем классический матанализ. Я хочу получить матанализ без пределов, где можно оперировать dx как обычным числом. Но я хочу это получить не за счет всяких нестандартных моделей, нестандартных теорий множеств и т.д., а немного по-другому. Я хочу изменить само определение функции (не как отображение между множествами, а как корректную запись со свободной переменной) и хочу сделать какой-нибудь синтаксический мув, чтобы оперировать с dx. Как вариант - перегрузить оператор равенства (чтобы в некоторых случаях оно, например, выполнялось только с точностью до бесконечно малых) или изменить саму "семантику" числа (не воспринимать число как идеальную точку и конкретное значение). Т.е. мне надо, чтобы например производная сложной функции доказывалась так:

$$f(g(x))' = \frac{f(g(x + dx) - f(g(x))}{dx} = \frac{f(g(x) + g'(x)dx) - f(g(x)))}{dx} = \frac{f(g(x)) + f'(g(x))g'(x)dx - f(g(x))}{dx} = $$ $$ = \frac{f'(g(x))g'(x)dx}{dx} = f'(g(x))g'(x)$$

[dgwuqtj]

EminentVictorians в сообщении #1650777 писал(а):

Но я хочу это получить не за счет всяких нестандартных моделей, нестандартных теорий множеств и т.д., а немного по-другому. Я хочу изменить само определение функции (не как отображение между множествами, а как корректную запись со свободной переменной) и хочу сделать какой-нибудь синтаксический мув, чтобы оперировать с dx.

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

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

Как мне кажется, придумывали это не для упрощения обычной дифференциальной геометрии, а скорее для переноса результатов в интуиционистскую математику, в другие топосы (не $\mathbf{Set}$), ну и для пруфчекеров.

[Утундрий]

$d$ как нильпотент?

[EminentVictorians]

dgwuqtj в сообщении #1650779 писал(а):

Так всякие нестандартные модели примерно это же и делают, если смотреть только на синтаксическую часть.

В обычном нестандартном анализе надо четко отслеживать, какие утверждения формализуются в логике первого порядка, а какие - нет. Я не понимаю, как можно с этим жить. По-моему, на это уходит сил гораздо больше, чем даже постоянные проверки областей определения и критерия Лебега. А еще таскается вся эта теоретико-множественная "семантика" с ультрафильтрами (я говорю о семантике в том смысле, что под нестандартными действительными числами понимаются конкретные понятно как построенные множества, пусть и неконструктивно). А еще напрягает, что $^*\mathbb R$ - поле.

Что касается Т.Тао и его дешевой версии нестандартного анализа, то там все более-менее то же самое, просто вместо ультрафильтра берется обычный фильтр Фреше на $\mathbb N$ (который не ультрафильтр). Вроде конструктивнее, но все равно надо отслеживать, что в каком языке и как формулируется (и там какой-то прикол со связками отрицания и дизъюнкции - их вроде надо избегать и формулировать для них противоположные обратным теоремы). В общем тоже какая-то фигня с логикой. А мне хочется проще, чтобы без отслеживания всех этих формальных утверждений и связок. Пусть даже придется заплатить тем, что числа перестанут быть полем, или станут ограниченными или еще что-нибудь.

dgwuqtj в сообщении #1650779 писал(а):

Как мне кажется, придумывали это не для упрощения обычной дифференциальной геометрии, а скорее для переноса результатов в интуиционистскую математику, в другие топосы (не $\mathbf{Set}$), ну и для пруфчекеров.

Вот, мне тоже так кажется. Мне наверное надо что-то не такое серьезное. Должны же быть какие-нибудь фриковатые, но строгие, версии матанализа, более урезанные по сравнению со стандартным, но зато проще на преобразования.

Утундрий в сообщении #1650780 писал(а):

$d$ как нильпотент?

Я не знаю, как должен вести себя dx при перемножении на самого себя (но больше ставлю на то, что должен быть ноль, а не бесконечно малая более высокого порядка как в $^*\mathbb R$). Т.е. скорее всего да, нильпотент.

[dgwuqtj]

EminentVictorians в сообщении #1650783 писал(а):

В общем тоже какая-то фигня с логикой.

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

Вообще я пока не понял вашу цель, что этот язык должен охватывать? Одно дело дифференцировать формульные выражения из элементарных функций и неких их расширений (специальных функций или решений ОДУ, скажем), то есть эдакий символьный калькулятор. Другое дело - иметь формальную систему для доказательств, где уже нужны хотя бы регулярная логика и те самые нелюбимые вами предикаты.

[dmd]

EminentVictorians в сообщении #1650777 писал(а):

Я просто хочу не совсем классический матанализ. Я хочу получить матанализ без пределов, где можно оперировать dx как обычным числом. Но я хочу это получить не за счет всяких нестандартных моделей, нестандартных теорий множеств и т.д., а немного по-другому. Я хочу изменить само определение функции (не как отображение между множествами, а как корректную запись со свободной переменной) и хочу сделать какой-нибудь синтаксический мув, чтобы оперировать с dx. Как вариант - перегрузить оператор равенства (чтобы в некоторых случаях оно, например, выполнялось только с точностью до бесконечно малых) или изменить саму "семантику" числа (не воспринимать число как идеальную точку и конкретное значение). Т.е. мне надо, чтобы например производная сложной функции доказывалась так:

$$f(g(x))' = \frac{f(g(x + dx) - f(g(x))}{dx} = \frac{f(g(x) + g'(x)dx) - f(g(x)))}{dx} = \frac{f(g(x)) + f'(g(x))g'(x)dx - f(g(x))}{dx} = $$ $$ = \frac{f'(g(x))g'(x)dx}{dx} = f'(g(x))g'(x)$$

Ничего не получится, пока Вы привязаны к $f(x)$-синтаксису. Он не полон, не исчерпывающ априори. Это просто дремучее средневековье. Все выглядит так, словно мы все еще чертим полет пушечного ядра на глиняной дощечке, касательную строим, угол вычисляем. Это примитивное офизичивание, не стоит его снова повторять. Не надо привязывать себя к "графику функции", даже для наипростейшего одномерного нелинейного изменения нужен безконечный набор разных "графиков функций".
Внутри dx два состояния - начальное и конечное. Где они в dx-записи? Производная - это просто скорость изменения функции, одно состояние скорости, "мгновенная" скорость. Зачем определять производную как df/dx? Эта кажущаяся примитивная простота вовсе не является простой при внимательном строгом рассмотрении. Производную можно и нужно определять в более естественной форме без каких либо фракций. Но начать надо конечно с определения функции, и это, мне думается, будет самым сложным шагом. Потому что именно правильное определение функции вытащит матанализ из средневековья.

[EminentVictorians]

dgwuqtj в сообщении #1650784 писал(а):

Другое дело - иметь формальную систему для доказательств, где уже нужны хотя бы регулярная логика и те самые нелюбимые вами предикаты.

Доказывать теоремы тоже хотелось бы. По типу доказательства производной сложной функции.

Могу еще такой пример привести (доказательство теоремы о дифференцировании интеграла с переменным верхним пределом)
Пусть есть функция $f(x)$ определенная на отрезке $[a, b]$ и интегрируемая на нём по Риману. Пусть она непрерывна в точке $x_0$.
Положим

$$F(x) := \int\limits_{a}^{x} f(t)dt$$

Докажем, что $F'$ дифференцируема в $x_0$ и что $F'(x_0) = f(x_0)$

$$F'(x_0) = \frac{F(x_0 + dx) - F(x_0)}{dx} = \frac{\int\limits_{a}^{x_0 + dx}f(t)dt - \int\limits_{a}^{x_0}f(t)dt}{dx} = $$

$$ = \frac{\int\limits_{a}^{x_0}f(t)dt + \int\limits_{x_0}^{x_0 + dx}f(t)dt- \int\limits_{a}^{x_0}f(t)dt}{dx} = \frac{\int\limits_{x_0}^{x_0 + dx}f(t)dt}{dx} = $$

$$ = \frac{f(x_0)dx}{dx} = f(x_0)$$

Факт дифференцируемости $F$ в точке $x_0$ доказался непосредственно путем нахождения $F'(x_0)$, т.е. буквально тем, что все переходы в равенстве выше были корректны (с т.з. этого самодельного матанализа) и что это равенство чем-то закончилось. И видно, зачем надо было требовать непрерывность $f$ в точке $x_0$ (чтобы выполнить предпоследнее равно в строчке преобразований)

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

[dgwuqtj]

EminentVictorians в сообщении #1650811 писал(а):

Примерно такой матанализ мне нужен.

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

[EminentVictorians]

dgwuqtj в сообщении #1650840 писал(а):

Так что лучше разбирайтесь с синтетической дифференциальной геометрией.

Это слишком тяжеловесный аппарат для меня.


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

EminentVictorians в сообщении #1650811 писал(а):

Пусть есть функция $f(x)$ определенная на отрезке $[a, b]$ и интегрируемая на нём по Риману. Пусть она непрерывна в точке $x_0$.
Положим

$$F(x) := \int\limits_{a}^{x} f(t)dt$$

Докажем, что $F'$ дифференцируема в $x_0$ и что $F'(x_0) = f(x_0)$

Доказательство:

$$F'(x_0) = \lim\limits_{\Delta x \to 0}^{} \frac{F(x_0 + \Delta x) - F(x_0)}{\Delta x} = \lim\limits_{\Delta x \to 0}^{} \frac{\int\limits_{a}^{x_0 + \Delta x}f - \int\limits_{a}^{x_0}f}{\Delta x} = $$

$$ = \lim\limits_{\Delta x \to 0}^{} \frac{\int\limits_{a}^{x_0}f + \int\limits_{x_0}^{x_0 + \Delta x}f- \int\limits_{a}^{x_0}f}{\Delta x} = \lim\limits_{\Delta x \to 0}^{} \frac{\int\limits_{x_0}^{x_0 + \Delta x}f}{\Delta x} = $$

и все, дальше у меня продолжать цепочку равенств не получается.

Понятно, что этот предел равен $f(x_0)$. Это можно в лоб доказать:

Возьмем произвольную $\varepsilon$-окрестность точки $f(x_0)$. Существует $\delta > 0$ такая, что для всех $t$ таких, что $| t - x_0 | < \delta$ (и при которых функция $f$ определена) выполняется $|f(t) - f(x_0)| < \varepsilon$ (т.к. $f$ по условию непрерывна в $x_0$). Выберем тогда $\Delta x$ такой, что $|\Delta x| < \delta$ (и если рассматривать этот $\Delta x$ как отрезок, то он должен быть еще и подмножеством отрезка $[a, b]$). Для всех $t$, попавших в отрезок $\Delta x$, выполняется следующее:

$$f(x_0) - \varepsilon < f(t) < f(x_0) + \varepsilon$$

Отсюда следует, что

$$(f(x_0) - \varepsilon) |\Delta x| \quad \leqslant \int\limits_{\operatorname{min} (x_0, x_0 + \Delta x)}^{\operatorname{max} (x_0, x_0 + \Delta x) } f \quad \leqslant \quad (f(x_0) + \varepsilon) |\Delta x| \quad \quad (1)$$

$$f(x_0) - \varepsilon \quad \leqslant \frac{\int\limits_{\operatorname{min} (x_0, x_0 + \Delta x)}^{\operatorname{max} (x_0, x_0 + \Delta x) } f}{|\Delta x|} \quad \leqslant \quad f(x_0) + \varepsilon \quad \quad (2)$$

Учитывая

$$ \left| \int\limits_{x_0}^{x_0 + \Delta x}f \right| = \left| \int\limits_{\operatorname{min} (x_0, x_0 + \Delta x)}^{\operatorname{max} (x_0, x_0 + \Delta x) } f \right|$$

получаем, что

$$\frac{ \int\limits_{\operatorname{min} (x_0, x_0 + \Delta x)}^{\operatorname{max} (x_0, x_0 + \Delta x) } f }{|\Delta x|} = \frac{\int\limits_{x_0}^{x_0 + \Delta x}f}{\Delta x}$$

а значит (см (2) ):

$$f(x_0) - \varepsilon \quad \leqslant \frac{\int\limits_{x_0}^{x_0 + \Delta x}f}{\Delta x} \quad \leqslant \quad f(x_0) + \varepsilon$$

что и доказывает нужное нам утверждение.





Мне не нравится, что пришлось обращаться к определению предела. Можно ли доказать это утверждение, путем продолжения той цепочки равенств из самого начала доказательства (т.е. продолжать цепочку равенств, начинающуюся с $F'(x_0) = ... = ... $)), чтобы по итогу прийти к $f(x_0)$?

[dgwuqtj]

EminentVictorians в сообщении #1651429 писал(а):

Можно ли доказать это утверждение, путем продолжения той цепочки равенств

Без проблем,

$$\lim_{\Delta x \to 0} \frac{\int_{x_0}^{x_0 + \Delta x} f}{\Delta x} = \lim_{\Delta x \to 0} \frac{\int_{x_0}^{x_0 + \Delta x} (f(x_0) + o(1))}{\Delta x} = f(x_0) + \lim_{\Delta x \to 0} \frac{\int_{x_0}^{x_0 + \Delta x} o(1)}{\Delta x} = f(x_0) + \lim_{\Delta x \to 0} \frac{o(\Delta x)}{\Delta x} = f(x_0).$$

Первое равенство использует непрерывность, третье — это оценка интеграла через супремум подынтегральной функции.