Title | Currying Second-Order Unification Problems |

Publication Type | Conference Paper |

Year of Publication | 2002 |

Authors | Levy J [1], Villaret M [2] |

Conference Name | Lecture Notes in Computer Science |

Volume | 2378 |

Publisher | Springer-Verlag |

Pagination | 326-339 |

Abstract | 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). Here we answer the question: Do Curry forms help to solve second-order unification problems? 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 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 think that currying could also help to simplify the signature in the case of higher-order matching, for which decidability is also unknown. |