C# + Sprache Lambda-Expr

Program.cs

using Sprache;
using System;
using System.Collections.Generic;
using System.Linq;
using System.Text;

namespace lambda_calc
{
    abstract class Statement { }
    abstract class Expr : Statement
    {
        public abstract Expr Conversion(Identifier before, Expr after);
        public abstract Expr Reduction(Identifier before = null, Expr after = null);

        public abstract Expr Optimize();
        public abstract IEnumerable<char> Definitions();

        public IEnumerable<char> AnonymousVar()
        {
            return Enumerable.Range('a', 26).Select(x => (char)x).Except(Definitions());
        }

        public abstract Expr Substitute(Assign assign);
    }
    class Identifier : Expr
    {
        public string Item { get; private set; }
        public Identifier(string item)
        {
            Item = item;
        }
        public Identifier(char item)
        {
            Item = item.ToString();
        }
        public override string ToString()
        {
            return Item;
        }
        public override Expr Conversion(Identifier before, Expr after)
        {
            return new Identifier(Item.Replace(before.Item, after.ToString()));
        }
        public override Expr Reduction(Identifier before = null, Expr after = null)
        {
            return (before != null && after != null) ?
                LambdaParser.expr.Parse(
                    (Item.Replace(before.Item, after.ToString()).Split(' ').Aggregate((s, x) => string.Format("({0}) {1}", s, x)))
                ) :
                this;
        }
        public override Expr Optimize()
        {
            return this;
        }
        public IEnumerable<Identifier> Tokens
        {
            get
            {
                return Item.Select(x => new Identifier(x.ToString()));
            }
        }
        public override IEnumerable<char> Definitions()
        {
            return Item.Distinct();
        }
        public override Expr Substitute(Assign assign)
        {
            return assign.Name == Item ? assign.Expr : this;
        }

    }
    class Abstraction : Expr
    {
        public Identifier Left { get; private set; }
        public Expr Right { get; private set; }

        public Abstraction(Identifier l, Expr r)
        {
            Left = l;
            Right = r;
        }
        public override string ToString()
        {
            return string.Format(@"λ{0}.{1}", Left, Right);
        }
        public override Expr Conversion(Identifier before, Expr after)
        {
            return new Abstraction(Left.Conversion(before, after) as Identifier, Right.Conversion(before, after));
        }
        public override Expr Reduction(Identifier before = null, Expr after = null)
        {
            return (before != null && after != null) ?
                Conversion(before, after) :
                this;
        }
        public override Expr Optimize()
        {
            return Left.Tokens.Reverse().Aggregate(Right, (s, x) => new Abstraction(x, s));
        }
        public override IEnumerable<char> Definitions()
        {
            return Left.Definitions().Concat(Right.Definitions()).Distinct();
        }
        public override Expr Substitute(Assign assign)
        {
            return new Abstraction(Left, Right.Substitute(assign));
        }
    }
    class Application : Expr
    {
        public Expr Left { get; private set; }
        public Expr Right { get; private set; }
        public Application(Expr l, Expr r)
        {
            Left = l;
            Right = r;
        }
        public override string ToString()
        {
            return string.Format(@"({0}) {1}", Left, Right);
        }
        public override Expr Conversion(Identifier before, Expr after)
        {
            return new Application(Left.Conversion(before, after), Right.Conversion(before, after));
        }
        public override Expr Reduction(Identifier before = null, Expr after = null)
        {
            var id = Left as Abstraction;
            if (before == null && after == null && id != null && (Right is Abstraction || Right is Identifier))
            {
                var defined = id.Right.Definitions().Intersect(Right.Definitions()).Where(x => x != ' ');
                if (defined.Any())
                {
                    var nr = defined.Aggregate(Right, (s, x) => s.Conversion(new Identifier(x), new Identifier(s.AnonymousVar().Except(id.Right.Definitions()).First())));
                    var beta = id.Right.Reduction(id.Left, nr);

                    Console.WriteLine("\tαβ[{0} -> {1}] : {2}", id.Left, nr, beta);

                    return beta;
                }
                else
                {
                    var beta = id.Right.Reduction(id.Left, Right);
                    Console.WriteLine("\tβ[{0} -> {1}] : {2}", id.Left, Right, beta);
                    return beta;
                }
            }
            else
            {
                return new Application(Left.Reduction(before, after), Right.Reduction(before, after));
            }
        }
        public override Expr Optimize()
        {
            return new Application(Left.Optimize(), Right.Optimize());
        }
        public override IEnumerable<char> Definitions()
        {
            return Left.Definitions().Concat(Right.Definitions()).Distinct();
        }
        public override Expr Substitute(Assign assign)
        {
            return new Application(Left.Substitute(assign), Right.Substitute(assign));
        }
    }
    class Assign : Statement
    {
        public string Name { get; private set; }
        public Expr Expr { get; private set; }
        public Assign(string n, Expr e)
        {
            Name = n;
            Expr = e;
        }
        public override string ToString()
        {
            return string.Format("<{0} = {1}>", Name, Expr);
        }
    }
    class LambdaParser
    {
        public static readonly Parser<char> lambda = Parse.Char('\\')
                                                          .Or(Parse.Char('λ'));
        public static readonly Parser<char> dot = Parse.Char('.');
        public static readonly Parser<char> space = Parse.WhiteSpace;

        public static readonly Parser<Expr> expr = Parse.Ref(() => application.Or<Expr>(abstraction).Or<Expr>(identifier));

        public static readonly Parser<Identifier> identifier = Parse.LetterOrDigit.Or(space).AtLeastOnce().Text().Select(x => new Identifier(x));
        public static readonly Parser<Abstraction> abstraction =
            from l in lambda
            from id in Parse.Letter.Or(space).AtLeastOnce().Text().Select(x => new Identifier(x))
            from d in dot
            from e in expr.Token().Many().Select(z => z.Aggregate((s, x) => new Application(s, x)))
            select new Abstraction(id, e);

        public static readonly Parser<Application> application =
            from ob in Parse.Char('(')
            from l in expr
            from cb in Parse.Char(')')
            from s in space
            from r in expr
            select new Application(l, r);


        public static readonly Parser<Assign> assign =
            from name in Parse.Upper.Or(Parse.Digit).AtLeastOnce().Text()
            from eq in Parse.Char('=').Token()
            from e in expr.End()
            select new Assign(name, e);

        public static readonly Parser<Statement> statement = assign.Or<Statement>(expr);
    }
    class Program
    {
        static void Main(string[] args)
        {
            var dic = new SortedDictionary<string, Assign>();
            while (true)
            {
                //input
                Console.Write(">");
                var src = Console.ReadLine();
                var parse = LambdaParser.statement.Parse(src);
                Console.WriteLine(parse);

                Expr result = (parse is Assign) ? (parse as Assign).Expr : parse as Expr;

                //substitute
                foreach (var p in dic)
                {
                    result = result.Substitute(p.Value);
                    Console.WriteLine("\t{0} -> {1}", p.Value, result);
                }

                //reduction
                string beta = "";
                while (true)
                {
                    Console.WriteLine("-> {0}", result);
                    result = result.Reduction();

                    if (result.ToString() == beta) break;
                    else beta = result.ToString();
                }
                //store
                var assign = parse as Assign;
                if (assign != null)
                {
                    var na = new Assign(assign.Name, result);
                    dic.Add(na.Name, na);
                }
            }

        }
    }
}