Edit detail for SandBoxSymbolic revision 24 of 35

Symbolic Integers

A simple form of symbolic computation using just Variable and Integer.

axiom
a:Union(Variable a,Integer)

axiom
b:Union(Variable b,Integer)

axiom
c:=a*3-b*2

(1)

axiom
p:UP(x,Integer):=x*2-7

(2)

axiom
pc := p c

(3)

axiom
f(x)==x^3-x^2+1

axiom
fb := f b

Compiling function f with type Variable b -> Polynomial Integer

(4)

axiom
a:=1

(5)

axiom
b:=-3

(6)

axiom
c

(7)

axiom
eval(pc,['a=a,'b=b])

(8)

axiom
eval(c,['a=a,'b=b])

(9)

axiom
eval(fb,['a=a,'b=b])

(10)

axiom
a:=3.14  -- not permitted!
   Cannot convert right-hand side of assignment
   3.14
      to an object of the type Union(Variable a,Integer) of the
      left-hand side.
a:='b    -- not permitted!

   Cannot convert right-hand side of assignment
   b
      to an object of the type Union(Variable a,Integer) of the
      left-hand side.

For more complex cases it is necessary to define a new domain of "indeterminants". These are symbols and unevaluated expressions that can be evaluated at a later time. This domain is modeled after InputForm? which provides all of the basic functionality.

