## Immediate vs. Delayed evaluation

Help
Bonny
2009-07-16
2012-11-20
• Bonny - 2009-07-16

I am using the rlqe command in the Redlog package for quantifier elimination. I want to store the quantifier-free expression as a function or procedure. For example, a procedure might look like:

procedure f(a,b,c);
rlqe ex({x,y}, a*x^2 + b*y + c = 0);

When I do

f(a,b,c);

the result is

b =/= 0 V (a = 0 /\ c = 0) V (ac <= 0 /\ a =/= 0)

I want to store this quantifier-free expression as a function or procedure, say g(a,b,c), so that when I want to evaluate f(u,v,w), I can call g(u,v,w) which is already quantifier-free.

• Bonny - 2009-07-16

[Sorry for the incomplete message above.]

How can I write a function or procedure to store the quantifier-free expression equivalent to a given quantified expression?

• Bonny - 2009-07-17

I am not sure I explained my problem clearly enough. Let me try once more.

I am used to working in Mathematica, so I will use it for my explanation. In Mathematica, one can declare a function in two ways:

f[a_, b_, c_] := Resolve[ Exists[ {x,y}, a*x^2 + b*y + c == 0 ], Reals ];

f[a_, b_, c_] = Resolve[ Exists[ {x,y}, a*x^2 + b*y + c == 0 ], Reals ];

where Resolve is a function for quantifier elimination (QE) similar to rlqe in Reduce.

In the first declaration, Mathematica will do delayed evaluation (:=), i.e. if I want to compute f[1, 2, 3], it will call the function Resolve to evaluate Resolve[ Exists[ {x,y}, 1*x^2 + 2*y + 3 == 0 ], Reals ].

In the latter declaration, Mathematica will do immediate evaluation (=), i.e. if I want to compute f[1, 2, 3], it will not call Resolve but will evaluate

2 =/= 0 V (1 = 0 /\ 3 = 0) V (1*3 <= 0 /\ 1 =/= 0)

In the latter case, the evaluation of Resolve[ Exists[ {x,y}, a*x^2 + b*y + c == 0 ], Reals ] has already been done as soon as the declaration was made (i.e. immediate evaluation) and now

f[a_, b_, c_] := b =/= 0 V (a = 0 /\ c = 0) V (ac <= 0 /\ a =/= 0)

That is, as a result of immediate evaluation, f[a_, b_, c_] stores the equivalent quantifier-free expression as compared to Resolve[quantified expression, domain].

The benefit of immediate evaluation is, for time consuming computations like QE, one can do the time consuming computation in symbolic form (as opposed to numerical form) for once and store the result. When in future, the quantified expression needs to be evaluated for some symbolic and/or numerical values, the time consuming QE process can be completely bypassed thereby producing the correct result in a very short time. Storing the ultimate result in symbolic form will be useful not only for QE but for any time consuming computation (e.g. certain simplifications). Since we are doing the time consuming computation for once, we can dedicate significant time and memory for it.

I would like to know how to do immediate evaluation in Reduce. It will suffice if I can somehow store the equivalent quantifier-free expression as a function or procedure so that I can bypass the QE process after the first time.

Feel free to ask questions for more clarification. Look forward to your help.

Thanks,
Bonny

• Thomas Sturm - 2009-07-17

I presume that you are programming in the algebraic mode of Reduce.

Try the following:

rlset reals;

lisp procedure formimmediate(s,a,m);

