# Custom opaque operator with custom axioms?

Is there any way to define a custom opaque operator/function in Mathematica that satisfies custom axioms, so that the Mathematica engine can perform simplifications using those axioms?

For example, say I want to define f such that f[Times[a,b]] evaluates to Times[f[a],b], and subsequently I want to be able to Assert[f[Times[a,b]] == Times[f[a],b]].

Can Mathematica do this?

(All the answers I see so far on custom operators on this site seem to be focusing on the notation/rendering rather than the axiomatic rules...)

• You'll usually want to use UpSetDelayed[] or TagSetDelayed[] for this; I prefer the latter: f /: f[Times[a_, b_]] := Times[f[a], b] Apr 10, 2017 at 3:36
• @J.M.: Oooh, seems like that's what I need, let me give that a try, thanks! Apr 10, 2017 at 3:53
• @Mehrdad Keep in mind that this tells the system to immediately transform f[a b] to f[a] b. It does not tell it how to go from f[a] b to f[a b], and Simplify will not be able to use these identities. Apr 10, 2017 at 8:15

No, unfortunately, Mathematica cannot do this automatically with a general set of axioms. There are some things you can do that work in specific cases only.

You can create definitions to control how f[x] evaluates, but evaluation is one-way only.

As J.M. said, you can define

f /: f[Times[a_, b_]] := Times[f[a], b]


then

f[x y]
(* y f[x] *)


But this is just a one-way evaluation rule that does not care about the mathematical meaning of this formula. Mathematica will not be able to transform y f[x] back to f[x y] in functions like Simplify to prove more complex identities.

It is not possible to create rules that Refine/Simplify/etc. will be able to use automatically. [Correction: There is the TransformationFunctions option of Simplify. I do not know how far you can go with it. Let us know!]

You can give Assumptions to Simplify, if the identities you want to use refer to simple complex variables. For more complicated situations, such as identities for functions, or mathematical objects that are not numbers (e.g. vectors, matrices, or something in non-commutative algebra), this is not possible. You would need to implement your own simplification functions (which is probably not trivial to do).

You are misusing Assert here. It is not for symbolic computation. It is for programming and debugging (a rough analogue of assert in C).

• I see, thanks! And yeah I know what assert is, I was just trying to say I want those to be seen as equivalent, you got what I meant. Apr 10, 2017 at 10:36
• @Mehrdad Well, it will work when you can construct a canonical form with one-way evaluations only. Apr 10, 2017 at 10:52
• Yes, I understand, thanks. Apr 10, 2017 at 10:53
• @Mehrdad See my update. There is TransformationFunctions. At this point, this answer feels so inaccurate that I am tempted to delete it. But at the same time, I have the feeling that what you are asking is really not easy to do in a general and useful way. I would prefer to just state those axioms and leave the rest up to Mathematica. It is not going to be that simple. But could it be done at least in principle? Apr 10, 2017 at 11:02
• @Mehrdad The thing is that if I told you to "just use TagSet and TransformationFunctions" then I would create the impression that it is a simple matter to work with such axioms ... I don't think it is. Apr 10, 2017 at 11:03

Let's start with some example test expression that we'll try to simplify:

f // ClearAll
expr = f[a b]^3/((f[a c] + c f[a]) f[b])


# Assumptions

One could try to give assumptions to simplification functions, but only some of expressions used in assumptions accept patterns e.g. Element, equations and inequalities don't, so one needs to explicitly use assumptions with all relevant literal arguments of f that are in expression, or could potentially appear there during simplifications. Even then assumptions will work only in simplest cases:

f // ClearAll
Simplify[expr, f[a b] == f[a] b && f[a c] == f[a] c]
(* f[a b]^3/(2 f[b] f[a c]) *)


# Canonical Form

If there exists preferred canonical form of an operator we can try to assign some ...Values to it. Then Mathematica will automatically "simplify" expressions involving this operator to its canonical form.

For example from OP we can assign DownValues to f:

f // ClearAll
f[x_ y_] := f[x] y

expr
(* (b^3 f[a]^2)/(2 c f[b]) *)


Note that for this toy example, due to Attributes of Times function, for any expression x, f[x] is equivalent to f[1 x] which according to property of f is equivalent to f[1] x, so this particular operator is just multiplication by a constant f[1], so f[x : Except@1] := f[1] x would be most obvious definition, but that's not relevant for general case.

If we prefer canonical form to be f with product inside we could try to assign UpValues to f:

f // ClearAll
f /: f[x_] y_ := f[x y]


But above definition will not apply if f[...] is inside Power expression:

expr
(* f[a b]^3/(f[b] f[2 a c]) *)
% // FullForm
(* Times[Power[f[b],-1],Power[f[Times[a,b]],3],Power[f[Times[2,a,c]],-1]] *)


We can't assign UpValues to f that would cover Times[Power[f[...], ...], ...] because f is to deep in this expression. One could Unprotect and redefine Times, but that's, in general, not advised. Other alternative is to define separate function that will convert expressions involving f.

# Transformation Functions

Most general way of "adding axioms" is to define transformation functions, i.e. functions that accept arbitrary expression and evaluate to expression that is mathematically equivalent, according to our "axioms", but in different form. For example from OP we could define:

f // ClearAll
fFactorOut = # /. f[x_ y_] :> f[x] y &;
fFactorIn = Replace[#, (f@x_)^m_. y_^n_. :> f[x y]^m y^(n - m), {0, Infinity}] &;


We can use transformation functions directly:

expr // fFactorOut
(* (b^3 f[a]^2)/(2 c f[b]) *)
expr // fFactorIn
(* f[a b]^3/(2 f[b] f[a c]) *)


or pass them to (Full)Simplify:

Simplify[expr, TransformationFunctions -> {Automatic, fFactorOut}]
(* (b^3 f[a]^2)/(2 c f[b]) *)
Simplify[expr, TransformationFunctions -> {Automatic, fFactorIn}]
(* f[a b]^3/f[f[2 a b c]] *)
Simplify[expr, TransformationFunctions -> {Automatic, fFactorIn, fFactorOut}]
(* (b^3 f[a]^2)/(2 f[b c]) *)


If we want simplification functions to always use our transformation functions we can set options globally:

SetOptions[{Simplify, FullSimplify},
TransformationFunctions -> {Automatic, fFactorIn, fFactorOut}
]