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

# Edit detail for SandBoxINFSUM revision 1 of 1

 1 Editor: Kurt Pagani Time: 2018/07/28 20:58:06 GMT+0 Note:

changed:
-
)abbrev package UNIFY Unify
++ Author: Kurt Pagani
++ Date Created: Mon Feb 06 18:56:20 CET 2017
++ References:
++ Description:
++
Unify(X) : Exports == Implementation where

X: Join(ConvertibleTo InputForm, ExpressionSpace)
IF ==> InputForm
SEXP ==> SExpression

Exports ==  with

sexpr : X -> IF
++ Convert to InputForm
occursIn : (IF,IF) -> Boolean
++ Return true if ELT occurs in EXP at any level
cons : (IF,IF) -> IF
++ Cons
subst1 : (IF,IF,IF) -> IF
++ Substitute A for each occurrence of B in LST.
doSubst : (IF,IF) -> IF
++ Perform all substitutions in L on EXP in reverse order.
unify : (IF,IF) -> IF

failed:IF:=convert('failure)$IF sexpr(x:X):IF == convert(x)@IF occursIn(elt,exp) == elt=exp => true atom? exp => false occursIn(elt,car exp) or occursIn(elt,cdr exp) cons(a:IF,b:IF):IF == s:SExpression:=CONS(a,b)$Lisp
convert(s)$IF subst1(a:IF,b:IF,lst:IF):IF == null? lst => lst lst=b => a atom? lst => lst b=car lst => cons(a,subst1(a,b,cdr lst)) atom? car lst => cons(car lst, subst1(a,b,cdr lst)) cons(subst1(a,b,car lst),subst1(a,b,cdr lst)) doSubst(exp:IF,l:IF):IF == null? l => exp a:=car l subst1(car a, car cdr a, doSubst(exp,cdr l)) variable?(x:IF):Boolean == not atom? x => false symbol? x => true false addPair(term:IF,variable:IF,u:IF):IF == occursIn(variable,term) => failed cons(convert [term,variable],subst1(term,variable,u)) unify1(termlist1:IF,termlist2:IF,u:IF):IF == termlist1=termlist2 => u null? termlist1 or null? termlist2 => failed variable? termlist1 => addPair(termlist2,termlist1,u) variable? termlist2 => addPair(termlist1,termlist2,u) atom? termlist1 or atom? termlist2 => failed u:=unify1(doSubst(car termlist1,u),doSubst(car termlist2,u),u) u=failed => failed unify1(cdr termlist1,cdr termlist2,u) unify(literal1:IF,literal2:IF):IF == u:=convert([])$IF
if car literal1 = car literal2 then
unify1(cdr literal1,cdr literal2,u)
else
failed

\begin{axiom}

)set break resume
)set output algebra on
)set output tex off

X ==> Expression Integer
IF ==> InputForm
UFX ==> Unify(X)

REC ==> Record(inp:X,res:X)

r1:=[sum((-1)^(k?+1)/k?,k?=1..oo),log(2)]$REC r2:=[sum((-1)^(k?+1)/(2*k?-1),k?=1..oo),%pi/4]$REC

r3:=[sum(1/k?^p?,k?=1..oo),riemannZeta(p?)]$REC r4:=[sum((-1)^(k?+1)/k?^p?,k?=1..oo),(1-2^(1-p?))*riemannZeta(p?)]$REC

r5:=[sum(1/k?^2,k?=1..oo),%pi^2/6]$REC match(a,b) == r:=unify(a,b)$UFX
r='failure::IF => []
dr:=destruct r
ddr:=[destruct s for s in dr]
eq:=[symbol(s.1)::X=symbol(s.2)::X for s in ddr]

lookup(e,r) ==
test(e=r.inp) => r.res
ei:=e::IF
test(ei=(r.inp)::IF) => r.res
m:=match(ei,(r.inp)::IF)
subst(r.res,m)

