[Axiom-developer] Re: [fricas-devel] Re: [Axiom-mail] InputForm

[Tim Daly]

I've been reading this thread. It seems to me that what people are seeking
is a symbolic algebra rather than a computer algebra system. The distinction
is that a symbolic system manipulates input as parse trees in syntactic 
form.
A computer algebra system manipulates input as semantic forms. It appears
that you want to recover the syntax from the semantics, a very hard problem.

This discussion came up before. At the time I wrote the beginnings of a
symbolic front end to Axiom based on Joel Cohen's work. Joel has given
me permission to use his books as part of the effort.

Joel describes a symbolic, expression tree based system for doing
computational mathematics. I call this a "Cohen Algebra". Using these
expression trees allows us to carefully craft and manipulate the expressions
in ways that Axiom would not normally permit because they are not
semantically valid. As long as the forms are never coerced to Axiom
domains until they are semantically valid, it is possible to do many
"badly formed" intermediate manipulations, some of which are very
useful for teaching purposes.

We can get the Cohen algebra into Axiom using categories, domains, and
packages that support expression tree I/O and coercions to and from
Axiom domains, e.g.
  cohenPolynomial(cohenInteger) <-> Polynomial(Integer)

This enables us to address several issues that have been outstanding
in the field for a while, including those mentioned at the last conference:

 *) It would be possible to do "step-by-step" output (Watt?)
         That is, you could show the steps of solving 3*x=6
          by showing the step of dividing both sides by 3
             3       6
             -  x =  -
             3       3
        and preserve the 3 on both sides

  *) It would be possible to do "step-by-step* explanations (Watt?)
         Algorithms in the Cohen domains could easily have
         explanations attached to the operations so that it could
         automatically print:
              "divide each side by 3"

    *) It would be possible to modify the output if the result
         turned into "wallpaper" (as mentioned by Davenport).
         So you could simply print the condensed output of a
         groebner basis computation.

     *) It would be much easier to input and output forms for
         other systems (e.g. supporting OpenMath output)
         (Davenport)

I plan to do more work on Cohen domains because all of the
above features would be useful. My simple test example domains
are attached.

In my opinion, the idea of using InputForm beyond its intended
interpreter connections is not a viable effort. It would be much
easier and more profitable to construct something like the Cohen
domains to support the goal.

Tim

============================================

)abbrev category CCAT CohenCategory

+++ Author: Timothy Daly
+++ Date Created: 7 April 2007
+++ Description: Joel Cohen's Computer Algebra and Symbolic Computation
CohenCategory(): Category == SetCategory with

 kind:(CExpr)->Boolean
   ++ kind(CExpr)
 operand:(CExpr,Integer)->CExpr
   ++ operand:(CExpr,Integer)
 numberOfOperand:(CExpr)->Integer
   ++ numberOfOperand:(CExpr)->Integer
 construct:(CExpr,CExpr)->CExpr
   ++ construct:(CExpr,CExpr)->CExpr

-------------------------------------------------------------------
)abbrev domain CTERM CohenTerm

+++ Author: Timothy Daly
+++ Date Created: 7 April 2007
+++ Description: Joel Cohen's Computer Algebra and Symbolic Computation
CohenTerm(): Exports == Implementation where
 OUT     ==> OutputForm
 ATTRIBS ==> Record(attrib: String, value: String)
 UNION   ==> Union(Symbol,String,Integer)
 TAGS    ==> Record(name:UNION, tags:List ATTRIBS)

 Exports ==> CohenCategory with
   term: () -> %
   term: Symbol -> %
   term: String -> %
   term: Integer -> %
   name: % -> String
   tags: % -> List ATTRIBS
   coerce: Symbol -> %
   coerce: String -> %
   coerce: Integer -> %
   coerce: % -> OUT
   _=: (%,%) -> Boolean

 Implementation ==> add

   Rep := TAGS

   tagPair(atype:String,thetype:String):ATTRIBS ==
     attr:ATTRIBS:=[atype,thetype]

   name(t0:%):String ==
     t1:=t0.name
     t1 case Symbol  => string t1
     t1 case String  => t1
     t1 case Integer => string t1
     "failed"

   tags(t0:%):List ATTRIBS == t0.tags

   term():% ==
     attr:List ATTRIBS:= list tagPair("type","String")
     aname:=""::UNION
     result:TAGS:=[aname,attr]
     result

   term(s:Symbol):%  == [s,[tagPair("type","Symbol")]]
   coerce(s:Symbol):%  == [s,[tagPair("type","Symbol")]]

   term(s:String):%  == [s,[tagPair("type","String")]]
   coerce(s:String):%  == [s,[tagPair("type","String")]]

   term(s:Integer):% == [s,[tagPair("type","Integer")]]
   coerce(s:Integer):% == [s,[tagPair("type","Integer")]]

   coerce(arg:%):OUT ==
     t0:=arg.name
     t1:=arg.tags
     t2:=
       t0 case Symbol  => outputForm t0
       t0 case String  => outputForm t0
       t0 case Integer => outputForm t0
       "failed"
     --bracket [ t2, t1.1 ]
     t2

   a = b ==
     a.name = b.name


