error

gistfile1.cs

using System;
using System.Collections.Generic;
using System.Linq;
using System.Text;
using System.Threading.Tasks;

namespace TRS
{
    using RuleSet = SortedSet<TermPair>;
    using Subst = List<SubstItem>;

    class TermPairComparator : IComparer<TermPair>
    {
        public int Compare(TermPair x, TermPair y)
        {
            return x.CompareTo(y);
        }
    }

    class VName
    {
        public VName()
        { }

        public VName(string name)
        {
            this.name = name;
            this.value = 0;
        }

        public VName(string name, int value)
        {
            this.name = name;
            this.value = value;
        }

        public override string ToString()
        {
            return name + value.ToString();
        }

        public static int Compare(VName x, VName y)
        {
            int n = string.Compare(x.name, y.name);
            if (n != 0)
            {
                return n;
            }
            else
            {
                return x.value < y.value ? -1 : x.value > y.value ? +1 : 0;
            }
        }

        public static bool operator< (VName x, VName y)
        {
            return Compare(x, y) == -1;
        }

        public static bool operator> (VName x, VName y)
        {
            return y < x;
        }

        public static bool operator== (VName x, VName y)
        {
            return Compare(x, y) == 0;
        }

        public static bool operator!= (VName x, VName y)
        {
            return Compare(x, y) != 0;
        }

        public string name = "";
        public int value  = 0;
    }

    class Term
    {
        public virtual Term Clone()
        {
            return null;
        }
        
        public static int Compare(Term s, Term t)
        {
            if (s.GetType() == typeof(VTerm) && t.GetType() == typeof(TTerm))
            {
                return -1;
            }
            if (s.GetType() == typeof(TTerm) && t.GetType() == typeof(VTerm))
            {
                return +1;
            }
            if (s.GetType() == t.GetType())
            {
                if (s.GetType() == typeof(VTerm))
                {
                    return VName.Compare(((VTerm)s).vname, ((VTerm)t).vname);
                }
                else if (s.GetType() == typeof(TTerm))
                {
                    TTerm sPrime = (TTerm)s, tPrime = (TTerm)t;
                    int n = string.Compare(sPrime.name, tPrime.name);
                    if (n != 0)
                    {
                        return n;
                    }
                    else
                    {
                        int i = 0;
                        for (; i < sPrime.termList.Count() && i < tPrime.termList.Count(); ++i)
                        {
                            int m = Compare(sPrime.termList[i], tPrime.termList[i]);
                            if (m != 0)
                            {
                                return m;
                            }
                        }
                        if (i == sPrime.termList.Count() && i < tPrime.termList.Count())
                        {
                            return -1;
                        }
                        else if (i < sPrime.termList.Count() && i == tPrime.termList.Count())
                        {
                            return +1;
                        }
                        return 0;
                    }
                }
            }
            throw (new ArgumentException());
        }

        public static bool operator< (Term s, Term t)
        {
            return Compare(s, t) == -1;
        }

        public static bool operator> (Term s, Term t)
        {
            return Compare(s, t) == +1;
        }

        public static bool operator== (Term s, Term t)
        {
            return Compare(s, t) == 0;
        }

        public static bool operator!= (Term s, Term t)
        {
            return Compare(s, t) != 0;
        }

    }

    class VTerm : Term
    {
        public VTerm()
        { }

        public VTerm(string name, int value)
        {
            vname.name = name;
            vname.value = value;
        }

        public override Term Clone()
        {
            VTerm other = new VTerm();
            other.vname = vname;
            return other;
        }

        public override string ToString()
        {
            return vname.ToString();
        }

        public VName vname = new VName();
    }

    class TTerm : Term
    {
        public TTerm(string name)
        {
            this.name = name;
            termList = new List<Term>();
        }

        public TTerm(string name, List<Term> termList)
        {
            this.name = name;
            this.termList = new List<Term>(termList);
        }

        public override Term Clone()
        {
            return new TTerm(name, termList);
        }

