Unification in Maude 2.4
===========================

Order sorted unification is supported for a subset of the theories
supported by regular rewriting.

The object level unify command has the syntax:

 unify [<limit>] in <module> : <term> =? <term> .

As usual the
  [<limit>]
and
  in <module> :
parts are optional with unbounded and current module being assumed
respectively if they are omitted. Unification respects subsort
declarations but ignores membership axioms.
Supported theories are free, commutative and associative-commutative
together with the iter representation used for Nats.  Further more
ground subterms may be built from any symbols. Unifiers are always
expressed using fresh variables of the form: #n:Sort
Variables of this form should not appear in the unificands.
Some examples:

*** order sorted free theory unification is not unitary
fmod TEST is
  pr NAT .
  op f : Nat Nat -> Nat .
  op f : NzNat Nat -> NzNat .
  op f : Nat NzNat -> NzNat .
endfm

unify f(X:Nat, Y:Nat) ^ B:NzNat =? A:NzNat ^ f(Y:Nat, Z:Nat) .

*** quite modest AC unification problems can produce a large number of
*** unifiers 
unify [100] in NAT :
  X:Nat + X:Nat + Y:Nat =? A:Nat + B:Nat + C:Nat .

*** built-in constants are handled; built in functions are not
*** evaluated 
unify in CONVERSION :
  X:String < "foo" + Y:Char =?
  Z:String + string(pi) < "foo" + Z:String .

*** using forbidden variable names in unificands fails with a warning
unify in NAT : X:Nat ^ #1:Nat =? #2:Nat .

fmod TEST2 is
  pr NAT .
  op f : Nat Nat -> Nat [assoc] .
endfm

*** using of a symbol from an unsupported theory above a non-gound
*** term fails with a warning
unify f(f(X:Nat, Y:Nat), Z:Nat) =? f(A:Nat, B:Nat) .

*** all symbols are allowed in ground terms
unify X:Nat + f(41, 42) =? Y:Nat + f(41, 42) .

*** order sorted unification is efficient on the iter representation
mod ITER is
  sorts NzEvenNat EvenNat OddNat NzNat Nat EvenInt OddInt NzInt Int .

  subsorts OddNat < OddInt NzNat < NzInt < Int .
  subsorts EvenNat < EvenInt Nat < Int .
  subsorts NzEvenNat < NzNat EvenNat < Nat .

  op 0 : -> EvenNat .

  op s : EvenNat -> OddNat [iter] .
  op s : OddNat -> NzEvenNat [iter] .
  op s : Nat -> NzNat [iter] .

  op s : EvenInt -> OddInt [iter] .
  op s : OddInt -> EvenInt [iter] .
  op s : Int -> Int [iter] .

  op _+_ : Int Int -> Int [comm gather (E e)] .
  op _+_ : OddInt OddInt -> EvenInt [ditto] .
  op _+_ : EvenInt EvenInt -> EvenInt [ditto] .
  op _+_ : OddInt EvenInt -> OddInt [ditto] .

  op _+_ : Nat Nat -> Nat [ditto] .
  op _+_ : Nat NzNat -> NzNat [ditto] .
  op _+_ : OddNat OddNat -> NzEvenNat [ditto] .
  op _+_ : NzEvenNat EvenNat -> NzEvenNat [ditto] .
  op _+_ : EvenNat EvenNat -> EvenNat [ditto] .
  op _+_ : OddNat EvenNat -> OddNat [ditto] .
endfm

unify s^1000000(X:OddNat) =? s^100000000001(Y:Int) .
unify s^1000000(X:OddNat) =? s^100000000001(Y:Int + Z:Int + W:Int) .

Assuming there is no limit, a complete set of unifiers will be
generated however there is no guarantee that all unifiers will be most
general.

In the metalevel unification is reflected by two descent functions:
  op metaUnify : Module UnificationProblem Nat Nat ~> UnificationPair? .
and
  op metaDisjointUnify : Module UnificationProblem Nat Nat ~> UnificationTriple? .
These work on more general simultaneous unification problems
constructed from the signature:
  sorts UnificandPair UnificationProblem .
  subsort UnificandPair < UnificationProblem .
  op _=?_ : Term Term -> UnificandPair [ctor prec 71] .
  op _/\_ : UnificationProblem UnificationProblem -> UnificationProblem
    [ctor assoc comm prec 73] .

The difference between the two functions is that metaDisjointUnify()
assumes that the variables in the left and right hand unificands are
to be considered  disjoint and it generates a pair of substitutions,
one for left unificands and one for right unificands. This is the
usual case, in critical pair checking and narrowing.

Since it is convenient to reuse variable names from unifiers in new
problems, for example in narrowing, this is allowed via the 3rd
argument, which is the largest number n appearing in a unificand
metavariable of the form: '#n:Sort
Metavariable in the unifiers will be numbered from n+1.

As is normal for descent functions the last argument is used to select
which result is wanted, starting from 0. Caching is used so that if
unifier i has just been returned, requesting unifier i+1 is an
incremental computation.

Results are returned using the constructors:
  op {_,_} : Substitution Nat -> UnificationPair [ctor] .
and
  op {_,_,_} : Substitution Substitution Nat -> UnificationTriple [ctor] .
as appropriate for the descent function. The final Nat argument is the
largest n occurring in a fresh metavariable of the form: '#n:Sort

When no unifier with a given index exists, 
  op noUnifier : -> UnificationPair? [ctor] .
or
  op noUnifier : -> UnificationTriple? [ctor] .
is returned as appropriate for the descent function.

Some examples:

*** variable names allow arbitrarily large numbering
reduce in META-LEVEL :
  metaUnify(['NAT],
            '_+_['X:Nat, 'Y:Nat] =? '_+_['A:Nat, 'B:Nat],
	    100000000000000000000, 0) .

*** using variable names in unifications with larger numbers than
*** declared by the the 3rd argument generates a warning and no
*** reduction.
reduce in META-LEVEL :
  metaUnify(['NAT],
            '_+_['X:Nat, 'Y:Nat] =? '_+_['#1:Nat, 'Y:Nat],
	    0, 0) .