login  home  contents  what's new  discussion  bug reports     help  links  subscribe  changes  refresh  edit
SandBox
SandBoxTroubleWithOperators  ← ↑ →  SandBoxUnitsAndDimensions

SandBoxUnify
  
last edited 7 years ago by pagani

fricas
)abbrev package EQREASON EquationalReasoning
++ Author: Kurt Pagani
++ Date Created: Mon Mar 21 17:10:18 CET 2016
++ License: BSD
++ References:
++ Description:
++
EquationalReasoning(R) : Exports == Implementation where

  R : Join(Comparable, IntegralDomain)
  X ==> Expression R
  EQX ==> Equation X
  LEQX ==> List EQX
  Y ==> Union(LEQX,"failed")

  Exports ==  with

    unify: (LEQX, LEQX) -> Y
    reduceWith: (LEQX,LEQX) -> LEQX
    --coerce : % -> OutputForm

  Implementation ==  add 

    symbolClash(x:EQX):Boolean ==
      l:X:=lhs x
      r:X:=rhs x
      kl:=mainKernel l
      kr:=mainKernel r
      if (kl case Kernel(X)) and (kr case Kernel(X)) then
        return test(name kl ~= name kr)
      else
        true

    termReduce(x:EQX):Y ==
      l:=lhs x
      r:=rhs x
      kl:=mainKernel l
      kr:=mainKernel r
      if (kl case Kernel(X)) and (kr case Kernel(X)) then
        al:=argument kl
        ar:=argument kr
        #al ~= #ar => "failed"
        [al.j = ar.j for j in 1..#al]
      else
        "failed"  

    app?(x:X):Boolean ==
      k:=mainKernel(x)
      if (k case Kernel X) then
        test(height k > 1)
      else
        false  

    var?(x:X):Boolean == not(app?(x) or number?(x))

    reduceWith2(x:LEQX, y:LEQX):LEQX ==
      r:=x
      for i in 1..#y repeat
        r:=[subst(r.j,y.i) for j in 1..#x]
      return r

    reduceWith(x:LEQX, y:LEQX):LEQX ==
      [subst(lhs(x.i),y) = subst(rhs(x.i),y) for i in 1..#x]

    occurs(x:X,y:X):Boolean ==
      member?(x,[s::X for s in variables(y)])

    unify(x:LEQX,S:LEQX):Y ==
      if empty? x then return S
      l:=lhs(first x)
      r:=rhs(first x)
      if l = r  then return unify(rest x,S)
      if number? l and number? r then return "failed"
      if (app? l or number? l) and var? r then 
        return unify(concat([r=l],rest x),S)
      if var? l then
        if occurs(l,r) then return "failed"
        return unify(reduceWith(rest x,[l=r]),concat(reduceWith(S,[l=r]),[l=r]))
      if app? l and app? r then
        if symbolClash(l=r) then return "failed"
        rr:Y:=termReduce(l=r)
        if (rr case LEQX) then
          return unify(concat(rr,rest x),S)
        else
          return "failed"
fricas
Compiling FriCAS source code from file 
      /var/lib/zope2.10/instance/axiom-wiki/var/LatexWiki/3793212659814308865-25px.001.spad
      using old system compiler.
   EQREASON abbreviates package EquationalReasoning 
------------------------------------------------------------------------
   initializing NRLIB EQREASON for EquationalReasoning 
   compiling into NRLIB EQREASON 
****** Domain: R already in scope
   compiling local symbolClash : Equation Expression R -> Boolean
Time: 0.02 SEC.

   compiling local termReduce : Equation Expression R -> Union(List Equation Expression R,failed)
Time: 0.02 SEC.

   compiling local app? : Expression R -> Boolean
Time: 0 SEC.

   compiling local var? : Expression R -> Boolean
Time: 0 SEC.

   compiling local reduceWith2 : (List Equation Expression R,List Equation Expression R) -> List Equation Expression R
Time: 0.02 SEC.

   compiling exported reduceWith : (List Equation Expression R,List Equation Expression R) -> List Equation Expression R
Time: 0 SEC.

   compiling local occurs : (Expression R,Expression R) -> Boolean
Time: 0.02 SEC.

   compiling exported unify : (List Equation Expression R,List Equation Expression R) -> Union(List Equation Expression R,failed)
Time: 0.01 SEC.

(time taken in buildFunctor:  0)

;;;     ***       |EquationalReasoning| REDEFINED

;;;     ***       |EquationalReasoning| REDEFINED
Time: 0 SEC.

   Cumulative Statistics for Constructor EquationalReasoning
      Time: 0.09 seconds

   finalizing NRLIB EQREASON 
   Processing EquationalReasoning for Browser database:
--------constructor---------
--->-->EquationalReasoning((unify ((Union (List (Equation (Expression R))) failed) (List (Equation (Expression R))) (List (Equation (Expression R)))))): Not documented!!!!
--->-->EquationalReasoning((reduceWith ((List (Equation (Expression R))) (List (Equation (Expression R))) (List (Equation (Expression R)))))): Not documented!!!!
; compiling file "/var/aw/var/LatexWiki/EQREASON.NRLIB/EQREASON.lsp" (written 04 APR 2022 08:11:36 PM):

; /var/aw/var/LatexWiki/EQREASON.NRLIB/EQREASON.fasl written
; compilation finished in 0:00:00.067
------------------------------------------------------------------------
   EquationalReasoning is now explicitly exposed in frame initial 
   EquationalReasoning will be automatically loaded when needed from 
      /var/aw/var/LatexWiki/EQREASON.NRLIB/EQREASON

fricas
-- nilqed Fre Sep 30 18:25:37 CEST 2016 :: helix
76 lines (66 sloc) 2.49 KB
fricas
)clear all

   All user variables and function definitions have been cleared.

p:=operator 'p
\label{eq1}p(1)
Type: BasicOperator?
fricas
f:=operator 'f
\label{eq2}f(2)
Type: BasicOperator?
fricas
g:=operator 'g
\label{eq3}g(3)
Type: BasicOperator?
fricas
h:=operator 'h
\label{eq4}h(4)
Type: BasicOperator?
fricas
m:=operator 'm
\label{eq5}m(5)
Type: BasicOperator?
fricas
N:=29 -- number of tests
\label{eq6}29(6)
Type: PositiveInteger?
fricas
-----------------------------------------
--
Type: List Equation Expression Integer
fricas
-----------------------------------------
P1:=[f(g(x),x) = f(y,a)]
\label{eq7}\left[{{f \left({{g \left({x}\right)}, \: x}\right)}={f \left({y , \: a}\right)}}\right](7)
Type: List(Equation(Expression(Integer)))
fricas
P2:=[f(x,h(x),y) = f(g(z), u, z)]
\label{eq8}\left[{{f \left({x , \:{h \left({x}\right)}, \: y}\right)}={f \left({{g \left({z}\right)}, \: u , \: z}\right)}}\right](8)
Type: List(Equation(Expression(Integer)))
fricas
P3:=[p(a,x,f(y)) = p(u,v,w),p(a,x,f(y))= p(a, s,f(c)),p(u,v,w) = p(a,s,f(c))]
\label{eq9}\begin{array}{@{}l} \displaystyle \left[{{p \left({a , \: x , \:{f \left({y}\right)}}\right)}={p \left({u , \: v , \: w}\right)}}, \:{{p \left({a , \: x , \:{f \left({y}\right)}}\right)}={p \left({a , \: s , \:{f \left({c}\right)}}\right)}}, \: \right. \ \ \displaystyle \left.{{p \left({u , \: v , \: w}\right)}={p \left({a , \: s , \:{f \left({c}\right)}}\right)}}\right] (9)
Type: List(Equation(Expression(Integer)))
fricas
P4:=[f(x, b, g(z)) = f(f(y), y, g(u))]
\label{eq10}\left[{{f \left({x , \: b , \:{g \left({z}\right)}}\right)}={f \left({{f \left({y}\right)}, \: y , \:{g \left({u}\right)}}\right)}}\right](10)
Type: List(Equation(Expression(Integer)))
fricas
P5:=[p(a,x,h(g(z))) = p(z,h(y),h(y))]
\label{eq11}\left[{{p \left({a , \: x , \:{h \left({g \left({z}\right)}\right)}}\right)}={p \left({z , \:{h \left({y}\right)}, \:{h \left({y}\right)}}\right)}}\right](11)
Type: List(Equation(Expression(Integer)))
fricas
P6:=[p(f(a),g(x)) = p(y,y)]
\label{eq12}\left[{{p \left({{f \left({a}\right)}, \:{g \left({x}\right)}}\right)}={p \left({y , \: y}\right)}}\right](12)
Type: List(Equation(Expression(Integer)))
fricas
P7:=[p(x,x) = p(y,f(y))]
\label{eq13}\left[{{p \left({x , \: x}\right)}={p \left({y , \:{f \left({y}\right)}}\right)}}\right](13)
Type: List(Equation(Expression(Integer)))
fricas
P8:=[sin(x+y) = sin(u^2+v^2)]
\label{eq14}\left[{{\sin \left({y + x}\right)}={\sin \left({{{v}^{2}}+{{u}^{2}}}\right)}}\right](14)
Type: List(Equation(Expression(Integer)))
fricas
P9:=[p(c,b)=p(a,c),p(a,b)=p(b,c)]
\label{eq15}\left[{{p \left({c , \: b}\right)}={p \left({a , \: c}\right)}}, \:{{p \left({a , \: b}\right)}={p \left({b , \: c}\right)}}\right](15)
Type: List(Equation(Expression(Integer)))
fricas
P10:=[p(c,b)=p(a,c),p(a,b)=p(b,c),m(a,b)=m(c,d)]
\label{eq16}\left[{{p \left({c , \: b}\right)}={p \left({a , \: c}\right)}}, \:{{p \left({a , \: b}\right)}={p \left({b , \: c}\right)}}, \:{{m \left({a , \: b}\right)}={m \left({c , \: d}\right)}}\right](16)
Type: List(Equation(Expression(Integer)))
fricas
P11:=[g(x,f(x,b))=g(f(a,b),f(y,z))]
\label{eq17}\left[{{g \left({x , \:{f \left({x , \: b}\right)}}\right)}={g \left({{f \left({a , \: b}\right)}, \:{f \left({y , \: z}\right)}}\right)}}\right](17)
Type: List(Equation(Expression(Integer)))
fricas
P12:=[p(a,x,h(g(z)))=p(z,h(y),h(y))]
\label{eq18}\left[{{p \left({a , \: x , \:{h \left({g \left({z}\right)}\right)}}\right)}={p \left({z , \:{h \left({y}\right)}, \:{h \left({y}\right)}}\right)}}\right](18)
Type: List(Equation(Expression(Integer)))
fricas
P13:=[p(f(a),g(x))=p(y,y)]
\label{eq19}\left[{{p \left({{f \left({a}\right)}, \:{g \left({x}\right)}}\right)}={p \left({y , \: y}\right)}}\right](19)
Type: List(Equation(Expression(Integer)))
fricas
P14:=[f(x1)=f(g(x0,x0))]
\label{eq20}\left[{{f \left({x 1}\right)}={f \left({g \left({x 0, \: x 0}\right)}\right)}}\right](20)
Type: List(Equation(Expression(Integer)))
fricas
P15:=[f(x1,x2)=f(g(x0,x0),g(x1,x1))]
\label{eq21}\left[{{f \left({x 1, \: x 2}\right)}={f \left({{g \left({x 0, \: x 0}\right)}, \:{g \left({x 1, \: x 1}\right)}}\right)}}\right](21)
Type: List(Equation(Expression(Integer)))
fricas
P16:=[f(x1,x2,x3)=f(g(x0,x0),g(x1,x1),g(x2,x2))]
\label{eq22}\left[{{f \left({x 1, \: x 2, \: x 3}\right)}={f \left({{g \left({x 0, \: x 0}\right)}, \:{g \left({x 1, \: x 1}\right)}, \:{g \left({x 2, \: x 2}\right)}}\right)}}\right](22)
Type: List(Equation(Expression(Integer)))
fricas
-- Result list
res:List(Boolean):=[false for i in 1..N]
\label{eq23}\begin{array}{@{}l} \displaystyle \left[ \mbox{\rm false} , \: \mbox{\rm false} , \: \mbox{\rm false} , \: \mbox{\rm false} , \: \mbox{\rm false} , \: \mbox{\rm false} , \: \mbox{\rm false} , \: \mbox{\rm false} , \: \mbox{\rm false} , \: \right. \ \ \displaystyle \left. \mbox{\rm false} , \: \mbox{\rm false} , \: \mbox{\rm false} , \: \mbox{\rm false} , \: \mbox{\rm false} , \: \mbox{\rm false} , \: \mbox{\rm false} , \: \mbox{\rm false} , \: \mbox{\rm false} , \: \right. \ \ \displaystyle \left. \mbox{\rm false} , \: \mbox{\rm false} , \: \mbox{\rm false} , \: \mbox{\rm false} , \: \mbox{\rm false} , \: \mbox{\rm false} , \: \mbox{\rm false} , \: \mbox{\rm false} , \: \mbox{\rm false} , \: \right. \ \ \displaystyle \left. \mbox{\rm false} , \: \mbox{\rm false} \right] (23)
Type: List(Boolean)
fricas
--------
-- unify
--------
res.1:=test (unify(P1,[])=[y= g(a),x= a])
\label{eq24} \mbox{\rm true} (24)
Type: Boolean
fricas
res.2:=test (unify(P2,[])=[x= g(z),u= h(g(z)),y= z])
\label{eq25} \mbox{\rm true} (25)
Type: Boolean
fricas
res.3:=test (unify(P3,[])=[a= u,x= s,w= f(c),v= s,y= c])
\label{eq26} \mbox{\rm true} (26)
Type: Boolean
fricas
res.4:=test (unify(P4,[])=[x= f(y),b= y,z= u])
\label{eq27} \mbox{\rm true} (27)
Type: Boolean
fricas
res.5:=test (unify(P5,[])=[a= z,x= h(g(z)),y= g(z)])
\label{eq28} \mbox{\rm true} (28)
Type: Boolean
fricas
res.6:=test (unify(P6,[]) case "failed")
\label{eq29} \mbox{\rm true} (29)
Type: Boolean
fricas
res.7:=test (unify(P7,[]) case "failed")
\label{eq30} \mbox{\rm true} (30)
Type: Boolean
fricas
res.8:=test (unify(P8,[])=[y + x = v^2  + u^2 ])
\label{eq31} \mbox{\rm true} (31)
Type: Boolean
fricas
res.9:=test (unify(P9,[])= [c = a,b = a])
\label{eq32} \mbox{\rm true} (32)
Type: Boolean
fricas
res.10:=test (unify(P10,[])= [c = d,b = d,a = d])
\label{eq33} \mbox{\rm true} (33)
Type: Boolean
fricas
res.11:=test (unify(P11,[])=[x= f(a,z),y= f(a,z),b= z])
\label{eq34} \mbox{\rm true} (34)
Type: Boolean
fricas
res.12:=test (unify(P12,[])=[a = z,x = h(g(z)),y = g(z)])
\label{eq35} \mbox{\rm true} (35)
Type: Boolean
fricas
res.13:=test (unify(P13,[]) case "failed")
\label{eq36} \mbox{\rm true} (36)
Type: Boolean
fricas
res.14:=test (unify(P14,[])= [x1 = g(x0,x0)])
\label{eq37} \mbox{\rm true} (37)
Type: Boolean
fricas
res.15:=test (unify(P15,[])=[x1 = g(x0,x0),x2 = g(g(x0,x0),g(x0,x0))])
\label{eq38} \mbox{\rm true} (38)
Type: Boolean
fricas
res.16:=test (unify(P16,[])= [x1 = g(x0,x0), x2 = g(g(x0,x0),g(x0,x0)), _
    x3 = g(g(g(x0,x0),g(x0,x0)),g(g(x0,x0),g(x0,x0)))])
\label{eq39} \mbox{\rm true} (39)
Type: Boolean
fricas
res.17:=true
\label{eq40} \mbox{\rm true} (40)
Type: Boolean
fricas
-------------
-- reduceWith
-------------
res.18:=test (reduceWith(P1,unify(P1,[])).1)
\label{eq41} \mbox{\rm true} (41)
Type: Boolean
fricas
res.19:=test (reduceWith(P2,unify(P2,[])).1)
\label{eq42} \mbox{\rm true} (42)
Type: Boolean
fricas
res.20:=test (reduceWith(P3,unify(P3,[])).1)
\label{eq43} \mbox{\rm true} (43)
Type: Boolean
fricas
res.21:=test (reduceWith(P4,unify(P4,[])).1)
\label{eq44} \mbox{\rm true} (44)
Type: Boolean
fricas
res.22:=test (reduceWith(P5,unify(P5,[])).1)
\label{eq45} \mbox{\rm true} (45)
Type: Boolean
fricas
res.23:=test (reduceWith(P9,unify(P9,[])).1)
\label{eq46} \mbox{\rm true} (46)
Type: Boolean
fricas
res.24:=test (reduceWith(P10,unify(P10,[])).1)
\label{eq47} \mbox{\rm true} (47)
Type: Boolean
fricas
res.25:=test (reduceWith(P11,unify(P11,[])).1)
\label{eq48} \mbox{\rm true} (48)
Type: Boolean
fricas
res.26:=test (reduceWith(P12,unify(P12,[])).1)
\label{eq49} \mbox{\rm true} (49)
Type: Boolean
fricas
res.27:=test (reduceWith(P14,unify(P14,[])).1)
\label{eq50} \mbox{\rm true} (50)
Type: Boolean
fricas
res.28:=test (reduceWith(P15,unify(P15,[])).1)
\label{eq51} \mbox{\rm true} (51)
Type: Boolean
fricas
res.29:=test (reduceWith(P16,unify(P16,[])).1)
\label{eq52} \mbox{\rm true} (52)
Type: Boolean
fricas
-- ***** Final result *****
reduce(_and,res)
\label{eq53} \mbox{\rm true} (53)
Type: Boolean



  Subject:   Be Bold !!
  ( 14 subscribers )  
Please rate this page: