# Is the root function computationally equivalent to function application?

If a function type is representable by exponentiation, does it follow that function application is represented by the right inverse, roots? It would seem that roots consume a function's input to return the output, and logarithms consume a function's output to return the input.

$$$$\sqrt[a] {b^a} = b$$$$ $$$$\log_{b} {b^a} = a$$$$

I don't know of any mathematical notation that lets one flip the notation to represent application nicely, so I'll abuse some notation briefly to layout out some identities in a way that feels computationally intuitive to me.

• Exponent: (<- or ->)
• Root (right inverse): (<-o or o->)
• Logarithm (left inverse): (o<- or ->o)

Given this notation, function application seems to resemble:

(A -> B) <-o A = B (when f: A -> B, and a: A, then f(A): B)

Logarithms look like the following, perhaps representing ideas like looking up the index for an array element:

(A -> B) ->o B = B

Is this baseless conjecture, or is there research to support this?

• I've found a related question here: cstheory.stackexchange.com/questions/17006/… Indeed, logarithm types seem to be similar to what I described, but the verdict is still out for root types... Commented Jul 17, 2022 at 5:41
• What you call "this conjecture" is unclear to me. Could you state it explicitly ?
– user16034
Commented Mar 23, 2023 at 8:10
• I don't think that an exponential type is related to the exponential function (except for cardinality issues). What would a "root type" be ?
– user16034
Commented Mar 23, 2023 at 8:22
• Yes, I'm thinking in terms of cardinality here. Say I have a function that takes a boolean and returns a triple. There are 9 possible such functions. If I apply one of those functions to a boolean (by taking the square root), then I get a triple. Thus the actual application of the function to a value can be described by a root type (a right inverse), in the same way that quotient types and subtractive types have meaning in type theory literature as related to product types and sum types. Commented Mar 25, 2023 at 3:02
• My conjecture is that the "root" describes the cardinality of function application in the same way that an "exponential" describes the cardinality of functions. Commented Mar 25, 2023 at 3:02

This is the definition of root and logarithms.

And the usual notation for the inverse of a function $$f$$ is $$f^{-1}$$, which satisfies $$f^{-1}(f(x))=x$$ and $$f(f^{-1}(y))=y$$

$$\log_a(x)=f^{-1}(x)$$ where $$f(x)=a^x$$

$$\sqrt x=f^{-1}(x)$$ where $$f(x)=x^a$$.

Function composition, which is denoted by $$h=f\circ g$$, creates a new function $$h$$ which computes to be $$h(x)=f(g(x))$$. So the inverses, can also be defines as $$f\circ f^{-1}=f^{-1}\circ f=Id$$ where $$Id$$ is the identity function which gets an input $$x$$ and returns it unchanged.

• Thank you for this response! You've defined two functions f that compute an exponentiation, but I'm not sure this quite fits the idea of function types themselves as exponents: ie the function space Maybe[Bool] -> Bool has cardinality represented by the exponentiation of Bool ^ Maybe[Bool] such that 2^3 such possible functions exist. I'm interpreting your answer slightly differently. Commented Jun 25, 2022 at 22:09
• I don't quite get how this relates to booleans. Can you please elaborate on that? Commented Jun 26, 2022 at 7:29
• Boolean is an example datatype - it has two inhabitants (true, false). Maybe[Bool] has three inhabitants (none, some(true), some(false)). Thus, the number of possible functions with the type Maybe[Bool] -> Bool is 2^3 or 8, representable by the table [[F F F] [F F T] [F T F] [F T T] [T F F] [T F T] [T T F] [T T T]] where each entry represents the Bool output for each possible Maybe[Bool] input. Commented Jun 26, 2022 at 16:13