Exponential relationships/identities

[DroneBetter]

I made this diagram a while ago, with the notation from this 3Blue1Brown video (I don't like the other proposals in the introduction but thought this main part quite nice), we ought to add these (and their converses, for those that don't reduce the number of parameters).

I hereby decree (in my infinite wisdom) that log should be expressed with its base as its second parameter, behaving like Python and defaulting to the natural logarithm if not specified.
Note that WolframAlpha has a root function but Python doesn't, should we implement one or use root(a,b)=a**(1/b)? (All here will be in terms of the latter, I think it's a redundant convention that only makes things too complicated.)
Hereafter are the relationships in Dλ syntax (sorry if any are insultingly trivial, it is intended to be an exhaustive checklist (and you may find yourself surprised by a few)).
The six inverse relationships explained in the video are:

['log',['**',a,b],a]=b
['**',a,['log',b,a]]=b
['log',a,['**',a,['/',1,b]]]=b
['**',a,['/',1,['log',a,b]]]=b
['**',['**',b,['/',1,a]],a]=b
['**',['**',b,a],['/',1,a]]=b

More generally,

['log',['**',a,b],c]=['*',b,['log',a,c]]
['**',c,['log',b,a]]=['**',c,['/',1,['log',b,a]]]=['**',b,['log',c,a]]=['**',b,['/',1,['log',a,c]]]
['log',c,['**',a,['/',1,b]]]=['*',b,['log',c,a]]
['**',['**',b,['/',1,a]],c]=['**',['**',b,c],['/',1,a]]=['**',b,['/',c,a]]

In the second one with the four equivalent forms, WolframAlpha doesn't recognise anything across the second equals sign, but it is true for positive b and c (a can be negative), perhaps we should add the abs function for this.
The composition ones (converting equations of two calls of a function with one input fixed, in terms of lower-order arithmetic functions on the outputs, to a single call with arithmetic on the input):

['*',['**',a,b],['**',c,b]]=['**',['*',a,c],b]
['*',['**',a,['/',1,b]],['**',c,['/',1,b]]]=['**',['*',a,c],['/',1,b]]

['*',['**',b,a],['**',b,c]]=['**',b,['+',a,c]]
['+',['log',a,b],['log',c,b]]=['log',['*',a,c],b]

['*',['**',b,['/',1,a]],['**',b,['/',1,c]]]=['**',b,['+',['/',1,a],['/',1,c]]]
['/',1,['+',['/',1,['log',b,a]],['/',1,['log',b,c]]]]=['log',b,['*',a,c]]

Nesting of the self (only works for exponentiation)

['**',['**',a,b],c]=['**',a,['*',b,c]]
['**',['**',a,['/',1,b],['/',1,c]]]=['**',a,['/',1,['*',b,c]]]

Again, roots have no special properties that don't follow from (and can't be implemented as) exponentiation ones.

['log',['**',a,b],c]=['log',a,['**',c,['/',1,b]]]=['*',['log',a,c],b]
['log',['**',a,['/',1,b]],c]=['log',a,['**',c,b]]=['/',['log',a,c],b]

And finally, the logarithm identities

['/',['log',b,a],['log',b,c]]=['log',['**',b,['/',1,['log',b,c]]],a]=['log',['**',b,['log',c,b]],a]=['log',c,a]
['*',['log',c,b],['log',a,c]]=['log',['**',c,['log',a,c]],b]=['log',a,b]
['/',['log',a,b],['log',c,b]]=['log',['**',a,['/',1,['log',c,b]]],b]=['log',['**',a,['log',b,c]],b]=['log',['**',b,['log',a,c]],b]=['log',a,c]

(with a more concise (or at least, less nested) proof of the last one that relies on the use of the identity only true for positive values from earlier (I happened to know this one (though not its proof) much earlier than most of the others, because it is necessary to define logarithms with bases other than e and 10 in Scratch :-))
Now we must only find the minimal set of transformations that spans all of these identities.

During the discussion over this, I also realised that it would be a great deal easier if / were made unary, with the numerator always being 1 (and converted to this form in much the same way as subtraction is to addition of unary negation), so that things won't have to be implemented twice, so I think I will.

[DroneBetter]

I have done some thinking and think these actions will satisfy them all, for now

['log',a,a]=1 #0
['/',['log',b,a]]=['log',a,b] #1
['log',['**',a,b],c]=['*',['log',a,c],b] #2
['**',a,['log',b,a]]=b #3 (special case, see below)
['log',a,['**',c,b]]=['log',['**',a,['/',b]],c] #4
['log',['**',c,b],a]=['log',c,['**',a,['/',b]]] #5 (converse of 4)

These one aren't generally applicable to complex numbers

['**',['**',a,b],c]=['**',a,['*',b,c]] #6
['**',c,['log',b,a]]=['**',b,['log',c,a]] #due to ['**',e,['*',['log',c],['*',['log',b],['/',['log',a]]]]] #7

(consider (i**i)**5 != (i**5)**i), 6 will check that b and c are real and 7 that they're positive (while it is decided what to do about equations that require considering complex numbers separately).
Here are the applications of transformations necessary for it to prove each of the six identities at the beginning

['log',['**',a,b],a]=b #2, 0, multiplicative identity
['**',a,['log',b,a]]=b #3 alone
['log',a,['**',a,['/',b]]]=b #4, 2, 0, multiplicative identity
['**',a,['/',['log',a,b]]]=b #1, 3
['**',['**',b,['/',a]],a]=b #6, multiplicative identity
['**',['**',b,a],['/',a]]=b #6, multiplicative identity

And of the six relationships, being that roots won't be implemented separately, we must only implement three

['*',['**',a,b],['**',c,b]]=['**',['*',a,c],b] #8, will be implemented directly (extend distributivity to work based on pairs)
['*',['**',a,['/',b]],['**',c,['/',b]]]=['**',['*',a,c],['/',b]] #8

['*',['**',b,a],['**',b,c]]=['**',b,['+',a,c]] #9
['+',['log',a,b],['log',c,b]]=['log',['*',a,c],b] #10

['*',['**',b,['/',a]],['**',b,['/',c]]]=['**',b,['+',['/',a],['/',c]]] #9
['/',['+',['/',['log',b,a]],['/',['log',b,c]]]]=['log',b,['*',a,c]] #1 on both, 10, 1 again

nestings

['**',['**',a,b],c]=['**',a,['*',b,c]] #11
['**',['**',a,['/',b],['/',c]]]=['**',a,['/',['*',b,c]]] #11

the two others

['log',['**',a,b],c]=['log',a,['**',c,['/',b]]]=['*',['log',a,c],b] #5 and 2 respectively
['log',['**',a,['/',b]],c]=['log',a,['**',c,b]]=['/',['log',a,c],b] #also 5 and 2

and finally, the logarithm ones

['*',['log',b,a],['/',['log',b,c]]]=['log',['**',b,['/',['log',b,c]]],a]=['log',['**',b,['log',c,b]],a]=['log',c,a] #2's inverse (not listed here prior), 1, 3
['*',['log',c,b],['log',a,c]]=['log',['**',c,['log',a,c]],b]=['log',a,b] #2's inverse, 3
['*',['log',a,b],['/',['log',c,b]]]=['log',['**',a,['/',['log',c,b]]],b]=['log',['**',a,['log',b,c]],b]=['log',['**',b,['log',a,c]],b]=['log',a,c] #2's inverse, 1, 7, 2, 0

hmm perhaps the last one should be implemented directly (to avoid depending on 7)
We could also implement unary ln, perhaps, that would make algebraic manipulation of logarithms trivial.