[PL-sem-jr] Another topic: unification

[Dave Herman]

Dale, is something you could help out with? You're probably the most 
familiar with the unification literature of all of us, since you did a 
HoPL talk on it.

Dave

Felix S Klock II wrote:
> PLjr-ites-
> 
> Seeing Dave's recent email calling for a presentation on GADTs reminded 
> me of something.
> 
> I've recently been reading papers on (the undecidablity of) 
> Semi-Unification and 2nd-Order Unification.
> 
> Going through the process of trying to solve an instance of 2nd-Order 
> Unification made me realize what an interesting problem it was.
> 
> For example, let Type be the set of simple types generated by arrow and 
> some collection of base type constants containing at least { A, B, C, D 
> }.  Can you find some function F, taken from the domain Type to Type to 
> Type, such that:
> F( A -> B )( C -> D -> B )   =   F( B )( C ) -> D -> A -> A -> B
> 
> [[ This was adopted from Aleksy Shubert: 
> http://www.mimuw.edu.pl/~alx/papers.php ]]
> 
> Also, there is much work in the area of defining useful decidable 
> subclasses of 2nd-Order Unification.
> 
> So I would like to see someone give a talk on the research in 
> Unification in general.  I'd be willing to help with the presentation, 
> but I don't want to do it alone.
> 
> -Felix
> 
> ----
> "At a funeral, the real programmer is the one saying
>  'poor George. And he almost had the sort routine working
>  before the coronary.'"  -Real Programmers don't use Pascal
> 
> 
> _______________________________________________
> Pl-sem-jr mailing list
> Pl-sem-jr at lists.ccs.neu.edu
> https://lists.ccs.neu.edu/bin/listinfo/pl-sem-jr