Simplifying the signature in second-order unification | Zendy

Jordi Levy | Zendy; Mateu Villaret | Zendy

AI Assistant Blog Pricing

Home ZAIA Blog

Open Access

Simplifying the signature in second-order unification

Author(s) -

Jordi Levy,

Mateu Villaret

Publication year - 2009

Publication title -

applicable algebra in engineering communication and computing

Language(s) - English

Resource type - Journals

SCImago Journal Rank - 0.558

H-Index - 35

eISSN - 1432-0622

pISSN - 0938-1279

DOI - 10.1007/s00200-009-0106-4

Subject(s) - unification , decidability , undecidable problem , signature (topology) , binary function , mathematics , binary number , context (archaeology) , symbol (formal) , function (biology) , bounded function , computer science , algorithm , arithmetic , programming language , mathematical analysis , geometry , paleontology , evolutionary biology , biology

Second-Order Unification is undecidable even for very specialized fragments. The signature plays a crucial role in these fragments. If all symbols are monadic, then the problem is NP-complete, whereas it is enough to have just one binary constant to lose decidability. In this work we reduce Second-Order Unification to Second-Order Unification with a signature that contains just one binary function symbol and constants. The reduction is based on partially currying the equations by using the binary function symbol for explicit application @. Our work simplifies the study of Second-Order Unification and some of its variants, like Context Unification and Bounded Second-Order Unification.

The content you want is available to Zendy users.

Already have an account? Click here to sign in.

Having issues? You can contact us here

Accelerating Research