Как записать (f+g)(x) в виде обычной формулы?

[Sonic86]

Определение:
1. Любая переменная $x_j$ является обычной формулой. Любая функция $f_i$ является обычной формулой.
2. Если $A_1,...,A_n$ - обычные формулы, а $f$ - $n$-местная функция, то $f(A_1,...,A_n)$ - обычная формула.
3. Других обычных формул нет.
Рассмотрим выражение $f(x)+g(x)$. Его можно записать в виде $(f+g)(x)$. Но последнее выражение не является обычной формулой. Можно ли записать выражение в виде обычной формулы, в которой буква $x$ встречается всего 1 раз?
Попытки решения: $f(x)+g(x)=\mathrm{Apply}(f+g, x)$, где $\mathrm{Apply}$ - это какая-то неведомая функция, определяемая соотношением $(\forall f\in F)(\forall x \in D(f))f(x)=\mathrm{Apply}(f, x)$. Но я никакой $\mathrm{Apply}$ не знаю (кроме понятия "комбинация" из лямбда-исчисления, но и то плохо), поэтому сомневаюсь. Мне даже страшно представить то, где она определена.

[Munin]

Sonic86 в сообщении #1148846 писал(а):

Рассмотрим выражение $f(x)+g(x)$.

А оно-то разве "обычная"?

Я подозреваю, вам надо что-то типа $sum(f(x),g(x))$ из $sum(f,g),$ где и то и другое - "обычные" по вашему определению.

-- 03.09.2016 21:58:14 --

Причём, если $f$ и $g$ - 1-местные функции, а $sum$ - 2-местная функция, то про $sum(f,g)$ ничего подобного не сказано: это формула, но не функция вообще.

[Sonic86]

Munin в сообщении #1148858 писал(а):

А оно-то разве "обычная"?

Я подозреваю, вам надо что-то типа $sum(f(x),g(x))$ из $sum(f,g),$ где и то и другое - "обычные" по вашему определению.

Да, этот кусок я не продумал. Надо найти обычную формулу для $\mathrm{sum}(f(x),g(x))$.

[arseniiv]

Sonic86 в сообщении #1148846 писал(а):

Попытки решения: $f(x)+g(x)=\mathrm{Apply}(f+g, x)$

Но тут тоже встречается $f + g$!

-- Вс сен 04, 2016 09:43:49 --

А вот можно взять функцию $z$ с определением $z(f,g)(x) = f(x) + g(x)$. Это определение эквивалентно определениям $z(f,g) = x\mapsto f(x) + g(x)$ и $z = (f,g)\mapsto x\mapsto f(x) + g(x)$. Если $+\colon A\times A'\to A''$, тогда $f\colon B\to A, g\colon B'\to A'$ и $z\colon A^B\times A'^{B'} \to A''^{B\cap B'}$, скажем (и в строгом изложении эти аннотации должны рисоваться где-то рядом с $\mapsto$, и тогда выражения с ним будут самодостаточны). То?

P. S. Или, скажем, функцию $z\colon A^B\times A'^{B'}\times B\cap B' \to A''$, если двойное применение вдруг нежелательно.

-- Вс сен 04, 2016 09:45:45 --

Первая $z$ это и есть $\mathrm{sum}$ выше, я не пойми зачем назвал её новым именем.

[Sonic86]

arseniiv в сообщении #1148899 писал(а):

Sonic86 в сообщении #1148846 писал(а):

Попытки решения: $f(x)+g(x)=\mathrm{Apply}(f+g, x)$

Но тут тоже встречается $f + g$!

Имелось ввиду $\mathrm{sum}(f(x),g(x))=\mathrm{Apply}(\mathrm{sum}(f,g), x)$.

arseniiv в сообщении #1148899 писал(а):

А вот можно взять функцию $z$ с определением $z(f,g)(x) = f(x) + g(x)$. Это определение эквивалентно определениям $z(f,g) = x\mapsto f(x) + g(x)$ и $z = (f,g)\mapsto x\mapsto f(x) + g(x)$. Если $+\colon A\times A'\to A''$, тогда $f\colon B\to A, g\colon B'\to A'$ и $z\colon A^B\times A'^{B'} \to A''^{B\cap B'}$, скажем (и в строгом изложении эти аннотации должны рисоваться где-то рядом с $\mapsto$, и тогда выражения с ним будут самодостаточны). То?

P. S. Или, скажем, функцию $z\colon A^B\times A'^{B'}\times B\cap B' \to A''$, если двойное применение вдруг нежелательно.

-- Вс сен 04, 2016 09:45:45 --

Первая $z$ это и есть $\mathrm{sum}$ выше, я не пойми зачем назвал её новым именем.

М.б. и так можно (только тогда надо писать $z(f,g,x)$), пока не могу ответить явно.
А, нет, тогда мне надо так вопрос задать: пусть $h$ - двуместная функция, надо решить указанную задачу для $h(f(x),g(x))$. Тогда писать $z(h,f,g,x)$? И я опять не могу пока ответить явно.

