Pardon my curiosity, but I’m wondering how Wolfram calculates
FullSimplify[x == q Quotient[x, q] + Mod[x, q]].
I tried Trace and the TraceOriginal->True option, but I still don’t get it. Does Wolfram know it’s True, or does it apply some transformation rules to get True?
Using Reduce I get the message that it is using FunctionExpand:
Reduce[x == q Quotient[x, q] + Mod[x, q]]
In fact FunctionExpand translates the expression into Floor objects:
FunctionExpand[q Quotient[x, q]]
FunctionExpand[Mod[x, q]]
This behavior is documented in the
“Properties & Relations” section of Quotient—Wolfram Documentation (3rd example therein).
I tried that too, but I didn’t detect those transformations. How did you find them?
Rather, from the examples given there, we should conclude that the result is derived from theory rather than computation.
Yes, symbolic computation, which is what FullSimplify[] carries out, is done in part via equivalence transformations that are programmed into the system. From a purely mathematical viewpoint, one calls these transformations identities or even theorems. One presumes they are based on how the functions are defined and computed in WL (when there exists more than one definition out in the world). Symbolic computation is inescapably based on theory. I don’t think there is another way to perform this computation.
In WL, the transformations are often coded as replacement rules. There is a large table of them SimplifyDump`$FSTab[...]. Internally, FullSimplify[] does more or less what @Gianluca Gorni shows:
Block[{Internal`FunctionExpand`$Debug = True},
FullSimplify[x == q Quotient[x, q] + Mod[x, q]]
]
Then exploring which rules cause the transformations, we find these two:
SimplifyDump`$FSTab[540]
Quotient[x, q] /. %
(*
Quotient[SimplifyDump`x_, SimplifyDump`y_] :>
Floor[SimplifyDump`x/SimplifyDump`y]
Floor[x/q]
*)
SimplifyDump`$FSTab[680]
Mod[x, q] /. %
(*
Mod[SimplifyDump`x_, SimplifyDump`y_] :>
SimplifyDump`x - SimplifyDump`y Floor[SimplifyDump`x/SimplifyDump`y]
x - q Floor[x/q]
*)
Got it. Thanks!!!
I mistakenly thought that Wolfram computes in much the same way I write a sequence of commands, just along all paths at once, and selects the ones that get closest to the result. It turns out that applying a built-in function is not so easy to detect, much less see the entire computation process.