-------------------------------------------------------------------
)abbrev domain CTREE CohenTree

+++ Author: Timothy Daly
+++ Date Created: 7 April 2007
+++ Description: Joel Cohen's Computer Algebra and Symbolic Computation
CohenTree(S: CohenCategory): Exports == Implementation where
 Exports == BinaryTreeCategory(S) with
  cohenTree: S -> %
   ++ cohenTree(v) is an non-empty cohen tree
   ++ with value v, and left and right empty.
   ++
   ++X t1:=cohenTree([1,2,3])
  
  cohenTree: (%,S,%) -> %   
   ++ cohenTree(l,v,r) creates a cohen tree with
   ++ value v with left subtree l and right subtree r.
   ++
   ++X t1:=cohenTree([1,2,3])
   ++X t2:=cohenTree([4,5,6])
   ++X cohenTree(t1,[7,8,9],t2)

  cohenTree: (%,S) -> %
   ++ cohenTree(v,r) creates a cohen tree with
   ++ value v with right subtree r.

  cohenTree: (S,%) -> %
   ++ cohenTree(l,v) creates a cohen tree with
   ++ value v with left subtree l

  empty: () -> %
   ++ empty()
  empty?: % -> Boolean
   ++ empty?(a)
  leaf?: % -> Boolean
   ++ leaf?(a)
  left: % -> %
   ++ left(a)
  node: (%,S,%) -> %
   ++ node(a,b,c)
  right: % -> %
   ++ right(a)
  setleft_!: (%,%) -> %
   ++ setleft!(a,b)
  setright_!: (%,%) -> %
   ++ setright!(a,b)
  setvalue_!: (%,S) -> S
   ++ setvalue!(a,b)
  value: % -> S
   ++ value(a)
  
 Implementation == add
  Rep := List Tree S

  cohenTree(v:S) == node(empty(),v,empty())
  cohenTree(l:%,v:S,r:%):% == node(l,v,r)
  cohenTree(l:%,v:S):% == node(l,v,empty())
  cohenTree(v:S,r:%):% == node(empty(),v,r)
  empty()== [] pretend %
  empty? t == empty?(t)$Rep
  leaf? t  == empty? t or empty? left t and empty? right t
  left t ==
    empty? t => error "cohenTree:no left"
    children first t
  node(l,v,r) == cons(tree(v,l:Rep),r:Rep)
  right t ==
    empty? t => error "cohenTree:no right"
    rest t
  setleft_!(t1,t2) ==
    empty? t1 => error "cohenTree:no left to set"
    setchildren_!(first(t1:Rep),t2:Rep)
    t1
  setright_!(t1,t2) ==
    empty? t1 => error "cohenTree:no right to set"
    setrest_!(t1:List Tree S,t2)
  setvalue_!(t,nd) ==
    empty? t => error "cohenTree:no value to set"
    setvalue_!(first(t:Rep),nd)
    nd
  value t ==
    empty? t => error "cohenTree:no value"
    value first t
  t1 = t2 == (t1::Rep) =$Rep (t2::Rep)


