Qual é o logaritmo ou operação raiz no espaço de texto?

Recentemente, eu estava lendo As duas dualidades da computação: tipos negativo e fracionário . O artigo expande tipos de soma e tipos de produtos, fornecendo semântica para os tipos a - be a/b.

Ao contrário da adição e multiplicação, não há um, mas dois inversos de exponenciação, logaritmos e enraizamento. Se os tipos de função (a → b) são exponenciação da teoria dos tipos, dado o tipo a → b(ou b^a), o que significa ter o tipo logb(c)ou o tipo a√c?

Faz sentido estender logaritmos e raízes a tipos?

Em caso afirmativo, houve algum trabalho nessa área e quais são algumas boas orientações sobre como compreender as repercussões?

Tentei procurar informações sobre isso via lógica, esperando que a correspondência de Curry-Howard pudesse me ajudar, mas sem sucesso.

Um tipo tem um logaritmo de base de X de P exactamente quando C ≅ P → X . Isto é, C pode ser visto como um recipiente de X elementos em posições dadas por P . Na verdade, é uma questão de pedir para que poder P devemos levantar X para obter C .$C$$X$$P$$C \cong P\to X$$C$$X$$P$$P$$X$$C$

Faz sentido trabalhar com onde F é um functor, sempre que o logaritmo existir, o que significa l o $\mathop{log}F$$F$ . Observe que se$\mathop{log}\!_X(F\:X)$ , então nós certamente temos$F\:X\cong \mathop{log}F\to X$ , então o contêiner não nos diz nada de interessante além de seus elementos: os contêineres com uma escolha de formas não possuem logaritmos.$F\:1\cong 1$

Leis familiares de logaritmos fazem sentido quando você pensa em termos de conjuntos de posições

$$\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}$$

Também ganhamos onde Z = l o $\mathop{log}\!_X(\nu Y. T) = \mu Z. \mathop{log}\!_X T$ sob o fichário. Ou seja, ocaminhopara cada elemento em alguns codados é definido indutivamente pela iteração do logaritmo. Por exemplo,$Z=\mathop{log}\!_XY$

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

Dado que a derivada nos diz o tipo em contextos de um buraco e o logaritmo nos indica posições, devemos esperar uma conexão e, de fato,

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

Onde não há escolha de forma, uma posição é igual a um contexto de um orifício com os elementos apagados. De maneira mais geral, sempre representa a escolha de umaforma F junto com uma posição do elemento nessa forma.$\partial F\:1$$F$

Receio ter menos a dizer sobre raízes, mas é possível partir de uma definição semelhante e seguir o nariz. Para mais usos de logaritmos de tipos, consulte "Funções de memorando de Ralf Hinze, politipicamente!". Tenho que correr ...

Não conheço nenhum trabalho que persiga essa linha, mas alguns instantes pensei nela me levou a essa hipótese: a "raiz" do tipo exponencial não seria apenas o codomain e o "logaritmo" da exponencial apenas o domínio?