Portal de Periódicos da CAPES

Currying Second-Order Unification Problems

2002; Springer Science+Business Media; Linguagem: Inglês

10.1007/3-540-45610-4_23

1611-3349

Jordi Levy, Mateu Villaret,

Mathematics, Computing, and Information Processing

The Curry form of a term, like f(a, b), allows us to write it, using just a single binary function symbol, as @(@(f,a),b). Using this technique we prove that the signature is not relevant in second-order unification, and conclude that one binary symbol is enough. By currying variable applications, like X(a), as @(X,a), we can transform second-order terms into first-order terms, but we have to add beta-reduction as a theory. This is roughly what it is done in explicit unification. We prove that by currying only constant applications we can reduce second-order unification to second-order unification with just one binary function symbol. Both problems are already known to be undecidable, but applying the same idea to context unification, for which decidability is still unknown, we reduce the problem to context unification with just one binary function symbol. We also discuss about the difficulties of applying the same ideas to third or higher order unification.