-------------------------------------------------------------------
--  a:=a::CTERM
--  b:=b::CTERM
--  c:=a+b
--  left(c)
--  right(c)
--  d:=3::CTERM
--  e:=d*c
--  left(e)
--  right(e)
--
--  -- Figure 3.4 p88
--  )clear all
--
--  c:=c::CTERM
--  d:=d::CTERM
--  x:=x::CTERM
--  two:=2::CTERM
--  e:=c+d*x^2
--
--  -- Figure 3.5a p89
--  )clear all
--  a:=a::CTERM
--  b:=b::CTERM
--  c:=c::CTERM
--  d:=a*b+c
--  e:=-d

-------------------------------------------------------------------
)abbrev package CMATH CohenMath

+++ Author: Timothy Daly
+++ Date Created: 7 April 2007
+++ Description: Joel Cohen's Computer Algebra and Symbolic Computation
CohenMath: Exports == Implementation where
 TERM ==> CohenTerm
 TREE ==> CohenTree(TERM)

 Exports ==> with
  _-: (TERM) -> TREE
   ++ -a
  _-: (TREE) -> TREE
   ++ -a

--   "!": (TERM) -> TREE
--    ++ a!
--   "!": (TREE) -> TREE
--    ++ a!

  _-: (TERM,TERM) -> TREE
   ++ a-b
  _-: (TERM,TREE) -> TREE
   ++ a-b
  _-: (TREE,TERM) -> TREE
   ++ a-b
  _-: (TREE,TREE) -> TREE
   ++ a-b

  _+: (TERM,TERM) -> TREE
   ++ a+b
  _+: (TERM,TREE) -> TREE
   ++ a+b
  _+: (TREE,TERM) -> TREE
   ++ a+b
  _+: (TREE,TREE) -> TREE
   ++ a+b

  _*: (TERM,TERM) -> TREE
   ++ a*b
  _*: (TERM,TREE) -> TREE
   ++ a*b
  _*: (TREE,TERM) -> TREE
   ++ a*b
  _*: (TREE,TREE) -> TREE
   ++ a*b

  _^: (TERM,TERM) -> TREE
   ++ a*b
  _^: (TERM,TREE) -> TREE
   ++ a*b
  _^: (TREE,TERM) -> TREE
   ++ a*b
  _^: (TREE,TREE) -> TREE
   ++ a*b

 Implementation ==> add

  --- handle unary prefix terms

  prefixTerm(op:TERM,b:TERM):TREE  == cohenTree(op,cohenTree(b))
  prefixTree(op:TERM,b:TREE):TREE  == cohenTree(op,b)

  --- handle unary postfix terms

  postfixTerm(a:TERM,op:TERM):TREE == cohenTree(cohenTree(a),op)
  postfixTree(a:TREE,op:TERM):TREE == cohenTree(a,op)

  --- handle binary terms

  termOpTerm(a:TERM,op:TERM,b:TERM):TREE ==
     cohenTree(cohenTree(a),op,cohenTree(b))

  termOpTree(a:TERM,op:TERM,b:TREE):TREE ==
     cohenTree(cohenTree(a),op,b)

  treeOpTerm(a:TREE,op:TERM,b:TERM):TREE ==
     cohenTree(a,op,cohenTree(b))

  treeOpTree(a:TREE,op:TERM,b:TREE):TREE ==
     cohenTree(a,op,b)

  _-(b:TERM):TREE         == prefixTerm(term("-")$TERM,b)
  _-(c:TREE):TREE         == prefixTree(term("-")$TERM,c)