put('immediate,'formfn,'formimmediate);

procedure f(a);
immediate rlqe ex(x,a*x+b=0);

This causes the desired behaviour of f(a), which you can verify via

getd 'f;

Notice that this is an ad hoc solution, which might cause problems when you start mixing algebraic and symbolic mode code, use (s)macros, or similar advances things.

Thomas

• Bonny - 2009-07-21

After defining the procedure f(a), how do I compute f(1) for example? If I do

getd 'f(1);

I don't get any output.

Thanks,
Bonny

• Thomas Sturm - 2009-07-21

For calling the function sImply go

f(1);

The getd gives you the function definition as a lambda expression so that you can verify what you have actually defined. This is why I mentioned it.

Thomas

• Bonny - 2009-07-21

I did

procedure f(a, b, c);
immediate rlqe ex({x, y}, a*x^2 + b*y + c = 0);

procedure g(a, b, c);
rlqe ex({x, y}, a*x^2 + b*y + c = 0);

f(1,2,3);
0

g(1,2,3);
true

f(0,0,1);
<nothing>

g(0,0,1);
false

Is that how it should work? That is, it would output 0 when the solution is true and output nothing when the solution is false?

Thanks,
Bonny

• Thomas Sturm - 2009-07-21

Did you input the definition of immediate before using it? If so, please post your input file, which does not work.

Thomas

• Bonny - 2009-07-21

Sorry, I was wrong. When the solution is true, f returns t. When the solution is false, f returns nothing. I think that is the way it should be.

Here is my input file:

rlset ofsf;
lisp procedure formimmediate(s,a,m);
put('immediate,'formfn,'formimmediate);

procedure f(a, b, c);  immediate rlqe ex({x, y}, a*x^2 + b*y + c = 0);
procedure g(a, b, c); rlqe ex({x, y}, a*x^2 + b*y + c = 0);

f(1,2,3);
g(1,2,3);
f(0,0,1);
g(0,0,1);
end;

• Thomas Sturm - 2009-07-21

No, you are right! My formimmediate is too simple. I guess the "t" you see is essentially an evaluation of the resulting formula as an if-condition but not as a Redlog formula. I am going to fix this tomorrow morning (it's quite late here).

Thomas

• Thomas Sturm - 2009-07-22

OK, here's "immediate 2.0:"

lisp procedure formimmediate(s,vl,m);

You will now get:

7: f(1,2,3);

2 ≠ 0 ∨ (1 = 0 ∧ 3 = 0) ∨ (3 ≤ 0 ∧ 1 ≠ 0)

8: rlsimpl f(1,2,3);

true

Notice that it is natural that you need another rlsimpl when using f: rlqe generally simplifies at the end but with f in contrast to g you have got only the simplifications which are possible without the concrete values for the variables. Anyway, simplification is fast compared to QE.

Another caveat: immediate does not do any special parsing itself. So as with any Reduce function, if you go, e.g.,

immediate expr1+expr2;

immediate binds stronger than "+" and thus only refers to expr1. To include expr2, you have to go

immediate(expr1+expr2);

and to complete the picture

immediate expr1 + immediate expr 2;

would evaluate both expr1 and expr2 at definition time but not the "+".

Thomas

• Bonny - 2009-07-22

Thanks Thomas.

Here is my new input file:

rlset ofsf;

lisp procedure formimmediate(s,vl,m);
put('immediate,'formfn,'formimmediate);

procedure f(a, b, c); immediate rlqe ex({x, y}, a*x^2 + b*y + c = 0);
procedure g(a, b, c); rlqe ex({x, y}, a*x^2 + b*y + c = 0);

f(1,2,3);
g(1,2,3);
f(0,0,1);
g(0,0,1);
f(u,v,w);
g(u,v,w);

end;

I do get something very similar to what you said in your last post but not exactly the same. For e.g.,

f(1,2,3);

2 <> 0 or (1 = 0 and 3 = 0) or (3 <= 0 and 1 <> 0)2 <> 0 or (1 = 0 and 3 = 0) or (3 <= 0 and 1 <> 0)

g(1,2,3);

true

f(0,0,1);

0 <> 0 or (0 = 0 and 1 = 0) or (0 <= 0 and 0 <> 0)0 <> 0 or (0 = 0 and 1 = 0) or (0 <= 0 and 0 <> 0)

g(0,0,1);

false

f(u,v,w);

v <> 0 or (u = 0 and w = 0) or (u*w <= 0 and u <> 0)v <> 0 or (u = 0 and w = 0) or (u*w <= 0 and u <> 0)

g(u,v,w);

v <> 0 or (u = 0 and w = 0) or (u*w <= 0 and u <> 0)v <> 0 or (u = 0 and w = 0) or (u*w <= 0 and u <> 0)

Notice that part of the output is being written twice which I am not sure why.

Thanks again,
Bonny

• Thomas Sturm - 2009-07-22

The output looks correct except for the duplicate printing, which I cannot reproduce or explain. Notice that it also happens with g, where immediate is not involved at all.

Please try to reproduce this, and if you succeed, give me some details on which Reduce version you are using.

Thomas

• Bonny - 2009-07-22

I get the duplicate output printing even when I use an input file as simple as the following:

rlset ofsf;
procedure g(a,b,c); rlqe ex({x,y},a*x^2+b*y+c=0);
g(1,2,3);
g(0,0,1);
g(u,v,w);
end;

However, if I do not read from a file but type in each command, then the duplicate printing goes away. I am surprised!

I am using Reduce (Free CSL version), 14-Apr-09

Bonny

• Thomas Sturm - 2009-07-22

This is strange. Please zip or compress your input file, and email it to me as an attachment. There might be a problem with CR/LF.

I am going to mail you my version of this input file, which works.

I think the double quotes with load_package are not correct but it appears that they do not matter.

Thomas

• Bonny - 2009-07-22

I have emailed you my input file which is exactly the same as your input file. I get the same duplicate printing with your input file too.

Bonny