spad
)abbrev domain INDET Indeterminant
++ Description:
++   Based on InputForm
Indeterminant():
  Join(SExpressionCategory(String,Symbol,Integer,DoubleFloat,OutputForm),
       ConvertibleTo SExpression) with
    eval: % -> Any
      ++ eval(f) passes f to the interpreter.
    binary   : (%, List %) -> %
      ++ \spad{binary(op, [a1,...,an])} returns the input form
      ++ corresponding to  \spad{a1 op a2 op ... op an}.
    function : (%, List Symbol, Symbol) -> %
      ++ \spad{function(code, [x1,...,xn], f)} returns the input form
      ++ corresponding to \spad{f(x1,...,xn) == code}.
    lambda   : (%, List Symbol) -> %
      ++ \spad{lambda(code, [x1,...,xn])} returns the input form
      ++ corresponding to \spad{(x1,...,xn) +-> code} if \spad{n > 1},
      ++ or to \spad{x1 +-> code} if \spad{n = 1}.
    "+"      : (%, %) -> %
      ++ \spad{a + b} returns the input form corresponding to \spad{a + b}.
    "-"      : (%, %) -> %
      ++ \spad{a - b} returns the input form corresponding to \spad{a - b}.
    "-"      : % -> %
      ++ \spad{-a} returns the input form corresponding to \spad{-a}.
    "*"      : (%, %) -> %
      ++ \spad{a * b} returns the input form corresponding to \spad{a * b}.
    "/"      : (%, %) -> %
      ++ \spad{a / b} returns the input form corresponding to \spad{a / b}.
    "**"     : (%, NonNegativeInteger) -> %
      ++ \spad{a ** b} returns the input form corresponding to \spad{a ** b}.
    "**"     : (%, Integer) -> %
      ++ \spad{a ** b} returns the input form corresponding to \spad{a ** b}.
    unparse  : % -> String
      ++ unparse(f) returns a string s such that the parser
      ++ would transform s to f.
      ++ Error: if f is not the parsed form of a string.
    declare  : List %   -> Symbol
      ++ declare(t) returns a name f such that f has been
      ++ declared to the interpreter to be of type t, but has
      ++ not been assigned a value yet.
      ++ Note: t should be created as \spad{devaluate(T)$Lisp} where T is the
      ++ actual type of f (this hack is required for the case where
      ++ T is a mapping type).
    compile  : (Symbol, List %) -> Symbol
      ++ \spad{compile(f, [t1,...,tn])} forces the interpreter to compile
      ++ the function f with signature \spad{(t1,...,tn) -> ?}.
      ++ returns the symbol f if successful.
      ++ Error: if f was not defined beforehand in the interpreter,
      ++ or if the ti's are not valid types, or if the compiler fails.
    coerce : Integer -> %
 == SExpression add
    Rep := SExpression
    mkProperOp: Symbol -> %
    strsym    : % -> String
    tuplify   : List Symbol -> %
    coerce(x:Integer):% == convert(x)
    coerce(x:%):OutputForm == expr x
    convert(x:%):SExpression == x pretend SExpression
    conv(ll : List %): % ==
      convert(ll pretend List SExpression)$SExpression pretend %
    lambda(f,l) == conv([convert("+->"::Symbol),tuplify l,f]$List(%))
    eval x ==
      v := interpret(x)$Lisp
      mkObj(unwrap(objVal(v)$Lisp)$Lisp, objMode(v)$Lisp)$Lisp
    convert(x:DoubleFloat):% ==
      convert(x)$Rep
    strsym s ==
      string? s => string s
      symbol? s => string symbol s
      error "strsym: form is neither a string or symbol"
    unparse x ==
      atom?(s:% := form2String(x)$Lisp) => strsym s
      concat [strsym a for a in destruct s]
    declare signature ==
      declare(name := new()$Symbol, signature)$Lisp
      name
    compile(name, types) ==
      symbol car cdr car
        selectLocalMms(mkProperOp name, convert(name)@%,
          types, nil$List(%))$Lisp
    mkProperOp name ==
      op := mkAtree(nme := convert(name)@%)$Lisp
      transferPropsToNode(nme, op)$Lisp
      convert op
    binary(op, args) ==
      (n := #args) < 2 => error "Need at least 2 arguments"
      n = 2 => convert([op, first args, last args]$List(%))
      convert([op, first args, binary(op, rest args)]$List(%))
    tuplify l ==
      empty? rest l => convert first l
      conv
        concat(convert("Tuple"::Symbol), [convert x for x in l]$List(%))
    function(f, l, name) ==
      nn := convert(new(1 + #l, convert(nil()$List(%)))$List(%))@%
      conv([convert("DEF"::Symbol), conv(cons(convert(name)@%,
                        [convert(x)@% for x in l])), nn, nn, f]$List(%))
    s1 + s2 ==
      conv [convert("+"::Symbol), s1, s2]$List(%)
    s1 - s2 ==
      conv [convert("-"::Symbol), s1, s2]$List(%)
    _-(s1) ==
      conv [convert("-"::Symbol), s1]$List(%)
    s1 * s2 ==
      conv [convert("*"::Symbol), s1, s2]$List(%)
    s1:% ** n:Integer ==
      conv [convert("**"::Symbol), s1, convert n]$List(%)
    s1:% ** n:NonNegativeInteger == s1 ** (n::Integer)
    s1 / s2 ==
      conv [convert("/"::Symbol), s1, s2]$List(%)

   Compiling FriCAS source code from file 
      /var/zope2/var/LatexWiki/7483143363411555740-25px002.spad using 
      old system compiler.
   INDET abbreviates domain Indeterminant 
------------------------------------------------------------------------
   initializing NRLIB INDET for Indeterminant 
   compiling into NRLIB INDET 
   compiling exported coerce : Integer -> $
Time: 0.04 SEC.

   compiling exported coerce : $ -> OutputForm
Time: 0 SEC.
   compiling exported convert : $ -> SExpression
      INDET;convert;$Se;3 is replaced by x 
Time: 0 SEC.
   compiling local conv : List $ -> $
Time: 0.10 SEC.
   compiling exported lambda : ($,List Symbol) -> $
Time: 0.02 SEC.
   compiling exported eval : $ -> Any
Time: 0 SEC.
   compiling exported convert : DoubleFloat -> $
Time: 0 SEC.
   compiling local strsym : $ -> String
Time: 0.01 SEC.
   compiling exported unparse : $ -> String
Time: 0.07 SEC.
   compiling exported declare : List $ -> Symbol
Time: 0 SEC.
   compiling exported compile : (Symbol,List $) -> Symbol
Time: 0.01 SEC.
   compiling local mkProperOp : Symbol -> $
Time: 0 SEC.
   compiling exported binary : ($,List $) -> $
Time: 0.04 SEC.
   compiling local tuplify : List Symbol -> $
Time: 0.08 SEC.
   compiling exported function : ($,List Symbol,Symbol) -> $
Time: 0.03 SEC.
   compiling exported + : ($,$) -> $
Time: 0.01 SEC.
   compiling exported - : ($,$) -> $
Time: 0 SEC.
   compiling exported - : $ -> $
Time: 0.01 SEC.
   compiling exported * : ($,$) -> $
Time: 0.06 SEC.
   compiling exported ** : ($,Integer) -> $
Time: 0.01 SEC.
   compiling exported ** : ($,NonNegativeInteger) -> $
Time: 0 SEC.
   compiling exported / : ($,$) -> $
Time: 0.01 SEC.

(time taken in buildFunctor:  1)
;;;     ***       |Indeterminant| REDEFINED
;;;     ***       |Indeterminant| REDEFINED
Time: 0.01 SEC.
   Warnings: 
      [1] conv: pretend$ -- should replace by @
   Cumulative Statistics for Constructor Indeterminant
      Time: 0.51 seconds
   finalizing NRLIB INDET 
   Processing Indeterminant for Browser database:
--------(eval ((Any) %))---------
--------(binary (% % (List %)))---------
--------(function (% % (List (Symbol)) (Symbol)))---------
--------(lambda (% % (List (Symbol))))---------
--------(+ (% % %))---------
--------(- (% % %))---------
--------(- (% %))---------
--------(* (% % %))---------
--------(/ (% % %))---------
--------(** (% % (NonNegativeInteger)))---------
--------(** (% % (Integer)))---------
--------(unparse ((String) %))---------
--------(declare ((Symbol) (List %)))---------
--------(compile ((Symbol) (Symbol) (List %)))---------
--->-->Indeterminant((coerce (% (Integer)))): Not documented!!!!
--------constructor---------
------------------------------------------------------------------------
   Indeterminant is now explicitly exposed in frame initial 
   Indeterminant will be automatically loaded when needed from 
      /var/zope2/var/LatexWiki/INDET.NRLIB/code

Symbolic Matrices

axiom
)clear all
   All user variables and function definitions have been cleared.

axiom
m:Union(Indeterminant,Matrix Integer)

axiom
n:Union(Indeterminant,Matrix Integer)

axiom
a:Union(Indeterminant,Integer)

axiom
b:Union(Indeterminant,Integer)

axiom
ab:=(3*a+b)*(a-2*b)

(11)

axiom
a:=1$Integer  -- because 0 and 1 can be symbolic!

(12)

axiom
eval ab

(13)

axiom
b:=0$Integer

(14)

axiom
a:=-10

(15)

axiom
eval ab

(16)

axiom
mn1:= m*n-n*m

(17)

axiom
mn2:=(m+n)*(m-n-1)

(18)

axiom
m:=matrix [[1,2],[3,4]]

(19)

axiom
n:=matrix [[-1,-2],[-3,4]]

(20)

axiom
eval mn1

(21)

axiom
eval mn2

(22)

axiom
)clear all

All user variables and function definitions have been cleared.

axiom
d: Union(Variable d, Float)

axiom
d*2

(23)

will be problematic, and the assignment between symbolic integers is not allowed.

axiom
a: Union(Variable a, Integer)

axiom
b: Union(Variable b, Integer)

axiom
b:=a
   a is declared as being in Union(Variable a,Integer) but has not been
      given a value.

axiom
p:=2*d

(24)

axiom
eval(p,d=3.14)

(25)

But there is still a problem since I can write:

axiom
a:Union(Variable a,Integer)

axiom
a:=3.14
   Cannot convert right-hand side of assignment
   3.14
      to an object of the type Union(Variable a,Integer) of the
      left-hand side.
p:=2*a

(26)

axiom
eval(p,a=3.14)

(27)

and Axiom does not complain about the eval request because as far as Polynomial Integer is concerned d is just a Symbol.

In the case of the example Indeterminant domain, evaluation of symbolic expressions is always delayed so an appropriate eval operation could be defined that properly respects the type.

axiom
c:Union(Variable(c),Symbol)

axiom
c:=a

(28)

PS: In the light of polynomial, (2d) is a non-zero polynomial, so that it's always safe to write (1/(2d)), but it's actually non-safe to do it in the domain of float(or integer).

b:=a is meaningless, of course. But there are many scenarios

axiom
)clear all
   All user variables and function definitions have been cleared.