--   "!"(a:TERM):TREE         == postfixTerm(a,term("!")$TERM)
--   "!"(a:TREE):TREE         == postfixTree(a,term("!")$TERM)

  _-(a:TERM, b:TERM):TREE == termOpTerm(a,term("-")$TERM,b)
  _-(a:TERM, b:TREE):TREE == termOpTree(a,term("-")$TERM,b)
  _-(a:TREE, b:TERM):TREE == treeOpTerm(a,term("-")$TERM,b)
  _-(a:TREE, b:TREE):TREE == treeOpTree(a,term("-")$TERM,b)

  _+(a:TERM, b:TERM):TREE == termOpTerm(a,term("+")$TERM,b)
  _+(a:TERM, b:TREE):TREE == termOpTree(a,term("+")$TERM,b)
  _+(a:TREE, b:TERM):TREE == treeOpTerm(a,term("+")$TERM,b)
  _+(a:TREE, b:TREE):TREE == treeOpTree(a,term("+")$TERM,b)

  _*(a:TERM, b:TERM):TREE == termOpTerm(a,term("*")$TERM,b)
  _*(a:TERM, b:TREE):TREE == termOpTree(a,term("*")$TERM,b)
  _*(a:TREE, b:TERM):TREE == treeOpTerm(a,term("*")$TERM,b)
  _*(a:TREE, b:TREE):TREE == treeOpTree(a,term("*")$TERM,b)

  _^(a:TERM, b:TERM):TREE == termOpTerm(a,term("^")$TERM,b)
  _^(a:TERM, b:TREE):TREE == termOpTree(a,term("^")$TERM,b)
  _^(a:TREE, b:TERM):TREE == treeOpTerm(a,term("^")$TERM,b)
  _^(a:TREE, b:TREE):TREE == treeOpTree(a,term("^")$TERM,b)


-------------------------------------------------------------------
)abbrev domain COHEN CohenAlgebra

+++ Author: Timothy Daly (based on Joel Cohen's books)
+++ Date Created: 7 April 2007
+++ Description:
+++ This type represents symbolic algebra as detailed in Joel Cohen's
+++ books "Computer Algebra and Symbolic Computation"
+++ A.K. Peters, Ltd. ISBN 1-56881-159-4
+++
+++ Elements of this domain are purely symbolic expressions represented
+++ in a tree structure.

CohenAlgebra(X : CohenCategory) : CohenCategory with

 _+: (X,X) -> %
  ++ x + y is the formal sum of the input arguments

 _/: (X,X) -> %
  ++ x / y is the formal fraction of the input arguments

 numer : % -> X
  ++ numer(x) is the numerator of the formal fraction

 denom : % -> X
  ++ denom(x) is the denominator of the formal fraction

 if X has IntegralDomain then

   coerce : % -> Fraction(X)
    ++ coerce(x) from here to Fraction(there)

   coerce : Fraction(X) -> %
    ++ coerce(x) from Fraction(there) to here

 if X has Field then
  
   coerce : % -> X
    ++ coerce from here to Field(there)

== add

 import Record(num : X, den : X)

 Rep := Record(num : X, den : X)  -- representation

-- (a::CTERM + b::CTERM)$COHEN(CTERM)
-- c:CTERM:=d
-- e:CTERM:=f
-- (c+e)$COHEN(CTERM)

 (n:X + d:X):% == [n,d]

-- (a::CTERM / b::CTERM)$COHEN(CTERM)
-- c:CTERM:=d
-- e:CTERM:=f
-- (c/e)$COHEN(CTERM)

 (n:X / d:X):% == [n,d]

-- g:=(c/e)$COHEN(CTERM)
-- h:=(c/e)$COHEN(CTERM)
-- (g=h)
-- (g=h)::Boolean
-- i:=(a::CTERM / b::CTERM)$COHEN(CTERM)
-- j:=(a::CTERM / b::CTERM)$COHEN(CTERM)
-- (i=j)::Boolean
-- (g=i)
-- (g=i)::Boolean

 _=(x:%, y:%):Boolean == (x.num = y.num) and (x.den = y.den)

-- numer g
-- numer i

 numer(r:%):X == r.num

--denom g
--denom i

 denom(r:%):X == r.den

 coerce(r:%):OutputForm == (r.num :: OutputForm) / (r.den :: OutputForm)



-- COMPLEX(INT) has FIELD
-- COMPLEX(INT) has IntegralDomain
-- p:COMPLEX(INT):=2
-- p::FRAC(COMPLEX(INT))::COHEN(COMPLEX(INT))

 if X has IntegralDomain then

   coerce(r : %) : Fraction(X)
     ==  (r.num / r.den) @ Fraction(X)

   coerce(x : Fraction(X)) : % == x pretend % 

-- FRAC(POLY(INT)) has FIELD
-- m:=(x^2)@FRAC(POLY(INT))
-- m::COHEN(POLY(INT))

 if X has Field then
   coerce(r : %) : X
     == (r.num / r.den) @ X