2
$\begingroup$

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.

\begin{equation} \sqrt[a] {b^a} = b \end{equation} \begin{equation} \log_{b} {b^a} = a \end{equation}

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?

$\endgroup$
6
  • $\begingroup$ 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... $\endgroup$
    – montokapro
    Commented Jul 17, 2022 at 5:41
  • 1
    $\begingroup$ What you call "this conjecture" is unclear to me. Could you state it explicitly ? $\endgroup$
    – user16034
    Commented Mar 23, 2023 at 8:10
  • 1
    $\begingroup$ I don't think that an exponential type is related to the exponential function (except for cardinality issues). What would a "root type" be ? $\endgroup$
    – user16034
    Commented Mar 23, 2023 at 8:22
  • $\begingroup$ 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. $\endgroup$
    – montokapro
    Commented Mar 25, 2023 at 3:02
  • $\begingroup$ My conjecture is that the "root" describes the cardinality of function application in the same way that an "exponential" describes the cardinality of functions. $\endgroup$
    – montokapro
    Commented Mar 25, 2023 at 3:02

1 Answer 1

0
$\begingroup$

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.

$\endgroup$
3
  • $\begingroup$ 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. $\endgroup$
    – montokapro
    Commented Jun 25, 2022 at 22:09
  • 1
    $\begingroup$ I don't quite get how this relates to booleans. Can you please elaborate on that? $\endgroup$
    – nir shahar
    Commented Jun 26, 2022 at 7:29
  • $\begingroup$ 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. $\endgroup$
    – montokapro
    Commented Jun 26, 2022 at 16:13

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

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