Condition within `With` and other scoping environments is disregarded

[aravindh-krishnamoorthy]

Description

Wolfram language reference for Condition states that a condition within the Module, Block, and With statements:

lhs:=Module[{vars},rhs/;test]

applies to the lhs, i.e., it's added as a condition to the lhs. Presently, the condition is not added to the lhs in Mathics. See also the additional qualification in Additional context.

How to Reproduce

Mathics:

In[4]:= Clear[f]
Out[4]= None
In[5]:= f[x_] := With[{}, x /; x != 0]
Out[5]= None
In[6]:= f[0]
Out[6]= 0 /; 0 ≠ 0

and Mathematica:

>> Clear[f];
>> f[x_] := With[{}, x /; x != 0]
>> f[0]
f[0]

Output Given

0 /; 0 ≠ 0

Expected behavior

f[0]

Your Environment

Mathics 7.0.1dev0
on CPython 3.11.10 | packaged by conda-forge | (main, Oct 16 2024, 01:27:36) [GCC 13.3.0]
using SymPy 1.13.3, mpmath 1.3.0, numpy 2.1.3, cython Not installed

Workarounds

This workaround returns Indeterminate when the condition is false. Also, it only works when Condition is the only statement within the With block. It's a bad hack, but works for Rubi for now.

Unprotect[With]; 
With[vars_, Verbatim[Condition][expr_, wcond_]] := Condition[With[vars, expr], With[vars, wcond]]; 
With[vars_, Verbatim[Condition][expr_, wcond_]] := Condition[Indeterminate, Not[With[vars, wcond]]]; 
Protect[With]; 

Priority

Medium; results in Indeterminate results when a rule is picked, but eventually the condition within With is false.

Additional context

Note that the condition is considered for lhs only if it's a part of the last statement, as shown below for Mathematica $14.1.0$.

>> Clear[x];
>> Clear[f];
>> f[x_] := With[{}, x /; x != 0; x + 1]
>> f[0]
1

[mmatera]

The behavior of With, Module and Block in evaluation seems to be kind of special: When f[0] is evaluated, (according to the standard evaluation sequence), first the rule f[x_]:> With[{}, x /; x != 0] is applied. Then, the builtin rule is applied to With[{}, 0 /; 0 != 0] -> With.eval(...) which finally fails. Following this sequence, the result of f[0] would be With[{}, 0 /; 0 != 0] . So, rules with With & friends should be handled in a different way, I guess..

[aravindh-krishnamoorthy]

The behavior of With, Module and Block in evaluation seems to be kind of special: When f[0] is evaluated, (according to the standard evaluation sequence), first the rule f[x_]:> With[{}, x /; x != 0] is applied. Then, the builtin rule is applied to With[{}, 0 /; 0 != 0] -> With.eval(...) which finally fails. Following this sequence, the result of f[0] would be With[{}, 0 /; 0 != 0] . So, rules with With & friends should be handled in a different way, I guess..

Absolutely! https://github.com/corywalker/expreduce also has special handling for these.

To complicate things further, when compound statements are present within With, this special handling seems to happen only when the last statement has a condition. Such behaviour is not clearly specified and so is a MMA quirk.

[mmatera]

This discussion seems to be related: https://stackoverflow.com/questions/5866016/question-on-condition

[rocky]

This discussion seems to be related: https://stackoverflow.com/questions/5866016/question-on-condition

I've looked at this, and although things are complicated, there is one silver lining.

With respect to this part:

because Mathematica allows top-level manipulations through attributes and things like Evaluate, scoping constructs are not as black-box as they may seem - we may change the bindings by forcing the variable declarations, or the body, or both, to evaluate before the binding happens - for example, by removing some of the Hold* - attributes.

If this isn't black box, this means that an implementation can be done, and I think should be done following user-level constructs, at least to start out with, instead obliviously hacking at the Python object level by inventing new attributes on Python objects.

Also, the StackOverflow discusion shows how we can ensure we match behavior, such as by using Trace.

In the future, I will make more of an effort to try to match that evaluation behavior. I think we will have more details and more convenient ways to see what's going on, but there will be a way to match show Mathematica Trace behavior and we can try to match that better in those cases where our evaluation is not conforming.

[mmatera]

@rocky, I am not fully convinced that the proposal on https://stackoverflow.com/questions/5866016/question-on-condition is the right implementation. In any case, I think that this topic worth to be included in FUTURE.rst

[rocky]

@rocky, I am not fully convinced that the proposal on https://stackoverflow.com/questions/5866016/question-on-condition is the right implementation. In any case, I think that this topic worth to be included in FUTURE.rst

@mmatera See 535b74e . If this is not sufficient, feel free to modify.

[rocky]

@rocky, I am not fully convinced that the proposal on https://stackoverflow.com/questions/5866016/question-on-condition is the right implementation

It's not so much about the implementation but what is user-visible, and how one should think about and discuss this. The discussion is on scoping concepts and HOLD* attributes of a function. The correspondence to these ideas, like scoping, is a bit opaque in our code. Instead, I am seeing setting a Python attribute on a Symbol, which (for good reason) is immutable.