Xref: utzoo sci.math:12394 comp.theory:1049
Path: utzoo!utgpu!news-server.csri.toronto.edu!cs.utexas.edu!wuarchive!mit-eddie!bloom-beacon!eru!hagbard!sunic!liuida!jonwa
From: jonwa@ida.liu.se (Jonas Wallgren)
Newsgroups: sci.math,comp.theory
Subject: What is unification?
Message-ID: <1990Sep18.165715.16120@ida.liu.se>
Date: 18 Sep 90 16:57:15 GMT
Organization: CIS Dept, Univ of Linkoping, Sweden
Lines: 32

What is unification?

How would you describe or explain unification in a simple way, with as few
technicalities as possible?

Is "equation solving" a good candidate?

Well, what do you mean by equation solving?
Does it have to result in a number of variable bindings (a unifier)?
Or could I say that a=b is solved if I can construct a c that is the result of
trying to get a and b equal?

My specific problem has to do with types:

        If I have a=int and b=X (a type variable) I can solve a=b by letting
        X=int and substitute that on both sides to get int=int.

        But if I also allow sum types (e.g. overloading) I could have
        a=int and b=bool and then solve a=b by saying that the resulting
        type c should be int+bool.

Would you call this equation solving? Would you call it unification?

If not, what would you call it?

-------------------------------------------------------------------------------
Jonas Wallgren                                 |                 jwc@ida.liu.se
Department of Computer and Information Science |
Linkoping University                           |-------------------------------
SE-581 83  Linkoping                           |
Sweden                                         |(\x.xx)(\x.x):(forall a.(a->a))
-------------------------------------------------------------------------------