Take the 2-minute tour ×
Theoretical Computer Science Stack Exchange is a question and answer site for theoretical computer scientists and researchers in related fields. It's 100% free, no registration required.

I was recently reading The Two Dualities of Computation: Negative and Fractional Types. The paper expands on sum-types and product-types, giving semantics to the types a - b and a/b.

Unlike addition and multiplication, there are not one but two inverses of exponentiation, logarithms and rooting. If function types (a → b) are type-theoretic exponentiation, given the type a → b (or b^a) what does it mean to have the type logb(c) or the type a√c?

Does it make sense to extend logarithms and roots to types at all?

If so, has there been any work in this area, and what are some good directions on how to comprehend the repercussions?

I tried looking up information on this via logic, hoping the Curry-Howard correspondence could help me, but to no avail.

share|improve this question

2 Answers 2

up vote 33 down vote accepted

A type $C$ has a logarithm to base $X$ of $P$ exactly when $C \cong P\to X$. That is, $C$ can be seen as a container of $X$ elements in positions given by $P$. Indeed, it's a matter of asking to what power $P$ we must raise $X$ to obtain $C$.

It makes sense to work with $\mathop{log}F$ where $F$ is a functor, whenever the logarithm exists, meaning $\mathop{log}\!_X(F\:X)$. Note that if $F\:X\cong \mathop{log}F\to X$, then we certainly have $F\:1\cong 1$, so the container tells us nothing interesting other than its elements: containers with a choice of shapes do not have logarithms.

Familiar laws of logarithms make sense when you think in terms of position sets

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

We also gain $\mathop{log}\!_X(\nu Y. T) = \mu Z. \mathop{log}\!_X T$ where $Z=\mathop{log}\!_XY$ under the binder. That is, the path to each element in some codata is defined inductively by iterating the logarithm. E.g.,

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

Given that the derivative tells us the type in one-hole contexts and the logarithm tells us positions, we should expect a connection, and indeed

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

Where there is no choice of shape, a position is just the same as a one-hole context with the elements rubbed out. More generally, $\partial F\:1$ always represents the choice of an $F$ shape together with an element position within that shape.

I'm afraid I have less to say about roots, but one could start from a similar definition and follow one's nose. For more uses of logarithms of types, check Ralf Hinze's "Memo functions, polytypically!". Gotta run...

share|improve this answer
2  
The answer from Da Man himself. Welcome Conor! –  Andrej Bauer Mar 25 '13 at 15:17
    
Hmm, I am interested to see what root types are, as they would require types having imaginary numbers of inhabitants. Unless I am wrong. I will accept your answer, but if you have the time to elaborate on roots that would be much appreciated. –  efrey Mar 26 '13 at 1:56
    
Can this be related to the Taylor series of ln(1+x) somehow? –  yatima2975 Mar 26 '13 at 15:22
1  
With logarithms and exponentials, I wonder... what do we need to construct a Napier object? (e.g. the supposedly unique object e such that ∂e = e) –  Rhymoid Mar 29 '13 at 12:50

I don't know of any work that pursues this line, but a few moments thought about it led me to this hypothesis: wouldn't the "root" of the exponential type just be the codomain, and the "logarithm" of the exponential just the domain?

share|improve this answer
    
Right, so I think your intuition is good but your conclusion is off. The root operation and the logarithm operation are what you get when you "invert" the codomain or the domain respectively, not the (co)domain's themselves. The question is, what do we mean by invert and what is the binary type operation it produces? –  efrey Mar 24 '13 at 22:11
    
Not sure that's right. If I have $x^y$, the $y$th root is $x$ and the base $x$ logarithm is $y$. The inversion is of the operation, not the components. –  Marc Hamann Mar 24 '13 at 22:35
    
Sorry, I have not been totally clear in my terminology. I do not mean to ask "what is the root, what is the result of applying the logarithm function". I am wondering what the operation of rooting is. What the operation of finding the logarithm is. If is expenentiation, what is a two types under the root operation. What is two types under the logarithm operation. What I mean by "invert the argument" is something there is not time to explain here. I will clarify my question, thanks. –  efrey Mar 25 '13 at 5:33
    
The paper I linked provides a semantics for the type a - b and the type a / b. I am not concerned with the result of reducing the operations logarithm and root, but in understanding their semantics as binary type operators. –  efrey Mar 25 '13 at 5:50

Your Answer

 
discard

By posting your answer, you agree to the privacy policy and terms of service.

Not the answer you're looking for? Browse other questions tagged or ask your own question.