        public override string ToString()
        {
            string str;
            str = name;
            if (termList.Count() > 0)
            {
                str += "(";
                for (int i = 0; i < termList.Count(); ++i)
                {
                    str += termList[i].ToString();
                    if (i < termList.Count() - 1)
                    {
                        str += ", ";
                    }
                }
                str += ")";
            }
            return str;
        }

        public string name;
        public List<Term> termList;
    }

    class SubstItem
    {
        public SubstItem(VName vname)
        {
            this.vname = vname;
            term = null;
        }

        public SubstItem(VName vname, Term term)
        {
            this.vname = vname;
            this.term = term;
        }

        public VName vname;
        public Term term;
    }

    class UnifyException : Exception
    { }

    class NormException : Exception
    { }

    class CompletionFailedException : Exception
    { }

    class TermPair : IComparable
    {
        public int CompareTo(object other)
        {
            int n = Term.Compare(t1, ((TermPair)other).t1);
            n = n == 0 ? Term.Compare(t2, ((TermPair)other).t2) : n;
            return n;
        }

        public TermPair(Term t1, Term t2)
        {
            this.t1 = t1.Clone();
            this.t2 = t2.Clone();
        }

        public Term t1, t2;
    }
    
    class TRS
    {
        public static bool Indom(VName x, Subst s)
        {
            return Utility<SubstItem>.Exists(a => a.vname == x, s);
        }

        public static Term App(Subst subst, VName x)
        {
            for (int i = 0; i < subst.Count(); ++i)
            {
                if (subst[i].vname == x)
                {
                    return subst[i].term.Clone() as Term;
                }
            }
            return null;
        }

        public static Term Lift(Subst s, Term t)
        {
            if (t.GetType() == typeof(VTerm))
            {
                VName x = ((VTerm)t).vname;
                if (Indom(x, s))
                {
                    return App(s, x);
                }
                else
                {
                    return t.Clone() as Term;
                }
            }
            else if (t.GetType() == typeof(TTerm))
            {
                return new TTerm(((TTerm)t).name, Utility<Term>.Mapping(a => Lift(s, a), ((TTerm)t).termList));
            }
            return null;
        }

        public static bool Occurs(VName x, Term t)
        {
            if (t.GetType() == typeof(VTerm))
            {
                return x == ((VTerm)t).vname;
            }
            else if (t.GetType() == typeof(TTerm))
            {
                return Utility<Term>.Exists(a => Occurs(x, a), ((TTerm)t).termList);
            }
            else
            {
                throw (new ArgumentException());
            }
        }

        public static Subst Solve(List<TermPair> ttList, Subst s)
        {
            if (ttList.Count() == 0)
            {
                return new Subst(s);
            }
            TermPair tt = ttList[0];
            ttList.RemoveAt(0);
            if (tt.t1.GetType() == typeof(VTerm))
            {
                if (tt.t1 == tt.t2)
                {
                    return Solve(ttList, s);
                }
                else
                {
                    return Elim(((VTerm)tt.t1).vname, tt.t2, ttList, s);
                }
            }
            else if (tt.t2.GetType() == typeof(VTerm))
            {
                return Elim(((VTerm)tt.t2).vname, tt.t1, ttList, s);
            }
            else if (tt.t1.GetType() == typeof(TTerm) && tt.t2.GetType() == typeof(TTerm))
            {
                string f = ((TTerm)tt.t1).name, g = ((TTerm)tt.t2).name;
                List<Term> ts = ((TTerm)tt.t1).termList, us = ((TTerm)tt.t2).termList;
                if (f == g)
                {
                    List<TermPair> tmp = TermUtility.Zip(ts, us);
                    tmp.AddRange(ttList);
                    return Solve(tmp, s);
                }
                else
                {
                    throw (new UnifyException());
                }
            }
            else
            {
                throw (new ArgumentException());
            }
        }

        public static Subst Elim(VName x, Term t, List<TermPair> ttList, Subst s)
        {
            if (Occurs(x, t))
            {
                throw (new UnifyException());
            }
            Subst l2 = new Subst(){ new SubstItem(x, t) };
            l2.AddRange(Utility<SubstItem>.Mapping(a => new SubstItem(a.vname, Lift(new Subst(){ new SubstItem(x, t) }, a.term)), s));
            return Solve(Utility<TermPair>.Mapping(a => new TermPair(Lift(new Subst() { new SubstItem(x, t) }, a.t1), Lift(new Subst() { new SubstItem(x, t) }, a.t2)), ttList), l2);
        }

        public static Subst Unify(Term t1, Term t2)
        {
            return Solve(new List<TermPair>(){ new TermPair(t1, t2) }, new Subst());
        }

        public static Subst Matchs(List<TermPair> ttList, Subst s)
        {
            if (ttList.Count() == 0)
            {
                return s;
            }
            TermPair tt = ttList[0];
            ttList.RemoveAt(0);
            if (tt.t1.GetType() == typeof(VTerm))
            {
                VTerm x = (VTerm)tt.t1;
                if (Indom(x.vname, s))
                {
                    if (App(s, x.vname) == tt.t2)
                    {
                        return Matchs(ttList, s);
                    }
                    else
                    {
                        throw (new UnifyException());
                    }
                }
                else
                {
                    Subst r = new Subst() { new SubstItem(x.vname, tt.t2) };
                    r.AddRange(s);
                    return Matchs(ttList, r);
                }
            }
            else if (tt.t2.GetType() == typeof(VTerm))
            {
                throw (new UnifyException());
            }
            else if (tt.t1.GetType() == typeof(TTerm) && tt.t2.GetType() == typeof(TTerm))
            {
                string f = ((TTerm)tt.t1).name, g = ((TTerm)tt.t2).name;
                List<Term> ts = ((TTerm)tt.t1).termList, us = ((TTerm)tt.t2).termList;
                if (f == g)
                {
                    List<TermPair> list = TermUtility.Zip(ts, us);
                    list.AddRange(ttList);
                    return Matchs(list, s);
                }
                else
                {
                    throw (new UnifyException());
                }
            }
            else
            {
                throw (new ArgumentException());
            }
        }

        public static Subst Match(Term pat, Term obj)
        {
            return Matchs(new List<TermPair>() { new TermPair(pat, obj) }, new Subst());
        }

        public static Term Rewrite(List<TermPair> ttList, Term t)
        {
            if (ttList.Count() == 0)
            {
                throw (new NormException());
            }
            TermPair tt = ttList[0];
            ttList.RemoveAt(0);
            try
            {
                return Lift(Match(tt.t1, t), tt.t2);
            }
            catch (UnifyException)
            {
                return Rewrite(ttList, t);
            }
        }

        public static Term Norm(List<TermPair> ttList, Term t)
        {
            if (t.GetType() == typeof(VTerm))
            {
                return t;
            }
            else if (t.GetType() == typeof(TTerm))
            {
                List<Term> ts = ((TTerm)t).termList;
                Term u = new TTerm(((TTerm)t).name, Utility<Term>.Mapping(a => Norm(ttList, a), ts));
                try
                {
                    return Norm(ttList, Rewrite(ttList, u));
                }
                catch(NormException)
                {
                    return u;
                }
            }
            else
            {
                throw (new ArgumentException());
            }
        }

        public static Term Rename(int n, Term term)
        {
            if (term.GetType() == typeof(VTerm))
            {
                VTerm v = (VTerm)(term.Clone());
                v.vname.value += n;
                return v;
            }
            else if (term.GetType() == typeof(TTerm))
            {
                TTerm t = (TTerm)(term.Clone());
                return new TTerm(t.name, Utility<Term>.Mapping(a => Rename(n, a), t.termList));
            }
            else
            {
                throw (new ArgumentException());
            }
        }

        public static int Maxs(List<int> list)
        {
            int m = 0;
            foreach (int value in list)
            {
                m = Math.Max(m, value);
            }
            return m;
        }

        public static int MaxIndex(Term term)
        {
            if (term.GetType() == typeof(VTerm))
            {
                return ((VTerm)term).vname.value;
            }
            else if (term.GetType() == typeof(TTerm))
            {
                return Maxs(Utility<Term>.IntMapping(a => MaxIndex(a), ((TTerm)term).termList));
            }
            else
            {
                throw (new ArgumentException());
            }
        }