axiom
i:=10

how about i:=-10?

(29)

Type: PositiveInteger?

axiom
a: Union(Variable a, Integer)

Type: Void

axiom
b: Union(Variable b, Integer)

Type: Void

axiom
b:= (i>0=>1; a)

(30)

Type: Union(Integer,...)

which is meaningful.

We wish to place a restriction on the possible values that certain symbols can take. Such symbols and expressions formed from them certainly cannot live in a numeric domain such as Float. Except in certain circumstances (mentioned previously) I think a domain such as a:Union(Variable(a),Float) and the domains to which it can be coerced (such as Polynomial, Expression, ...) does already represent such a symbolic expressions fairly well.

But 1) What is Symbolic Float? Can you give a description?

And 2) How can I express the concept of "non-zero polynomial" in Axiom? I might use a domain that does not include zero for example a:Union(Variable(a),PositiveInteger) but there is no general domain of NonZero anything.

Ok, back to my own point. what's the justification of that the multiplication of two floats returns a polynomial float? Even the value is unknown, the type is certain, and float is closed under multiplication, so the return must be still a float, right?

AFAIK, Axiom currently support only polynomials with coefficients of known values. Then the only zero-polynomial(Integer) is 0$Polynomial Integer, others are non-zero polynomials.

But Axiom currently does not have any domain whose values are symbolic expressions which only evaluate to values in some specific domain. Polynomial is one of the existing domains in Axiom whose values are symbolic expressions (of a very specific type). Symbolic expression in the domain Expression are more general but still rather restricted in form. Finally there is InputForm? which consists of fully unevaluated expressions of the most general form allowed in Axiom.

Perhaps what you have called "Symbolic Float" could be implemented as an extension of the domain I called "Indeterminant" above.