[arseniiv]

Sonic86 в сообщении #1148903 писал(а):

Имелось ввиду $\mathrm{sum}(f(x),g(x))=\mathrm{Apply}(\mathrm{sum}(f,g), x)$

Но у вас в любом случае у $\mathrm{Apply}$ будут проблемы с определением, если она применяется к формулам — первая формула может не быть функцией. Если же ограничить первый аргумент функциями, это будет синонимом для обычного применения функции. Проблема тут только в том, чтобы сохранить информацию о том, что $\mathrm{sum}$ выдаёт функцию. Её можно решить, сопоставив всем формулам типы. Получится такая небольшая теория типов.

Sonic86 в сообщении #1148903 писал(а):

А, нет, тогда мне надо так вопрос задать: пусть $h$ - двуместная функция, надо решить указанную задачу для $h(f(x),g(x))$. Тогда писать $z(h,f,g,x)$?

Да, можно определить более общую версию $z$ для любого случая. Правда, мы пока не коснулись вопроса о том, определяются ли функции с помощью выше определённых формул, или они могут быть чёрными ящиками.

-- Вс сен 04, 2016 11:03:01 --

Понимаю, что плохой тон, но можно поинтересоваться контекстом этой задачи?

[Sonic86]

arseniiv в сообщении #1148905 писал(а):

Понимаю, что плохой тон, но можно поинтересоваться контекстом этой задачи?

Да все просто: проектирую некий алгоритм, который бы работал с математическими формулами. Только вот стандартно формулы представляются в виде синтаксических деревьев, а $(f+g)(x)$ - нет.

Мне тут в ЛС написали и показали, что я туплю - я на самом деле выписал определение обычной формулы так, что оно шире, чем синтаксические деревья: $+$ - функция, $f,g$ - обычные формулы, значит $+(f,g)$ - обычная формула, значит $+(f,g)(x)$ - обычная формула Только вот синтаксического дерева у моей формулы все равно нет (или есть? ). Значит мне надо определение обычной формулы корректировать так, чтобы получались синтаксические деревья.

Sonic86 в сообщении #1148846 писал(а):

Любая функция $f_i$ является обычной формулой.

Видимо, надо выкинуть этот кусок.

[Xaositect]

Лучше скорректируйте определение синтаксического дерева - вместо \begin{tikzpicture}\node[above] at (0,0) {$f$}; \node[below] at (-1,-1) {$x_1$}; \node[below] at (0,-1) {$x_2$}; \node[below] at (1,-1) {$x_3$}; \draw (0,0)--(-1,-1); \draw (0,0)--(0,-1); \draw (0,0)--(1,-1);\end{tikzpicture} делайте \begin{tikzpicture}\draw (0,0) circle (2pt); \node[below] at (-2,-1) {$f$}; \node[below] at (-1,-1) {$x_1$}; \node[below] at (0,-1) {$x_2$}; \node[below] at (1,-1) {$x_3$}; \draw (0,0)--(-2,-1); \draw (0,0)--(-1,-1); \draw (0,0)--(0,-1); \draw (0,0)--(1,-1);\end{tikzpicture}. Работать с таким деревом можно так же, как и с обычным, просто первый лист учитывать специально, как раньше корень. А формулы типа $+(f,g)(x)$ теперь позволяются. По сути это как дерево из применений функции (Ваша $\mathrm{Apply}$).

[Munin]

Xaositect
LISP?

[Xaositect]

По сути да.

[arseniiv]

Ага, S-expressions. Кстати, назначению типов это всё равно не помешает, хотя если в выражениях для $1+2$ и $f+g$ плюс один и тот же, правила понадобятся достаточно непростые. Ну, вычислять-то или как-то обрабатывать (хотя бы проверять на корректность) всё равно такие многозначные конструкции придётся в любом случае, и эти правила там будут присутствовать в неявном виде.

[Sonic86]

Xaositect в сообщении #1148920 писал(а):

Лучше скорректируйте определение синтаксического дерева - вместо \begin{tikzpicture}\node[above] at (0,0) {$f$}; \node[below] at (-1,-1) {$x_1$}; \node[below] at (0,-1) {$x_2$}; \node[below] at (1,-1) {$x_3$}; \draw (0,0)--(-1,-1); \draw (0,0)--(0,-1); \draw (0,0)--(1,-1);\end{tikzpicture} делайте \begin{tikzpicture}\draw (0,0) circle (2pt); \node[below] at (-2,-1) {$f$}; \node[below] at (-1,-1) {$x_1$}; \node[below] at (0,-1) {$x_2$}; \node[below] at (1,-1) {$x_3$}; \draw (0,0)--(-2,-1); \draw (0,0)--(-1,-1); \draw (0,0)--(0,-1); \draw (0,0)--(1,-1);\end{tikzpicture}. Работать с таким деревом можно так же, как и с обычным, просто первый лист учитывать специально, как раньше корень.

Ладно, буду пока считать, что так. Спасибо!