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
 (1)
Type: BasicOperator?
fricas
f:=operator 'f
 (2)
Type: BasicOperator?
fricas
g:=operator 'g
 (3)
Type: BasicOperator?
fricas
h:=operator 'h
 (4)
Type: BasicOperator?
fricas
m:=operator 'm
 (5)
Type: BasicOperator?
fricas
N:=29 -- number of tests
 (6)
Type: PositiveInteger?
fricas
-----------------------------------------
--
Type: List Equation Expression Integer
fricas
-----------------------------------------
P1:=[f(g(x),x) = f(y,a)]
 (7)
Type: List(Equation(Expression(Integer)))
fricas
P2:=[f(x,h(x),y) = f(g(z), u, z)]
 (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))]
 (9)
Type: List(Equation(Expression(Integer)))
fricas
P4:=[f(x, b, g(z)) = f(f(y), y, g(u))]
 (10)
Type: List(Equation(Expression(Integer)))
fricas
P5:=[p(a,x,h(g(z))) = p(z,h(y),h(y))]
 (11)
Type: List(Equation(Expression(Integer)))
fricas
P6:=[p(f(a),g(x)) = p(y,y)]
 (12)
Type: List(Equation(Expression(Integer)))
fricas
P7:=[p(x,x) = p(y,f(y))]
 (13)
Type: List(Equation(Expression(Integer)))
fricas
P8:=[sin(x+y) = sin(u^2+v^2)]
 (14)
Type: List(Equation(Expression(Integer)))
fricas
P9:=[p(c,b)=p(a,c),p(a,b)=p(b,c)]
 (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)]
 (16)
Type: List(Equation(Expression(Integer)))
fricas
P11:=[g(x,f(x,b))=g(f(a,b),f(y,z))]
 (17)
Type: List(Equation(Expression(Integer)))
fricas
P12:=[p(a,x,h(g(z)))=p(z,h(y),h(y))]
 (18)
Type: List(Equation(Expression(Integer)))
fricas
P13:=[p(f(a),g(x))=p(y,y)]
 (19)
Type: List(Equation(Expression(Integer)))
fricas
P14:=[f(x1)=f(g(x0,x0))]
 (20)
Type: List(Equation(Expression(Integer)))
fricas
P15:=[f(x1,x2)=f(g(x0,x0),g(x1,x1))]
 (21)
Type: List(Equation(Expression(Integer)))
fricas
P16:=[f(x1,x2,x3)=f(g(x0,x0),g(x1,x1),g(x2,x2))]
 (22)
Type: List(Equation(Expression(Integer)))
fricas
-- Result list
res:List(Boolean):=[false for i in 1..N]
 (23)
Type: List(Boolean)
fricas
--------
-- unify
--------
res.1:=test (unify(P1,[])=[y= g(a),x= a])
 (24)
Type: Boolean
fricas
res.2:=test (unify(P2,[])=[x= g(z),u= h(g(z)),y= z])
 (25)
Type: Boolean
fricas
res.3:=test (unify(P3,[])=[a= u,x= s,w= f(c),v= s,y= c])
 (26)
Type: Boolean
fricas
res.4:=test (unify(P4,[])=[x= f(y),b= y,z= u])
 (27)
Type: Boolean
fricas
res.5:=test (unify(P5,[])=[a= z,x= h(g(z)),y= g(z)])
 (28)
Type: Boolean
fricas
res.6:=test (unify(P6,[]) case "failed")
 (29)
Type: Boolean
fricas
res.7:=test (unify(P7,[]) case "failed")
 (30)
Type: Boolean
fricas
res.8:=test (unify(P8,[])=[y + x = v^2  + u^2 ])
 (31)
Type: Boolean
fricas
res.9:=test (unify(P9,[])= [c = a,b = a])
 (32)
Type: Boolean
fricas
res.10:=test (unify(P10,[])= [c = d,b = d,a = d])
 (33)
Type: Boolean
fricas
res.11:=test (unify(P11,[])=[x= f(a,z),y= f(a,z),b= z])
 (34)
Type: Boolean
fricas
res.12:=test (unify(P12,[])=[a = z,x = h(g(z)),y = g(z)])
 (35)
Type: Boolean
fricas
res.13:=test (unify(P13,[]) case "failed")
 (36)
Type: Boolean
fricas
res.14:=test (unify(P14,[])= [x1 = g(x0,x0)])
 (37)
Type: Boolean
fricas
res.15:=test (unify(P15,[])=[x1 = g(x0,x0),x2 = g(g(x0,x0),g(x0,x0))])
 (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)))])
 (39)
Type: Boolean
fricas
res.17:=true
 (40)
Type: Boolean
fricas
-------------
-- reduceWith
-------------
res.18:=test (reduceWith(P1,unify(P1,[])).1)
 (41)
Type: Boolean
fricas
res.19:=test (reduceWith(P2,unify(P2,[])).1)
 (42)
Type: Boolean
fricas
res.20:=test (reduceWith(P3,unify(P3,[])).1)
 (43)
Type: Boolean
fricas
res.21:=test (reduceWith(P4,unify(P4,[])).1)
 (44)
Type: Boolean
fricas
res.22:=test (reduceWith(P5,unify(P5,[])).1)
 (45)
Type: Boolean
fricas
res.23:=test (reduceWith(P9,unify(P9,[])).1)
 (46)
Type: Boolean
fricas
res.24:=test (reduceWith(P10,unify(P10,[])).1)
 (47)
Type: Boolean
fricas
res.25:=test (reduceWith(P11,unify(P11,[])).1)
 (48)
Type: Boolean
fricas
res.26:=test (reduceWith(P12,unify(P12,[])).1)
 (49)
Type: Boolean
fricas
res.27:=test (reduceWith(P14,unify(P14,[])).1)
 (50)
Type: Boolean
fricas
res.28:=test (reduceWith(P15,unify(P15,[])).1)
 (51)
Type: Boolean
fricas
res.29:=test (reduceWith(P16,unify(P16,[])).1)
 (52)
Type: Boolean
fricas
-- ***** Final result *****
reduce(_and,res)
 (53)
Type: Boolean

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