[fricas-devel] Defining a rewrite rule when calculation is failing

[Slawomir Kolodynski]

I am trying to figure out a way to tell FriCAS that
limit(erf(sqrt(c)*x),x=%plusInfinity) is 1 (say, I know that c>0).
To do that I define a rule:

limerf := rule limit(erf(sqrt(c)*x),x=%plusInfinity) == 1

However, when I try to apply the rule:

limerf(limit(erf(sqrt(c)*x),x=%plusInfinity))

I get

Cannot find a definition or applicable library operation named
limerf with argument type(s)
failed

It looks like FriCAS first tries to evaluate the argument of the rule (and
gets "failed"), then tries to match the rule pattern to the result.
Is there a way to prevent the rule to evaluate its argument before pattern
matching? Or I am doing something wrong here?

Thanks,

Slawomir

[Waldek Hebisch]

Post by Slawomir Kolodynski
I am trying to figure out a way to tell FriCAS that
limit(erf(sqrt(c)*x),x=%plusInfinity) is 1 (say, I know that c>0).
limerf := rule limit(erf(sqrt(c)*x),x=%plusInfinity) == 1
limerf(limit(erf(sqrt(c)*x),x=%plusInfinity))
I get
Cannot find a definition or applicable library operation named
limerf with argument type(s)
failed
It looks like FriCAS first tries to evaluate the argument of the rule (and
gets "failed"), then tries to match the rule pattern to the result.
Is there a way to prevent the rule to evaluate its argument before pattern
matching? Or I am doing something wrong here?

In FriCAS 'limit' is an operation, not an expression. The
same with '=' (which produces equation, not an expression).
There is also problem with types: '%plusInfinity' is not an
expression.

To get something in your spirit one needs to work with expressions:

lim := operator 'lim

limerf := rule lim(erf(sqrt(c)*x),infinity) == 1


OTOH if purpose is stricly to compute limit, than you can do

e1 := eval(erf(sqrt(c)*x), sqrt(c) = d^2)
limit(e1, x=%plusInfinity)

If you need to undo the substitution in part of expression
you can do more complicated thing:

(1) -> pos := operator 'pos

(1) pos
Type: BasicOperator
(2) -> e1 := eval(erf(sqrt(c)*x), sqrt(c) = pos(sqrt(c))^2)

+-+ 2
(2) erf(x pos(\|c ) )
Type: Expression(Integer)
(3) -> limit(e1, x=%plusInfinity)

(3) 1
Type: Union(OrderedCompletion(Expression(Integer)),...)
(4) -> eI := Expression(Integer)

(4) Expression(Integer)
Type: Type
(5) -> eval(e1, [name(pos)], [2], [(x : eI) : eI +-> x])

+-+
(5) erf(x\|c )
Type: Expression(Integer)

[Slawomir Kolodynski]

Thanks for the solution. It works for me.

Post by Waldek Hebisch
eval(e1, [name(pos)], [2], [(x : eI) : eI +-> x])

For the interested readers of this thread here is the documentation of the
last eval call:

eval: (%, List Symbol, List NonNegativeInteger, List % -> %) -> % if R has
Ring
eval(x, [s1, ..., sm], [n1, ..., nm], [f1, ..., fm]) replaces every
si(a)^ni in x by fi(a) for any a.

Thanks.

Slawomir