Что такое логарифм или корневая операция в пространстве типов?

Недавно я читал «Две дуальности вычислений: отрицательные и дробные типы» . В статье рассматриваются типы сумм и типы товаров, в которых даны семантика для типов a - bи a/b.

В отличие от сложения и умножения, существует не одна, а две инверсии возведения в степень, логарифмы и корни. Если типы функций (a → b) являются теоретико-типовым возведением в степень, учитывая тип a → b(или b^a), что означает иметь тип logb(c)или тип a√c?

Имеет ли смысл вообще распространять логарифмы и корни на типы?

Если так, была ли какая-либо работа в этой области, и каковы некоторые хорошие указания о том, как понять последствия?

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

lo.logic pl.programming-languages type-theory algebra efrey
источник

Ответы:

Тип имеет логарифм по основанию из точно , когда . То есть, можно рассматривать как контейнер элементов в позициях , заданных . На самом деле, это вопрос с просьбой к тому , что мощность мы должны поднять , чтобы получить . $C$ $X$ $P$ $C \cong P\to X$ $C$ $X$ $P$ $P$ $X$ $C$

Имеет смысл работать с где - функтор, всякий раз, когда существует логарифм, что означает . Обратите внимание, что если , то у нас, конечно, есть , поэтому контейнер не говорит нам ничего интересного, кроме его элементов: контейнеры с выбором форм делают не имеют логарифмов. $\mathop{log}F$ $F$ $\mathop{log}\!_X(F\:X)$ $F\:X\cong \mathop{log}F\to X$ $F\:1\cong 1$

Знакомые законы логарифмов имеют смысл, когда вы думаете с точки зрения наборов позиций

\begin{array}{rcll} L о г (К 1) & знак равно & 0 & нет позиций в пустом контейнере \\ L о г я & знак равно & 1 & контейнер на одну, одну позицию \\ L о г (F \times г) & знак равно & L о г F + L о г г & пара контейнеров, выбор позиций \\ L о г (F \cdot г) & знак равно & L о г F \times L о г г & контейнер контейнеров, пара позиций \end{array}

$\begin{array}{rcl@{\qquad}l} \mathop{log} (\mathop{K}1) &=& 0 & \mbox{no positions in empty container}\\ \mathop{log} I &=& 1 & \mbox{container for one, one position}\\ \mathop{log} (F\times G) &=& \mathop{log}F+\mathop{log}G & \mbox{pair of containers, choice of positions} \\ \mathop{log} (F\cdot G) &=& \mathop{log}F\times\mathop{log}G & \mbox{container of containers, pair of positions} \end{array}$

Мы также где под связывателем. То есть путь к каждому элементу в некоторых кодатах определяется индуктивно путем итерации логарифма. Например, $\mathop{log}\!_X(\nu Y. T) = \mu Z. \mathop{log}\!_X T$ $Z=\mathop{log}\!_XY$

l o g S t r e a m = l o g_{X} (ν Y . X \times Y) = μ Z, 1 + Z знак равно N a T

$\mathop{log}\mathop{Stream} = \mathop{log}\!_X(\nu Y. X\times Y) = \mu Z. 1 + Z = \mathop{Nat}$

Учитывая, что производная сообщает нам тип в контекстах с одним отверстием, а логарифм сообщает нам позиции, мы должны ожидать соединение, и действительно

F 1 ≅ 1 \Rightarrow L о г F ≅ \partial F 1

$F\:1\cong 1 \;\Rightarrow\; \mathop{log}F\cong \partial F\:1$

Там, где нет выбора формы, позиция - это то же самое, что и контекст с одним отверстием, когда элементы стираются. В более общем смысле всегда представляет выбор формы вместе с позицией элемента в этой форме. $\partial F\:1$ $F$

Я боюсь, что могу сказать меньше о корнях, но можно начать с аналогичного определения и следовать своему носу. Для более широкого использования логарифмов типов, проверьте «Памятные функции, политипически!» Ральфа Хинце. Надо бежать...

pigworker
источник

Ответ от самого Да Мана. Добро пожаловать, Конор!

Андрей Бауэр

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

Эфри

Может ли это быть как-то связано с рядом Тейлора ln (1 + x)?

yatima2975

Интересно, с логарифмами и экспонентами ... что нам нужно для создания объекта Нейпира ? (например, предположительно уникальный объект, eтакой, что ∂e = e)

Рифмовая

Я не знаю ни одной работы, которая преследует эту линию, но несколько минут размышлений об этом привели меня к этой гипотезе: не будет ли «корень» экспоненциального типа просто кодоменом, а «логарифмом» экспоненты просто домен?

Марк Хаманн
источник

Правильно, поэтому я думаю, что ваша интуиция хороша, но ваш вывод неверен. Операция root и логарифм - это то, что вы получаете, когда вы «инвертируете» кодомен или домен соответственно, а не сами (со) домены. Вопрос в том, что мы подразумеваем под инвертированием и какую операцию двоичного типа он производит?

Эфри

x^{y}

$x^y$

y

$y$

x

$x$

x

$x$

y

$y$

Извините, я не совсем понял свою терминологию. Я не хочу спрашивать, «что является корнем, каков результат применения функции логарифма». Мне интересно, что такое операция рутирования. Что такое операция нахождения логарифма. Если →есть расходование, то, что является двумя типами под корневой операцией. Что такое два типа в логарифмической операции. То, что я подразумеваю под «инвертировать аргумент», - это то, что здесь не время объяснять. Я уточню свой вопрос, спасибо.

Эфри

В статье, на которую я ссылаюсь, приводится семантика для типа a - bи типа a / b. Меня не интересует результат сокращения операций логарифм и корень, а понимание их семантики как операторов двоичного типа.

Эфри