        public delegate Term CF(Term t);

        public static List<TermPair> CP(CF C, TermPair tr, TermPair l2r2)
        {
            try
            {
                Subst s = Unify(tr.t1, l2r2.t1);
                return new List<TermPair>() { new TermPair(Lift(s, tr.t2), Lift(s, tr.t2)) };
            }
            catch (UnifyException)
            {
                return new List<TermPair>();
            }
        }

        public delegate List<TermPair> CPsDelegate(CF C, TermPair tt);

        public class InnerCPsItem
        {
            public InnerCPsItem(string f, List<Term> ts0, List<Term> ts1, Term r)
            {
                this.f = f;
                this.ts0 = ts0;
                this.ts1 = ts1;
                this.r = r;
            }

            public string f;
            public List<Term> ts0, ts1;
            public Term r;
        }

        public delegate List<TermPair> InnerCPsDelegate(CF C, InnerCPsItem innerCPsItem);

        public class CPs
        {
            public CPs(List<TermPair> argR) {
                R = new List<TermPair>(argR);

                cps = (CF C, TermPair tt) =>
                {
                    if (tt.t1.GetType() == typeof(VTerm))
                    {
                        return new List<TermPair>();
                    }
                    else if (tt.t1.GetType() == typeof(TTerm))
                    {
                        TTerm t = (TTerm)tt.t1;
                        List<TermPair> list = Utility<TermPair>.ConvolutionMapping(a => CP(C, tt, a), R);
                        list.AddRange(innercps(C, new InnerCPsItem(t.name, new List<Term>(), t.termList, tt.t2)));
                        return list;
                    }
                    else
                    {
                        throw (new ArgumentException());
                    }
                };
                
                innercps = (CF C, InnerCPsItem innerCPsItem) =>
                {
                    if (innerCPsItem.ts1.Count() == 0)
                    {
                        return new List<TermPair>();
                    }
                    List<Term> ts1Prime = new List<Term>(innerCPsItem.ts1);
                    Term t = innerCPsItem.ts1[0];
                    ts1Prime.RemoveAt(0);

                    CF Cf = (Term s) =>
                    {
                        List<Term> list = new List<Term>();
                        list.AddRange(innerCPsItem.ts0);
                        list.Add(s);
                        list.AddRange(ts1Prime);
                        return C(new TTerm(innerCPsItem.f, list));
                    };

                    List<TermPair> pairList = cps(a => Cf(a), new TermPair(t, innerCPsItem.r));
                    List<Term> ts0Prime = new List<Term>(innerCPsItem.ts0);
                    ts0Prime.Add(t);
                    pairList.AddRange(innercps(C, new InnerCPsItem(innerCPsItem.f, ts0Prime, ts1Prime, innerCPsItem.r)));
                    return pairList;
                };

                m = Maxs(Utility<TermPair>.IntMapping(a => Math.Max(MaxIndex(a.t1), MaxIndex(a.t2)), R)) + 1;
            }

            public List<TermPair> Compute(Term l, Term r)
            {
                return cps(a => a, new TermPair(Rename(m, l), Rename(m, r)));
            }

            public List<TermPair> R;
            public InnerCPsDelegate innercps;
            public CPsDelegate cps;
            public int m;
        }

        public static List<TermPair> CriticalPairs(List<TermPair> R)
        {
            CPs cps = new CPs(R);
            return Utility<TermPair>.ConvolutionMapping(a => cps.Compute(a.t1, a.t2), R);
        }

        public static List<TermPair> ConvertRule(RuleSet rule)
        {
            List<TermPair> list = new List<TermPair>();
            foreach (TermPair tt in rule)
            {
                list.Add(tt);
            }
            return list;
        }

        public static RuleSet ConvertInternalRule(List<TermPair> internalRule)
        {
            RuleSet set = new RuleSet();
            foreach (TermPair tt in internalRule)
            {
                set.Add(tt);
            }
            return set;
        }

        public static void PutTermPair(TermPair tt)
        {
            Console.Write(" = ");
            Console.Write("\n");
        }

