2
$\begingroup$

I'm having troubles with this:

test1[forAll[t,x_]]:=x
test2[ForAll[t,x_]]:=x

While syntactically exact, test1 works and test2 does not:

?test1
(* test1[forAll[t,x_]]:=x *)

?test2
(* test2[x_]:=x *)

Why doesn't ?test2 output test2[ForAll[t,x_]]:=x?

Edit 2

For anyone interested - for yet unknown reasons - this and only this works as expected:

test3[ForAll[t,t_]]:=t

Edit 3

The legit working solution to non-standard evaluation traps like this is to use unambiguous pattern matching syntax that does not provide any hints to the system that this can be evaluated:

test2[(f:ForAll)[t,x_]]:=x
$\endgroup$
  • 4
    $\begingroup$ Thanks for the edit. You need HoldFirst or similar attribute, otherwise it is the same as defining f[1+1]:=whatever. $\endgroup$ – Kuba Jun 27 '17 at 19:48
  • $\begingroup$ @Kuba, I do not want HoldFirst for this method. I need it without HoldFirst $\endgroup$ – grandrew Jun 27 '17 at 19:51
  • $\begingroup$ @Kuba, btw I just tested test3[a_+b_]:=a and it actually does work: ?test3 (* => test3[a_+b_]:=a *) $\endgroup$ – grandrew Jun 27 '17 at 20:09
  • 3
    $\begingroup$ Because a_+b_ does not evaluate further while ForAll[t,x_] does, to x_. $\endgroup$ – Kuba Jun 27 '17 at 20:12
  • 2
    $\begingroup$ I'm not sure why you think this is a bug. ForAll has no Options (specifically HoldFirst), and I think by default, it takes the symbol that's in the first argument and looks for it in the second argument. Compare ForAll[x_, x_^2] with ForAll[x_, y_^2]. The second evaluates to y_^2 because it has no x_ in it. $\endgroup$ – march Jun 27 '17 at 20:32
5
$\begingroup$

First of all, though SetDelayed (:=) has HoldAll attribute, it still evaluates its 1st argument in this case, this behavior has been discussed in this post. To be specific, when test2 is defined, the argument ForAll[t, x_] will be evaluated.

Now the question becomes

Why ForAll[t, x_] evaluates to x_?

and this has been explained in the Scope of the document of ForAll:

If the expression does not explicitly contain a variable, ForAll simplifies automatically:

ForAll[x, y == 0] 
(* y == 0 *)

In your case, x_ doesn't explicitly contain t, and it's automatically simplified, while t_ explicitly contain t so it's not. (Notice the FullForm of t_ is Pattern[t, Blank[]] i.e. a function with 2 arguments whose 1st agrument is an explicit t. )

To get the desired function definition, you can make use of Unevaluated:

ClearAll@test2    
test2[Unevaluated@ForAll[t, x_]] := x
DownValues@test2
(* {HoldPattern[test2[ForAll[t, x_]]] :> x} *)

test2[ForAll[t, t + t^2]]
(* t + t^2 *)

But notice this function still won't work as expected if the ForAll[…] evaluates to something else, for example:

test2[ForAll[t, x]]
(* test2[x] *)

If you want it to evaluate to x, then Unevaluated again or as mentioned in the comment above, use HoldFirst:

test2[Unevaluated@ForAll[t, x]]
(* x *)
SetAttributes[test2, HoldFirst]
test2[ForAll[t, x]]
(* x *)
$\endgroup$
  • $\begingroup$ xzczd, thank you for detailed answer. Could you please elaborate on how does t_ explicitly contain t? I thought t_ is just a local pattern variable and does not explicitly state anything and could mean any expression when matched regardless of its name? $\endgroup$ – grandrew Jun 28 '17 at 7:39
  • $\begingroup$ Check my edit. If you're still confused, feel free to ask. $\endgroup$ – xzczd Jun 28 '17 at 9:20
  • $\begingroup$ many thanks! that makes a lot of sense and completes my understanding of how pattern matching is implemented on top of symbolic rules engine in MMA. Btw, the word "function" may add confusion and I am not sure if this is even correct for symbol Pattern (I doubt if it emits a Function in any scenario) $\endgroup$ – grandrew Jun 28 '17 at 12:42
  • $\begingroup$ I think it's OK to use the word "function" to name a non-atomic expression, even if it doesn't evaluate to anything else. In mathematics we'll simply call $f(x,y)$ a function even if we know nothing about the specific function relationship represented by $f$, right? $\endgroup$ – xzczd Jun 28 '17 at 13:15

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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