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

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
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
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.01 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.02 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 09:32:44 PM):
; /var/aw/var/LatexWiki/UNIFY.NRLIB/UNIFY.fasl written ; compilation finished in 0:00:00.050 ------------------------------------------------------------------------ Unify is now explicitly exposed in frame initial Unify will be automatically loaded when needed from /var/aw/var/LatexWiki/UNIFY.NRLIB/UNIFY

Test flavours

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
SPM ==> Unify(X)
Type: Void
fricas
p:=convert(p)$InputForm
(4) p
Type: InputForm
fricas
x:=x::IF
(5) x
Type: InputForm
fricas
f:=f::IF
(6) f
Type: InputForm
fricas
g:=g::IF
(7) g
Type: InputForm
fricas
h:=h::IF
(8) h
Type: InputForm
fricas
a:=a::IF
(9) a
Type: InputForm
fricas
b:=b::IF
(10) b
Type: InputForm
fricas
y:=y::IF
(11) y
Type: InputForm
fricas
z:=z::IF
(12) z
Type: InputForm
fricas
l1:=convert([p,x,convert [f,a]])$IF
(13) (p x (f a))
Type: InputForm
fricas
l2:=convert([p,b,y])$IF
(14) (p b y)
Type: InputForm
fricas
l3:=convert([p,convert [f,x],convert [g,a,y]])$IF
(15) (p (f x) (g a y))
Type: InputForm
fricas
l4:=convert([p,convert [f,convert [h,b]],convert [g,x,y]])$IF
(16) (p (f (h b)) (g x y))
Type: InputForm
fricas
l5:=convert([p,x])$IF
(17) (p x)
Type: InputForm
fricas
l6:=convert([p,convert [f,x]])$IF
(18) (p (f x))
Type: InputForm
fricas
l7:=convert([p,x,convert [f,y],x])$IF 
(19) (p x (f y) x)
Type: InputForm
fricas
l8:=convert([p,z,convert [f,z],a])$IF 
(20) (p z (f z) a)
Type: InputForm
fricas
r1:=unify(l1,l2)$SPM  -- (((f a) y) (b x))
(21) (((f a) y) (b x))
Type: InputForm
fricas
r2:=unify(l3,l4)$SPM  -- (((h b) a) ((h b) x)) , only if variable? a
(22) (((h b) a) ((h b) x))
Type: InputForm
fricas
r3:=unify(l5,l6)$SPM  -- not-unifiable
(23) failure
Type: InputForm
fricas
r4:=unify(l7,l8)$SPM  --  ((a z) (a y) (a x))
(24) ((a z) (a y) (a x))
Type: InputForm
fricas
s11:=doSubst(l1,r1)$SPM
(25) (p b (f a))
Type: InputForm
fricas
s21:=doSubst(l2,r1)$SPM
(26) (p b (f a))
Type: InputForm
fricas
s74:=doSubst(l7,r4)$SPM
(27) (p a (f a) a)
Type: InputForm
fricas
s84:=doSubst(l8,r4)$SPM
(28) (p a (f a) a)
Type: InputForm
fricas
L1:=exp(-r^2+s)::IF
(29) (exp (+ s (* - 1 (^ r 2))))
Type: InputForm
fricas
L2:=exp(-r^2+q)::IF
(30) (exp (+ (* - 1 (^ r 2)) q))
Type: InputForm
fricas
unify(L1,L2)$SPM  -- oweeh
(31) (((* - 1 (^ r 2)) q) ((* - 1 (^ r 2)) s))
Type: InputForm
fricas
unify(x+y,y+x)$SPM
(32) ((y x))
Type: InputForm




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