login  home  contents  what's new  discussion  bug reports     help  links  subscribe  changes  refresh  edit

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.03 SEC.
compiling local termReduce : Equation Expression R -> Union(List Equation Expression R,failed) Time: 0.03 SEC.
compiling local app? : Expression R -> Boolean Time: 0.01 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.01 SEC.
compiling local occurs : (Expression R,Expression R) -> Boolean Time: 0.01 SEC.
compiling exported unify : (List Equation Expression R,List Equation Expression R) -> Union(List Equation Expression R,failed) Time: 0.02 SEC.
(time taken in buildFunctor: 0)
;;; *** |EquationalReasoning| REDEFINED
;;; *** |EquationalReasoning| REDEFINED Time: 0 SEC.
Cumulative Statistics for Constructor EquationalReasoning Time: 0.13 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 23 DEC 2016 03:29:37 AM):
; /var/aw/var/LatexWiki/EQREASON.NRLIB/EQREASON.fasl written ; compilation finished in 0:00:00.058 ------------------------------------------------------------------------ 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)
fricas
f:=operator 'f

\label{eq2}f(2)
fricas
g:=operator 'g

\label{eq3}g(3)
fricas
h:=operator 'h

\label{eq4}h(4)
fricas
m:=operator 'm

\label{eq5}m(5)
fricas
N:=29 -- number of tests

\label{eq6}29(6)
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 !!
  ( 13 subscribers )  
Please rate this page: