Custom opaque operator with custom axioms?

Question

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...)

Answer 1

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).

Answer 2

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}
]