)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

   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

)set break resume
 

)set output algebra on
 

)set output tex off

X ==> Expression Integer

IF ==> InputForm

SPM ==> Unify(X)

p:=convert(p)$InputForm

   (4)  p

x:=x::IF

   (5)  x

f:=f::IF

   (6)  f

g:=g::IF

   (7)  g

h:=h::IF

   (8)  h

a:=a::IF

   (9)  a

b:=b::IF

   (10)  b

y:=y::IF

   (11)  y

z:=z::IF

   (12)  z

l1:=convert([p,x,convert [f,a]])$IF

   (13)  (p x (f a))

l2:=convert([p,b,y])$IF

   (14)  (p b y)

l3:=convert([p,convert [f,x],convert [g,a,y]])$IF

   (15)  (p (f x) (g a y))

l4:=convert([p,convert [f,convert [h,b]],convert [g,x,y]])$IF

   (16)  (p (f (h b)) (g x y))

l5:=convert([p,x])$IF

   (17)  (p x)

l6:=convert([p,convert [f,x]])$IF

   (18)  (p (f x))

l7:=convert([p,x,convert [f,y],x])$IF 

   (19)  (p x (f y) x)

l8:=convert([p,z,convert [f,z],a])$IF 

   (20)  (p z (f z) a)

r1:=unify(l1,l2)$SPM  -- (((f a) y) (b x))

   (21)  (((f a) y) (b x))

r2:=unify(l3,l4)$SPM  -- (((h b) a) ((h b) x)) , only if variable? a

   (22)  (((h b) a) ((h b) x))

r3:=unify(l5,l6)$SPM  -- not-unifiable

   (23)  failure

r4:=unify(l7,l8)$SPM  --  ((a z) (a y) (a x))

   (24)  ((a z) (a y) (a x))

s11:=doSubst(l1,r1)$SPM

   (25)  (p b (f a))

s21:=doSubst(l2,r1)$SPM

   (26)  (p b (f a))

s74:=doSubst(l7,r4)$SPM

   (27)  (p a (f a) a)

s84:=doSubst(l8,r4)$SPM

   (28)  (p a (f a) a)

L1:=exp(-r^2+s)::IF

   (29)  (exp (+ s (* - 1 (^ r 2))))

L2:=exp(-r^2+q)::IF

   (30)  (exp (+ (* - 1 (^ r 2)) q))

unify(L1,L2)$SPM  -- oweeh

   (31)  (((* - 1 (^ r 2)) q) ((* - 1 (^ r 2)) s))

unify(x+y,y+x)$SPM

   (32)  ((y x))