        public static RuleSet Completion(RuleSet argRuleSet)
        {
            RuleSet ruleSet = new RuleSet(argRuleSet);
            List<TermPair> internalRule, internalCPs;
            while(true)
            {
                Console.WriteLine("--------");
                internalRule = ConvertRule(ruleSet);
                internalCPs = CriticalPairs(internalRule);
                RuleSet rulePrime = new RuleSet(ruleSet), NCPs = ConvertInternalRule(internalCPs);
                foreach (TermPair tt in NCPs)
                {
                    TermPair st = new TermPair(Norm(new List<TermPair>(internalRule), tt.t1), Norm(new List<TermPair>(internalRule), tt.t2));
                    Console.WriteLine("<" + st.t1.ToString() + " vs " + st.t2.ToString() + ">");
                    if (st.t1 > st.t2)
                    {
                        rulePrime.Add(new TermPair(st.t1, st.t2));
                        Console.WriteLine(st.t1.ToString() + " = " + st.t2.ToString());
                    }
                    else if (st.t2 > st.t1)
                    {
                        rulePrime.Add(new TermPair(st.t2, st.t1));
                        Console.WriteLine(st.t2.ToString() + " = " + st.t1.ToString());
                    }
                    else
                    {
                        Console.WriteLine("[" + st.t2.ToString() + " = " + st.t1.ToString() + "]");
                    }
                }
                if (ruleSet.Count() == rulePrime.Count())
                {
                    break;
                }
                else
                {
                    ruleSet = rulePrime;
                }
            }
            return ruleSet;
        }

        public class Utility<Type>
        {
            public delegate Type F(Type x);
            public delegate List<Type> C(Type x);
            public delegate bool P(Type x);
            public delegate int I(Type x);

            public static List<Type> Mapping(F f, List<Type> list)
            {
                List<Type> newList = new List<Type>(list);
                for (int i = 0; i < newList.Count(); ++i)
                {
                    newList[i] = f(newList[i]);
                }
                return newList;
            }

            public static List<Type> ConvolutionMapping(C c, List<Type> list)
            {
                List<Type> newList = new List<Type>(list);
                for (int i = 0; i < list.Count(); ++i)
                {
                    newList.AddRange(c(newList[i]));
                }
                return newList;
            }
            
            public static List<int> IntMapping(I f, List<Type> list)
            {
                List<int> newList = new List<int>();
                for (int i = 0; i < newList.Count(); ++i)
                {
                    newList.Add(f(list[i]));
                }
                return newList;
            }

            public static bool Exists(P p, List<Type> list)
            {
                for (int i = 0; i < list.Count(); ++i)
                {
                    if (p(list[i]))
                    {
                        return true;
                    }
                }
                return false;
            }
        }

        public class TermUtility
        {
            public static List<TermPair> Zip(List<Term> a, List<Term> b)
            {
                List<TermPair> newList = new List<TermPair>();
                for (int i = 0; i < a.Count() && i < b.Count(); ++i)
                {
                    newList.Add(new TermPair(a[i], b[i]));
                }
                return newList;
            }
        }
    }

    class Program
    {
        static void Main(string[] args)
        {
            RuleSet rule = new RuleSet()
            {
                // f(x, 0) = x.
                new TermPair(new TTerm("f", new List<Term>() { new VTerm("x", 0), new TTerm("0") }), new VTerm("x", 0)),

                // f(i(x), x) = 0.
                new TermPair(new TTerm("f", new List<Term>() { new TTerm("i", new List<Term>() { new VTerm("x", 0) }) }), new TTerm("0")),

                // f(f(x, y), z) = f(x, f(y, z)).
                new TermPair(
                    new TTerm("f", new List<Term>() { new TTerm("f", new List<Term>() { new VTerm("x", 0), new VTerm("x", 1) }), new VTerm("x", 2) }),
                    new TTerm("f", new List<Term>() { new VTerm("x", 0), new TTerm("f", new List<Term>() { new VTerm("x", 1), new VTerm("x", 2) }) })
                )
            };

            // Knuth-Bendix Completion Algorithm.
            RuleSet compl = TRS.Completion(rule);
        }
    }
}