help links subscribe changes refresh edit

	SandBox
SandBoxInductiveType ←	↑	→ SandBoxJacobiDiag

SandBoxInequation

Edit detail for SandBoxInequation revision 2 of 11

	1 2 3 4 5 6 7 8 9 10 11
Editor: Bill Page Time: 2008/06/09 20:12:39 GMT-7
Note: Inequations as mathematical objects

changed:
-inequation(2,3)
-equation(2,3)
t1:=inequation(2,3)
t1::Boolean
t2:=equation(2,3)
t2::Boolean

spad)abbrev domain NE Inequation
--FOR THE BENEFIT  OF LIBAX0 GENERATION
++ Author: Bill Page
++ Based on: Equation by Stephen M. Watt, enhancements by Johannes Grabmeier
++ Date Created: June 2008
++ Basic Operations: ~=
++ Related Domains: Equation
++ Also See:
++ AMS Classifications:
++ Keywords: inequation
++ Examples:
++ References:
++ Description:
++   Inequations as mathematical objects.  All properties of the basis domain,
++   e.g. being an abelian group are carried over the equation domain, by
++   performing the structural operations on the left and on the
++   right hand side.
--   The interpreter translates "~=" to "inequation".  Otherwise, it will
--   find a modemap for "~=" in the domain of the arguments.
Inequation(S: Type): public == private where
  public ==> Type with
    "~=": (S, S) -> $
        ++ a~=b creates an inequation.
    inequation: (S, S) -> $
        ++ inequation(a,b) creates an inequation.
    swap: $ -> $
        ++ swap(eq) interchanges left and right hand side of inequation eq.
    lhs: $ -> S
        ++ lhs(eqn) returns the left hand side of inequation eqn.
    rhs: $ -> S
        ++ rhs(eqn) returns the right hand side of inequation eqn.
    map: (S -> S, $) -> $
        ++ map(f,eqn) constructs a new inequation by applying f to both
        ++ sides of eqn. (f must be an injection)
    if S has InnerEvalable(Symbol,S) then
             InnerEvalable(Symbol,S)
    if S has SetCategory then
        SetCategory
        CoercibleTo Boolean
        if S has Evalable(S) then
           eval: ($, Equation S) -> $
               ++ eval(eqn, x=f) replaces x by f in inequation eqn.
           eval: ($, List Equation S) -> $
               ++ eval(eqn, [x1=v1, ... xn=vn]) replaces xi by vi in inequation eqn.
    if S has AbelianSemiGroup then
        AbelianSemiGroup
        "+": (S, $) -> $
            ++ x+eqn produces a new inequation by adding x to both sides of
            ++ inequation eqn.
        "+": ($, S) -> $
            ++ eqn+x produces a new inequation by adding x to both sides of
            ++ inequation eqn.
    if S has AbelianGroup then
        AbelianGroup
        leftZero : $ -> $
          ++ leftZero(eq) subtracts the left hand side.
        rightZero : $ -> $
          ++ rightZero(eq) subtracts the right hand side.
        "-": (S, $) -> $
            ++ x-eqn produces a new equation by subtracting both sides of
            ++ equation eqn from x.
        "-": ($, S) -> $
            ++ eqn-x produces a new equation by subtracting x from  both sides of
            ++ equation eqn.
    if S has SemiGroup then
        SemiGroup
        "*": (S, $) -> $
            ++ x*eqn produces a new equation by multiplying both sides of
            ++ equation eqn by x.
        "*": ($, S) -> $
            ++ eqn*x produces a new equation by multiplying both sides of
            ++ equation eqn by x.
    if S has Monoid then
        Monoid
        leftOne : $ -> Union($,"failed")
          ++ leftOne(eq) divides by the left hand side, if possible.
        rightOne : $ -> Union($,"failed")
          ++ rightOne(eq) divides by the right hand side, if possible.
    if S has Group then
        Group
        leftOne : $ -> Union($,"failed")
          ++ leftOne(eq) divides by the left hand side.
        rightOne : $ -> Union($,"failed")
          ++ rightOne(eq) divides by the right hand side.
    if S has Ring then
      Ring
      BiModule(S,S)
    if S has CommutativeRing then
      Module(S)
      --Algebra(S)
    if S has IntegralDomain then
      factorAndSplit : $ -> List $
        ++ factorAndSplit(eq) make the right hand side 0 and
        ++ factors the new left hand side. Each factor is equated
        ++ to 0 and put into the resulting list without repetitions.
    if S has PartialDifferentialRing(Symbol) then
      PartialDifferentialRing(Symbol)
    if S has Field then
      VectorSpace(S)
      "/": ($, $) -> $
          ++ e1/e2 produces a new equation by dividing the left and right
          ++ hand sides of equations e1 and e2.
      inv: $ -> $
          ++ inv(x) returns the multiplicative inverse of x.
    if S has ExpressionSpace then
        subst: ($, $) -> $
             ++ subst(eq1,eq2) substitutes eq2 into both sides of eq1
             ++ the lhs of eq2 should be a kernel
  private ==> add
    Rep := Record(lhs: S, rhs: S)
    eq1,eq2: $
    s : S
    if S has IntegralDomain then
        factorAndSplit eq ==
          (S has factor : S -> Factored S) =>
            eq0 := rightZero eq
            [inequation(rcf.factor,0) for rcf in factors factor lhs eq0]
          [eq]
    l:S ~= r:S      == [l, r]
    inequation(l, r) == [l, r]    -- hack!  See comment above.
    lhs eqn        == eqn.lhs
    rhs eqn        == eqn.rhs
    swap eqn     == [rhs eqn, lhs eqn]
    map(fn, eqn)   == inequation(fn(eqn.lhs), fn(eqn.rhs))
    if S has InnerEvalable(Symbol,S) then
        s:Symbol
        ls:List Symbol
        x:S
        lx:List S
        eval(eqn,s,x) == eval(eqn.lhs,s,x) ~= eval(eqn.rhs,s,x)
        eval(eqn,ls,lx) == eval(eqn.lhs,ls,lx) ~= eval(eqn.rhs,ls,lx)
    if S has Evalable(S) then
        eval(eqn1:$, eqn2:Equation S):$ ==
           eval(eqn1.lhs, eqn2) ~= eval(eqn1.rhs, eqn2)
        eval(eqn1:$, leqn2:List Equation S):$ ==
           eval(eqn1.lhs, leqn2) ~= eval(eqn1.rhs, leqn2)
    if S has SetCategory then
        eq1 = eq2 == (eq1.lhs = eq2.lhs)@Boolean and
                     (eq1.rhs = eq2.rhs)@Boolean
        coerce(eqn:$):OutputForm == blankSeparate([eqn.lhs::OutputForm, "~=", eqn.rhs::OutputForm])$OutputForm
        coerce(eqn:$):Boolean == eqn.lhs ~= eqn.rhs
    if S has AbelianSemiGroup then
        eq1 + eq2 == eq1.lhs + eq2.lhs ~= eq1.rhs + eq2.rhs
        s + eq2 == [s,s] + eq2
        eq1 + s == eq1 + [s,s]
    if S has AbelianGroup then
        - eq == (- lhs eq) ~= (-rhs eq)
        s - eq2 == [s,s] - eq2
        eq1 - s == eq1 - [s,s]
        leftZero eq == 0 ~= rhs eq - lhs eq
        rightZero eq == lhs eq - rhs eq ~= 0
        0 == inequation(0$S,0$S)
        eq1 - eq2 == eq1.lhs - eq2.lhs ~= eq1.rhs - eq2.rhs
    if S has SemiGroup then
        eq1:$ * eq2:$ == eq1.lhs * eq2.lhs ~= eq1.rhs * eq2.rhs
        l:S   * eqn:$ == l       * eqn.lhs ~= l       * eqn.rhs
        l:S * eqn:$  ==  l * eqn.lhs    ~=    l * eqn.rhs
        eqn:$ * l:S  ==  eqn.lhs * l    ~=    eqn.rhs * l
        -- We have to be a bit careful here: raising to a +ve integer is OK
        -- (since it's the equivalent of repeated multiplication)
        -- but other powers may cause contradictions
        -- Watch what else you add here! JHD 2/Aug 1990
    if S has Monoid then
        1 == inequation(1$S,1$S)
        recip eq ==
          (lh := recip lhs eq) case "failed" => "failed"
          (rh := recip rhs eq) case "failed" => "failed"
          [lh :: S, rh :: S]
        leftOne eq ==
          (re := recip lhs eq) case "failed" => "failed"
          1 ~= rhs eq * re
        rightOne eq ==
          (re := recip rhs eq) case "failed" => "failed"
          lhs eq * re ~= 1
    if S has Group then
        inv eq == [inv lhs eq, inv rhs eq]
        leftOne eq == 1 ~= rhs eq * inv rhs eq
        rightOne eq == lhs eq * inv rhs eq ~= 1
    if S has Ring then
        characteristic() == characteristic()$S
        i:Integer * eq:$ == (i::S) * eq
    if S has IntegralDomain then
        factorAndSplit eq ==
          (S has factor : S -> Factored S) =>
            eq0 := rightZero eq
            [inequation(rcf.factor,0) for rcf in factors factor lhs eq0]
          (S has Polynomial Integer) =>
            eq0 := rightZero eq
            MF ==> MultivariateFactorize(Symbol, IndexedExponents Symbol, _
               Integer, Polynomial Integer)
            p : Polynomial Integer := (lhs eq0) pretend Polynomial Integer
            [inequation((rcf.factor) pretend S,0) for rcf in factors factor(p)$MF]
          [eq]
    if S has PartialDifferentialRing(Symbol) then
        differentiate(eq:$, sym:Symbol):$ ==
           [differentiate(lhs eq, sym), differentiate(rhs eq, sym)]
    if S has Field then
        dimension() == 2 :: CardinalNumber
        eq1:$ / eq2:$ == eq1.lhs / eq2.lhs ~= eq1.rhs / eq2.rhs
        inv eq == [inv lhs eq, inv rhs eq]
    if S has ExpressionSpace then
        subst(eq1,eq2) ==
            eq3 := eq2 pretend Equation S
            [subst(lhs eq1,eq3),subst(rhs eq1,eq3)]

spad

   Compiling FriCAS source code from file 
      /var/zope2/var/LatexWiki/1462006071647286096-25px001.spad using 
      old system compiler.
   NE abbreviates domain Inequation 
   processing macro definition public ==> -- the constructor category 
   processing macro definition private ==> -- the constructor capsule 
------------------------------------------------------------------------
   initializing NRLIB NE for Inequation 
   compiling into NRLIB NE 
****** Domain: S already in scope
augmenting S: (IntegralDomain)
augmenting $: (SIGNATURE $ factorAndSplit ((List $) $))
   compiling exported factorAndSplit : $ -> List $
augmenting S: (SIGNATURE S factor ((Factored S) S))
Time: 0.10 SEC.
   compiling exported ~= : (S,S) -> $
      NE;~=;2S$;2 is replaced by CONS 
Time: 0 SEC.
   compiling exported inequation : (S,S) -> $
      NE;inequation;2S$;3 is replaced by CONS 
Time: 0 SEC.
   compiling exported lhs : $ -> S
      NE;lhs;$S;4 is replaced by QCAR 
Time: 0.01 SEC.
   compiling exported rhs : $ -> S
      NE;rhs;$S;5 is replaced by QCDR 
Time: 0 SEC.
   compiling exported swap : $ -> $
Time: 0 SEC.
   compiling exported map : (S -> S,$) -> $
Time: 0 SEC.
****** Domain: S already in scope
augmenting S: (InnerEvalable (Symbol) S)
   compiling exported eval : ($,Symbol,S) -> $
Time: 0.01 SEC.
   compiling exported eval : ($,List Symbol,List S) -> $
Time: 0 SEC.
****** Domain: S already in scope
augmenting S: (Evalable S)
   compiling exported eval : ($,Equation S) -> $
Time: 0 SEC.
   compiling exported eval : ($,List Equation S) -> $
Time: 0.01 SEC.
****** Domain: S already in scope
augmenting S: (SetCategory)
   compiling exported = : ($,$) -> Boolean
Time: 0.07 SEC.
   compiling exported coerce : $ -> OutputForm
Time: 0.01 SEC.
   compiling exported coerce : $ -> Boolean
Time: 0 SEC.
****** Domain: S already in scope
augmenting S: (AbelianSemiGroup)
augmenting $: (SIGNATURE $ + ($ S $))
augmenting $: (SIGNATURE $ + ($ $ S))
   compiling exported + : ($,$) -> $
Time: 0 SEC.
   compiling exported + : (S,$) -> $
Time: 0 SEC.
   compiling exported + : ($,S) -> $
Time: 0 SEC.
****** Domain: S already in scope
augmenting S: (AbelianGroup)
augmenting $: (SIGNATURE $ leftZero ($ $))
augmenting $: (SIGNATURE $ rightZero ($ $))
augmenting $: (SIGNATURE $ - ($ S $))
augmenting $: (SIGNATURE $ - ($ $ S))
   compiling exported - : $ -> $
Time: 0.01 SEC.
   compiling exported - : (S,$) -> $
Time: 0 SEC.
   compiling exported - : ($,S) -> $
Time: 0 SEC.
   compiling exported leftZero : $ -> $
Time: 0 SEC.
   compiling exported rightZero : $ -> $
Time: 0 SEC.
   compiling exported Zero : () -> $
Time: 0 SEC.
   compiling exported - : ($,$) -> $
Time: 0 SEC.
****** Domain: S already in scope
augmenting S: (SemiGroup)
augmenting $: (SIGNATURE $ * ($ S $))
augmenting $: (SIGNATURE $ * ($ $ S))
   compiling exported * : ($,$) -> $
Time: 0.01 SEC.
   compiling exported * : (S,$) -> $
Time: 0 SEC.
   compiling exported * : (S,$) -> $
Time: 0 SEC.
   compiling exported * : ($,S) -> $
Time: 0 SEC.
****** Domain: S already in scope
augmenting S: (Monoid)
augmenting $: (SIGNATURE $ leftOne ((Union $ failed) $))
augmenting $: (SIGNATURE $ rightOne ((Union $ failed) $))
   compiling exported One : () -> $
Time: 0.01 SEC.
   compiling exported recip : $ -> Union($,failed)
Time: 0 SEC.
   compiling exported leftOne : $ -> Union($,failed)
Time: 0 SEC.
   compiling exported rightOne : $ -> Union($,failed)
Time: 0 SEC.
****** Domain: S already in scope
augmenting S: (Group)
augmenting $: (SIGNATURE $ leftOne ((Union $ failed) $))
augmenting $: (SIGNATURE $ rightOne ((Union $ failed) $))
   compiling exported inv : $ -> $
Time: 0.01 SEC.
   compiling exported leftOne : $ -> Union($,failed)
Time: 0 SEC.
   compiling exported rightOne : $ -> Union($,failed)
Time: 0 SEC.
****** Domain: S already in scope
augmenting S: (Ring)
   compiling exported characteristic : () -> NonNegativeInteger
Time: 0.07 SEC.
   compiling exported * : (Integer,$) -> $
Time: 0 SEC.
****** Domain: S already in scope
augmenting S: (IntegralDomain)
augmenting $: (SIGNATURE $ factorAndSplit ((List $) $))
   compiling exported factorAndSplit : $ -> List $
augmenting S: (SIGNATURE S factor ((Factored S) S))
extension of ##1 to (Polynomial (Integer)) ignored
   processing macro definition MF ==> MultivariateFactorize(Symbol,IndexedExponents Symbol,Integer,Polynomial Integer) 
Time: 0.19 SEC.
****** Domain: S already in scope
augmenting S: (PartialDifferentialRing (Symbol))
   compiling exported differentiate : ($,Symbol) -> $
Time: 0.01 SEC.
****** Domain: S already in scope
augmenting S: (Field)
augmenting $: (SIGNATURE $ / ($ $ $))
augmenting $: (SIGNATURE $ inv ($ $))
   compiling exported dimension : () -> CardinalNumber
Time: 0.01 SEC.
   compiling exported / : ($,$) -> $
Time: 0 SEC.
   compiling exported inv : $ -> $
Time: 0 SEC.
****** Domain: S already in scope
augmenting S: (ExpressionSpace)
augmenting $: (SIGNATURE $ subst ($ $ $))
   compiling exported subst : ($,$) -> $
Time: 0 SEC.
****** Domain: S already in scope
augmenting S: (Evalable S)
****** Domain: S already in scope
augmenting S: (SetCategory)
augmenting $: (SIGNATURE $ eval ($ $ (Equation S)))
augmenting $: (SIGNATURE $ eval ($ $ (List (Equation S))))
****** Domain: S already in scope
augmenting S: (AbelianGroup)
augmenting $: (SIGNATURE $ leftZero ($ $))
augmenting $: (SIGNATURE $ rightZero ($ $))
augmenting $: (SIGNATURE $ - ($ S $))
augmenting $: (SIGNATURE $ - ($ $ S))
****** Domain: S already in scope
augmenting S: (Field)
augmenting $: (SIGNATURE $ / ($ $ $))
augmenting $: (SIGNATURE $ inv ($ $))
****** Domain: S already in scope
augmenting S: (AbelianGroup)
augmenting $: (SIGNATURE $ leftZero ($ $))
augmenting $: (SIGNATURE $ rightZero ($ $))
augmenting $: (SIGNATURE $ - ($ S $))
augmenting $: (SIGNATURE $ - ($ $ S))
****** Domain: S already in scope
augmenting S: (AbelianSemiGroup)
augmenting $: (SIGNATURE $ + ($ S $))
augmenting $: (SIGNATURE $ + ($ $ S))
****** Domain: S already in scope
augmenting S: (ExpressionSpace)
augmenting $: (SIGNATURE $ subst ($ $ $))
****** Domain: S already in scope
augmenting S: (Field)
augmenting $: (SIGNATURE $ / ($ $ $))
augmenting $: (SIGNATURE $ inv ($ $))
****** Domain: S already in scope
augmenting S: (Group)
augmenting $: (SIGNATURE $ leftOne ((Union $ failed) $))
augmenting $: (SIGNATURE $ rightOne ((Union $ failed) $))
****** Domain: S already in scope
augmenting S: (InnerEvalable (Symbol) S)
****** Domain: S already in scope
augmenting S: (IntegralDomain)
augmenting $: (SIGNATURE $ factorAndSplit ((List $) $))
****** Domain: S already in scope
augmenting S: (Monoid)
augmenting $: (SIGNATURE $ leftOne ((Union $ failed) $))
augmenting $: (SIGNATURE $ rightOne ((Union $ failed) $))
****** Domain: S already in scope
augmenting S: (PartialDifferentialRing (Symbol))
****** Domain: S already in scope
augmenting S: (Ring)
****** Domain: S already in scope
augmenting S: (SemiGroup)
augmenting $: (SIGNATURE $ * ($ S $))
augmenting $: (SIGNATURE $ * ($ $ S))
****** Domain: S already in scope
augmenting S: (SetCategory)
(time taken in buildFunctor:  3)
;;;     ***       |Inequation| REDEFINED
;;;     ***       |Inequation| REDEFINED
Time: 0.16 SEC.
   Semantic Errors: 
      [1] factorAndSplit:  rcf has two modes: 
   Warnings: 
      [1] factorAndSplit: not known that (IntegralDomain) is of mode (CATEGORY domain (SIGNATURE factorAndSplit ((List $) $)))
      [2] factorAndSplit: not known that (IntegralDomain) is of mode (CATEGORY S (SIGNATURE factor ((Factored S) S)))
   Cumulative Statistics for Constructor Inequation
      Time: 0.69 seconds
   finalizing NRLIB NE 
   Processing Inequation for Browser database:
--------(~= ($ S S))---------
--------(inequation ($ S S))---------
--------(swap ($ $))---------
--------(lhs (S $))---------
--------(rhs (S $))---------
--------(map ($ (Mapping S S) $))---------
--------(eval ($ $ (Equation S)))---------
--------(eval ($ $ (List (Equation S))))---------
--------(+ ($ S $))---------
--------(+ ($ $ S))---------
--------(leftZero ($ $))---------
--------(rightZero ($ $))---------
--------(- ($ S $))---------
--------(- ($ $ S))---------
--------(* ($ S $))---------
--------(* ($ $ S))---------
--------(leftOne ((Union $ failed) $))---------
--------(rightOne ((Union $ failed) $))---------
--------(leftOne ((Union $ failed) $))---------
--------(rightOne ((Union $ failed) $))---------
--------(factorAndSplit ((List $) $))---------
--------(/ ($ $ $))---------
--------(inv ($ $))---------
--------(subst ($ $ $))---------
--------constructor---------
; (DEFUN |Inequation;| ...) is being compiled.
;; The variable IDENTITY is undefined.
;; The compiler will assume this variable is a global.
------------------------------------------------------------------------
   Inequation is now explicitly exposed in frame initial 
   Inequation will be automatically loaded when needed from 
      /var/zope2/var/LatexWiki/NE.NRLIB/code

It works but the LaTeX? output does not display

axiom)set output tex on
)set output algebra on
inequation(a,b)
   (1)  a ~= b

(1)

Type: Inequation Symbol

axiomt1:=inequation(2,3)
   (2)  2 ~= 3

(2)

Type: Inequation PositiveInteger?

axiomt1::Boolean
   (3)  true

(3)

Type: Boolean

axiomt2:=equation(2,3)
   (4)  2= 3

(4)

Type: Equation PositiveInteger?

axiomt2::Boolean
   (5)  false

(5)

Type: Boolean