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

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