title: Efficient Scala Implementation of Substitutions Merge
body: <p>Assume we have two substitutions, each of which is a list of pairs, how can we merge them efficiently? The pair size in one list is usually large (most are about 100, some are 5000 or larger).
  More formal definition:</p>
  
  <ul>
  <li>Substitution ::= List[Pair[Term]]</li>
  <li>Term ::= Variable | Constant</li>
  <li>Variable ::= Int of format :0xXXXXXXXXXXXX11 // for example: v1=7,
  v2=11, v3=15, ....</li>
  <li>Constant ::= Int of format :0xXXXXXXXXXXXX10 // for example: c1=6, c2=10, c3=14, ....</li>
  </ul>
  
  <p>Condition:
  One pair only maps a variable to a constant, or a variable to another variable. It can't map a constant to another constant or a variable.</p>
  
  <p>Note:</p>
  
  <ol>
  <li>It is possible that two substitutions can't merge: for example. merge List( (7, 6), (11, 10) and List(7, 11)  /* {v1->c1, v2->c2} and {v1->v2} */</li>
  <li>Input substitutions are always valid, meaning condition holds at the beginning. There is no identicial pair.</li>
  <li>For simplicity, variables appear in the left part of any pair cannot be appeared in the right part of any pair. For any two pairs, the left parts are always different.</li>
  </ol>
  
  <p>Question:</p>
  
  <ol>
  <li>What is an efficient encoding for a term.</li>
  <li>What is an efficient encoding for a substitution.</li>
  <li>What is the best way to merge two substitution.</li>
  </ol>
  
  <p>Thank you!</p>
  
  <p><strong>UPDATED</strong> Algorithm Description(merge one new pair p=(s, t) into a list (L) )</p>
  
  <ol>
  <li>If in the new pair p, s is a constant and t is a variable, then change to (v, c);</li>
  <li>If the new pair is identical s=t, then remove and DONE;</li>
  <li>If the new pair is mapping a constant to another constant(c1&lt;>c2), then fail and DONE;</li>
  <li>If t exists in the left part of one pair in the substitution L, replace it by the right part of that pair;</li>
  <li>If s exists in the left part of one pair, save the right part of the pair as t2 and goto 7; if no such pair, goto 6;
  6 If the right part of a pair in the substitution is equal to s, then replace it by t; Adds (s, t) to the list L; and DONE;</li>
  <li>If (s, t) is already in list L, return L and DONE;</li>
  <li>If t and t2 are constants, then fail and DONE;</li>
  <li>If t is a constant goto 10 else goto 11;</li>
  <li>If the right part of a pair in the substitution is equal to t2, then replace it by t; Adds (t2, t) to the list L; and DONE;</li>
  <li>If the right part of a pair in the substitution is equal to t, then replace it by t2; Adds (t, t2) to the list L; and DONE;</li>
  </ol>
  
  <p>Basic Term Definition: Term may use some other data structure.</p>
  
  <pre><code>object Terms {
      type Term = Int
      @inline final def isV( t : Term ) = ((t &amp; 3) == 0x3)
      @inline final def isC(t : Term) = ((t &amp; 3) == 0x2)
  }
  object MERGEException extends Exception
  </code></pre>
  
  <p>Main Scala Code:</p>
  
  <pre><code>final case class Subst( _data : List[ Tuple2[Int, Int] ] ) {
      type Term = Int
      type PairType = Tuple2[Term, Term]
      type ListType = List[PairType]
  
      // Find a pair in the list, which the first element matches the query t
      // Returns the second element if found; t if no match
      private final def find(t : Term, list : ListType) : Term =
          list match {
              case List() =&gt; t
              case h :: list2 =&gt;
                  val cmp = h._1 - t
                  if(cmp &lt; 0) find(t, list2)
                  else if(cmp == 0) h._2
                  else t
          }
      // Replace s for t in the substitution (right part)
      private final def replace_helper(s : Term, t : Term, list : ListType) : ListType =
          list.map( h =&gt; if(h._2 equals s) (h._1, t) else h).distinct
      // Assume: s in not in the list
      private final def add(s : Term, t : Term, list : ListType) : ListType = {
          var wlist = list
          var rlist : ListType = List.empty
          while(wlist != List.empty) {
              val h = wlist.head
              if(h._1 &lt; s) {
                  rlist = rlist ::: List(h)
                  wlist = wlist.tail
              } else
                  return rlist ::: ( (s, t) :: wlist )
          }
          return rlist ::: List( (s, t) )
      }
      private final def merge_helper(e : PairType, list : ListType) : ListType = {
          // Orient the pair of SubTerms
          def orient(s : Term, t : Term) : PairType = 
          if( Terms.isC(s) &amp;&amp; !Terms.isC(t) ) (t, s)
              else (s, t)
  
          // Orientation
          var (s, t) = orient(e._1, e._2)
          // Remove identical pair
          if(s equals t) return list
          // Constant
          if(Terms.isC(s) &amp;&amp; Terms.isC(t)) throw MERGEException
  
          if(list == List.empty) return List((s, t))
  
          // If t exists in the left part of one pair, replace it by the right part of the pair
          t = find(t, list)
          if(s equals t) list
          // now t is not in the left part of any pair
  
          val t2 = find(s, list)
          if(t2 equals s) {
              // s doesn't appear in the left part of existed elements
              add( s, t, replace_helper(s, t, list) )
          } else {
              // s appears in the left part of existed elements
              if( t2 equals t ) list
              else {
                  // s appear in the left part of existed elements
                  // then s doesn't appear in the right part of existed elements
                  // and isDirected = false
                  //merge_helper( (t, t2), list, isDirected )
                  if(Terms.isC(t) &amp;&amp; Terms.isC(t2)) throw MERGEException
                  else if(Terms.isC(t)) {
                      add( t2, t, replace_helper(t2, t, list) )
                  }
                  else add( t, t2, replace_helper(t, t2, list) )
              }
          }
      }
      // Merge a pair into the substitution
      final def merge( e : PairType ) : Option[Subst] = {
          try {
              val ret = merge_helper(e, _data)
              return Some( Subst(ret) )
          } catch {
              case MERGEException =&gt; return None
          }
      }
      // Union a new substitution together
      final def union(s : Subst) : Option[Subst] = {
          try {
              if(_data.isEmpty) return Some(s)
              else if(s.isEmpty) return Some(this)
              else {
                  var ret = _data
                  var Subst(slist) = s
                  slist.foreach( e =&gt;
                      ret = merge_helper(e, ret) )
                  return Some( Subst(ret) )
              }
          } catch {
              case e =&gt; return None
          }
      }
      final def isEmpty = _data.isEmpty
  }
  </code></pre>
  
  <p>Testing Code:</p>
  
  <pre><code>// Test case 1
  val s1 = Subst( List( (7, 6), (11, 10) ) )  // {v1-&gt;c1, v2-&gt;c2}
  val s2 = Subst( List( (7, 11) ) )  // {v1-&gt;v2}
  val s3 = s1.union(s2)  // none
  // Test case 2
  val s12 = Subst( List( (7, 6), (11, 6), (23, 19), (27, 15), (31, 35) ) ) // {v1-&gt;c1, v2-&gt;c1, v5-&gt;v4, v6-&gt;v3, v7-&gt;v8}
  val s22 = Subst( List( (11, 7), (15, 7), (19, 10) ) ) // {v2-&gt;v1, v3-&gt;v1, v4-&gt;c2}
  val s32 = s12.union(s22)  // Some( Subst( List( (7, 6), (11, 6), (15, 6), (19, 10), (23, 10), (27, 6), (31, 35) ) ) )
  </code></pre>