i1:=sum((-1)^(n+1)/n,n=1..oo)
i2:=sum((-1)^(m+1)/m,m=1..N)
i3:=sum((-1)^(m^2+1)/m,m=1..N)
lookup(i2,r1)
ii3:=i3::IF
unify(ii3,(r1.inp)::IF)$UFX i4:=sum((-1)^(s+1)/(2*s-1),s=1..oo) lookup(i4,r2) --> %pi/4 i5:=sum(1/n^z,n=1..oo) lookup(i5,r3) --> riemannZeta(z) i6:=sum((-1)^(t+1)/t^s,t=1..oo) lookup(i6,r4) --> i7:=sum(1/m^2,m=1..oo) lookup(i7,r5) --> %pi^2/6 \end{axiom}  spad )abbrev package UNIFY Unify ++ Author: Kurt Pagani ++ Date Created: Mon Feb 06 18:56:20 CET 2017 ++ License: BSD ++ References: ++ Description: ++ Unify(X) : Exports == Implementation where X: Join(ConvertibleTo InputForm, ExpressionSpace) IF ==> InputForm SEXP ==> SExpression Exports == with sexpr : X -> IF ++ Convert to InputForm occursIn : (IF,IF) -> Boolean ++ Return true if ELT occurs in EXP at any level cons : (IF,IF) -> IF ++ Cons subst1 : (IF,IF,IF) -> IF ++ Substitute A for each occurrence of B in LST. doSubst : (IF,IF) -> IF ++ Perform all substitutions in L on EXP in reverse order. unify : (IF,IF) -> IF Implementation == IF add failed:IF:=convert('failure)$IF
sexpr(x:X):IF == convert(x)@IF
occursIn(elt,exp) ==
elt=exp => true
atom? exp => false
occursIn(elt,car exp) or occursIn(elt,cdr exp)
cons(a:IF,b:IF):IF ==
s:SExpression:=CONS(a,b)$Lisp convert(s)$IF
subst1(a:IF,b:IF,lst:IF):IF ==
null? lst => lst
lst=b => a
atom? lst => lst
b=car lst => cons(a,subst1(a,b,cdr lst))
atom? car lst => cons(car lst, subst1(a,b,cdr lst))
cons(subst1(a,b,car lst),subst1(a,b,cdr lst))
doSubst(exp:IF,l:IF):IF ==
null? l => exp
a:=car l
subst1(car a, car cdr a, doSubst(exp,cdr l))
variable?(x:IF):Boolean ==
not atom? x => false
symbol? x => true
false
occursIn(variable,term) => failed
cons(convert [term,variable],subst1(term,variable,u))
unify1(termlist1:IF,termlist2:IF,u:IF):IF ==
termlist1=termlist2 => u
null? termlist1 or null? termlist2 => failed
atom? termlist1 or atom? termlist2 => failed
u:=unify1(doSubst(car termlist1,u),doSubst(car termlist2,u),u)
u=failed => failed
unify1(cdr termlist1,cdr termlist2,u)
unify(literal1:IF,literal2:IF):IF ==
u:=convert([])$IF if car literal1 = car literal2 then unify1(cdr literal1,cdr literal2,u) else failed spad  Compiling FriCAS source code from file /var/lib/zope2.10/instance/axiom-wiki/var/LatexWiki/1957568863081842059-25px001.spad using old system compiler. UNIFY abbreviates package Unify ------------------------------------------------------------------------ initializing NRLIB UNIFY for Unify compiling into NRLIB UNIFY ****** Domain: X already in scope compiling exported sexpr : X -> InputForm Time: 0.01 SEC. compiling exported occursIn : (InputForm,InputForm) -> Boolean Time: 0 SEC. compiling exported cons : (InputForm,InputForm) -> InputForm Time: 0 SEC. compiling exported subst1 : (InputForm,InputForm,InputForm) -> InputForm Time: 0 SEC. compiling exported doSubst : (InputForm,InputForm) -> InputForm Time: 0 SEC. compiling local variable? : InputForm -> Boolean Time: 0 SEC. compiling local addPair : (InputForm,InputForm,InputForm) -> InputForm Time: 0 SEC. compiling local unify1 : (InputForm,InputForm,InputForm) -> InputForm Time: 0 SEC. compiling exported unify : (InputForm,InputForm) -> InputForm Time: 0 SEC. (time taken in buildFunctor: 0) ;;; *** |Unify| REDEFINED ;;; *** |Unify| REDEFINED Time: 0 SEC. Cumulative Statistics for Constructor Unify Time: 0.01 seconds --------------non extending category---------------------- .. Unify(#1) of cat (CATEGORY |package| (SIGNATURE |sexpr| ((|InputForm|) |#1|)) (SIGNATURE |occursIn| ((|Boolean|) (|InputForm|) (|InputForm|))) (SIGNATURE |cons| ((|InputForm|) (|InputForm|) (|InputForm|))) (SIGNATURE |subst1| ((|InputForm|) (|InputForm|) (|InputForm|) (|InputForm|))) (SIGNATURE |doSubst| ((|InputForm|) (|InputForm|) (|InputForm|))) (SIGNATURE |unify| ((|InputForm|) (|InputForm|) (|InputForm|)))) has no (|SExpressionCategory| (|String|) (|Symbol|) (|Integer|) (|DoubleFloat|)) finalizing NRLIB UNIFY Processing Unify for Browser database: --------constructor--------- --------(sexpr ((InputForm) X))--------- --->-->Unify((sexpr ((InputForm) X))): Improper first word in comments: Convert "Convert to InputForm" --------(occursIn ((Boolean) (InputForm) (InputForm)))--------- --->-->Unify((occursIn ((Boolean) (InputForm) (InputForm)))): Improper first word in comments: Return "Return \\spad{true} if ELT occurs in EXP at any level" --------(cons ((InputForm) (InputForm) (InputForm)))--------- --------(subst1 ((InputForm) (InputForm) (InputForm) (InputForm)))--------- --->-->Unify((subst1 ((InputForm) (InputForm) (InputForm) (InputForm)))): Improper first word in comments: Substitute "Substitute A for each occurrence of \\spad{B} in \\spad{LST}." --------(doSubst ((InputForm) (InputForm) (InputForm)))--------- --->-->Unify((doSubst ((InputForm) (InputForm) (InputForm)))): Improper first word in comments: Perform "Perform all substitutions in \\spad{L} on EXP in reverse order." --->-->Unify((unify ((InputForm) (InputForm) (InputForm)))): Not documented!!!! ; compiling file "/var/aw/var/LatexWiki/UNIFY.NRLIB/UNIFY.lsp" (written 28 JUL 2018 08:58:06 PM): ; /var/aw/var/LatexWiki/UNIFY.NRLIB/UNIFY.fasl written ; compilation finished in 0:00:00.049 ------------------------------------------------------------------------ Unify is now explicitly exposed in frame initial Unify will be automatically loaded when needed from /var/aw/var/LatexWiki/UNIFY.NRLIB/UNIFY fricas )set break resume  fricas )set output algebra on  fricas )set output tex off X ==> Expression Integer Type: Void fricas IF ==> InputForm Type: Void fricas UFX ==> Unify(X) Type: Void fricas REC ==> Record(inp:X,res:X) Type: Void fricas r1:=[sum((-1)^(k?+1)/k?,k?=1..oo),log(2)]$REC
oo         k? + 1
--+    (- 1)
(5)  [inp =  >      -----------, res = log(2)]
--+         k?
k? = 1
Type: Record(inp: Expression(Integer),res: Expression(Integer))
fricas
r2:=[sum((-1)^(k?+1)/(2*k?-1),k?=1..oo),%pi/4]$REC oo k? + 1 --+ (- 1) %pi (6) [inp = > -----------, res = ---] --+ 2 k? - 1 4 k? = 1 Type: Record(inp: Expression(Integer),res: Expression(Integer)) fricas r3:=[sum(1/k?^p?,k?=1..oo),riemannZeta(p?)]$REC
oo
--+      1
(7)  [inp =  >      ----, res = riemannZeta(p?)]
--+      p?
k? = 1  k?
Type: Record(inp: Expression(Integer),res: Expression(Integer))
fricas
r4:=[sum((-1)^(k?+1)/k?^p?,k?=1..oo),(1-2^(1-p?))*riemannZeta(p?)]$REC (8) oo k? + 1 --+ (- 1) [inp = > -----------, --+ p? k? = 1 k? - p? + 1 res = - riemannZeta(p?)2 + riemannZeta(p?)] Type: Record(inp: Expression(Integer),res: Expression(Integer)) fricas r5:=[sum(1/k?^2,k?=1..oo),%pi^2/6]$REC
oo                  2
--+     1         %pi
(9)  [inp =  >      ---, res = ----]
--+      2          6
k? = 1  k?
Type: Record(inp: Expression(Integer),res: Expression(Integer))
fricas
match(a,b) ==
r:=unify(a,b)$UFX r='failure::IF => [] dr:=destruct r ddr:=[destruct s for s in dr] eq:=[symbol(s.1)::X=symbol(s.2)::X for s in ddr] Type: Void fricas lookup(e,r) == test(e=r.inp) => r.res ei:=e::IF test(ei=(r.inp)::IF) => r.res m:=match(ei,(r.inp)::IF) subst(r.res,m) Type: Void fricas i1:=sum((-1)^(n+1)/n,n=1..oo) oo k? + 1 --+ (- 1) (12) > ----------- --+ k? k? = 1 Type: Expression(Integer) fricas i2:=sum((-1)^(m+1)/m,m=1..N) N m + 1 --+ (- 1) (13) > ---------- --+ m m = 1 Type: Expression(Integer) fricas i3:=sum((-1)^(m^2+1)/m,m=1..N) 2 N m + 1 --+ (- 1) (14) > ----------- --+ m m = 1 Type: Expression(Integer) fricas lookup(i2,r1) fricas Compiling function match with type (InputForm, InputForm) -> List( Equation(Expression(Integer))) fricas Compiling function lookup with type (Expression(Integer), Record(inp : Expression(Integer),res: Expression(Integer))) -> Expression( Integer) (15) log(2) Type: Expression(Integer) fricas ii3:=i3::IF (16) (%defsum (/ (^ - 1 (+ (^ %S 2) 1)) %S) %S m 1 N) Type: InputForm fricas unify(ii3,(r1.inp)::IF)$UFX
(17)  failure
Type: InputForm
fricas
i4:=sum((-1)^(s+1)/(2*s-1),s=1..oo)
oo         k? + 1
--+    (- 1)
(18)   >      -----------
--+      2 k? - 1
k? = 1
Type: Expression(Integer)
fricas
lookup(i4,r2) --> %pi/4
%pi
(19)  ---
4
Type: Expression(Integer)
fricas
i5:=sum(1/n^z,n=1..oo)
oo
--+    1
(20)   >     --
--+    z
n = 1  n
Type: Expression(Integer)
fricas
lookup(i5,r3) --> riemannZeta(z)
(21)  riemannZeta(z)
Type: Expression(Integer)
fricas
i6:=sum((-1)^(t+1)/t^s,t=1..oo)
oo         t + 1
--+   (- 1)
(22)   >     ----------
--+        s
t = 1      t
Type: Expression(Integer)
fricas
lookup(i6,r4) -->
- s + 1
(23)  - riemannZeta(s)2        + riemannZeta(s)
Type: Expression(Integer)
fricas
i7:=sum(1/m^2,m=1..oo)
oo
--+     1
(24)   >      ---
--+      2
k? = 1  k?
Type: Union(Expression(Integer),...)
fricas
lookup(i7,r5) --> %pi^2/6
2
%pi
(25)  ----
6
Type: Expression(Integer)