== A second attempt ==

To solve  {{{(C implies t1=t2)}}} with respect to Ax

 1. First:
   1. We interpret Ax /\ C as a rewrite system (from left to right)   and 
   2. perform completion until the rewrite system is confluent.
 2. We exhaustively apply rewrite rules on t1 and t2, written t1 -->* t1' and t2 -->* t2' and check that t1' and t2' are syntactically equivalent.


Step (1.2) is new and crucial. For confluent rewrite systems the
checking step (2) will work fine (we also need termination of course).
But how do we now that completion will succeed?
The important condition is to guarantee that Ax is confluent (and
terminating) then completion will be successful (i.e. terminated
and produce a confluent rewrite system).

Let's take a look at our running example.
{{{
(forall a. S [a] = [S a]) /\      (R1) -- axioms
(T Int = Int)                     (R2)

 /\

(T [Int] = S [Int]) /\            (R3) -- local assumptions
(T Int = S Int)                   (R4)
}}}
The axioms are clearly confluent
but there's a critical pair between (R2,R4).

Completion yields

{{{
(S Int = Int)                     (R5)
}}}
Now, we can verify that (T [Int] = [Int])

by executing

{{{
T [Int] -->* [Int]       (R3,R1,R5)

[Int] -->* [Int]
}}}

The completion method in more detail.

=== There are two kinds of critical pairs ===

 * Axiom vs local assumption, see (R2,R4) above
 * Local assumption vs local assumption. For example,
{{{
  T Int = S Int  /\ 
  T Int = R Int
}}}
  Completion yields
{{{
  S Int = R Int
  R Int = S Int
}}}

NOTE: Axiom vs axiom impossible cause axiom set is confluent


Towards establishing a connection between completion and CHR [What is CHR? -samb] derivation steps 


NOTE: 

There's a straightforward translation from type functions to constraints. For each n-ary function symbol T, we introduce a n+1-ary constraint symbol T. Thus, we can represent 
{{{T Int = Int}}}  as
{{{ T Int a /\ a=Int}}}
For example, {{{T Int = S Int}}} is represented by 
{{{T Int a /\ S Int b /\ a=b}}}


We can verify that the completion method success by showing that each critical pair arises in the `corresponding' CHR derivation (this derivation terminates if the axiom system is confluent and terminating, hence, we'll only encounter a finite number of critical pairs, hence, completion terminates).

Recall the critical pair (axioms vs local assumption) from above
{{{
T Int = Int     -- axiom
T Int = S Int  -- local assumption
}}}
In the CHR world, we'll represent both as
{{{
T Int a <==> a=Int         -- axiom turned into CHR

T Int b /\ S Int c /\ b=c  -- local assumption turned into CHR
                           -- constraints
}}}
In the CHR world, we find that
{{{
    T Int b /\ S Int c /\ b=c
--> b=Int /\ S Int c /\ b=c      -- apply CHR
<--> b=Int /\ c=Int /\ S Int Int -- equivalence transformation
                                 -- apply mgu
}}}
directly corresponds to 
{{{
S Int = Int
}}}
generated by our completion method

Recall the critical pair (local assumption vs local assumption)
{{{
  T Int = S Int  /\ 
  T Int = R Int
}}}
represented in the CHR world as
{{{
 T Int a /\ S Int b /\ a=b /\
 T Int c /\ R Int d /\ c=d
}}}
In the CHR world, we find that
{{{
    T Int a /\ S Int b /\ a=b /\
    T Int c /\ R Int d /\ c=d
-->T Int a /\ S Int b /\ a=b /\  
   c=a /\ R Int d /\ c=d

      -- apply FD rule
      -- T a b /\ T a c ==> b=c

<--> T Int a /\ S Int a /\ R Int a /\
     a=b, c=a, d=a
}}}
directly corresponds to
{{{
S Int = R Int
R Int = S Int
}}}

The general cases are as follows.

==== Axiom vs local assumption case ====

{{{
forall as. (T t1 ... tn = s)  -- axiom

T t1' ... tn' = s'            -- local assumption
}}}
where exist phi, dom(phi)=as such that phi(ti) = ti' for i=1,...,n


completion yields
{{{
    s' = phi(s)
    phi(s) = s'       
}}}

NOTE: We may need both orientation see above example.
We assume that symbol t refers to types NOT containing type functions and s refers to types which may contain type functions (can be lifted, more below)


Explaining completion in terms of CHRs.
Above translates to
{{{
T t1 ... tn b <==> C

T t1' ... tn' b' /\ C'
}}}
where  s is translated to (C | b) and s' is translated to (C | b')

(see above where each type function type is represented by
a variable under some CHR constraints)

The type functions
{{{
    s' = phi(s)
    phi(s) = s'       
}}}
resulting from completion 'appear' in the CHR derivation
(i.e. the operational effect is the same)
{{{
     T t1' ... tn' b' /\ C'    -- apply CHR
--> b=b', phi(C) /\ C'
}}}

==== Local assumption vs local assumption ====

{{{
T t1 ... tn = s1
T t1 ....tn = sn
}}}

completion yields
{{{
  s1 = s2
  s2 = s1
}}}
In the CHR world, above represented by

{{{
T t1 ... tn a /\ C1
T t1 ....tn b /\ C2
}}}
where s1 translated to (C1 | a)
      s2 translated to (C1 | n)

Then, 
{{{
    T t1 ... tn a /\ C1 /\
    T t1 ....tn b /\ C2

--> FD rule step

    T t1 ... tn a /\ C1 /\
    a=b /\ [a/b] C2
}}}

Again, the operational effect of the type function generated
is also present in the CHR derivation


Lifting the restriction that t refers to types NOT containing
type functions (we only lift this restriction for
local assumptions).

Consider
{{{
forall a. T [a] = [T a]      -- axiom

T [S Int] = s                -- local assumption
}}}

We can normalize
{{{
T [S Int] = s
}}}
to
{{{
T [b] = s
S Int = b
}}}
Method from above applies then.

NOTE: Regarding generation of implication constraints.
GENERATEIMP

The literate implication constraints generated out of the
program text may look as follows
{{{ 
a=T Int implies ( a= S Int implies ...)
}}}

The above can be simplified to
{{{ 
(a=T Int /\ a = S Int) implies ...
}}}
Before we proceed with the completion method, we first
need to apply some closure rules (eg. transitivity, left, right etc)
Hence, from the above we generatet
{{{
   a=T Int /\ a = S Int /\ 
   T Int = a /\ S Int = a /\       -- symmetry
   T Int = S Int /\ S Int = T Int  -- transitivity
}}}
We omit the trival (reflexive) equations
{{{ 
T Int = T Int /\ S Int = S Int 
}}}