Nominal Unification from a Higher-Order Perspective

Details Nominal Unification from a Higher-Order Perspective Nominal Unification from a Higher-Order Perspective

2010-05-20

arxiv.org/abs/1005.3731v1

Computer Science

Logic in Computer Science

Scientific paper

Nominal Logic is a version of first-order logic with equality, name-binding, renaming via name-swapping and freshness of names. Contrarily to higher-order logic, bindable names, called atoms, and instantiable variables are considered as distinct entities. Moreover, atoms are capturable by instantiations, breaking a fundamental principle of lambda-calculus. Despite these differences, nominal unification can be seen from a higher-order perspective. From this view, we show that nominal unification can be reduced to a particular fragment of higher-order unification problems: Higher-Order Pattern Unification. This reduction proves that nominal unification can be decided in quadratic deterministic time, using the linear algorithm for Higher-Order Pattern Unification. We also prove that the translation preserves most generality of unifiers.

Affiliated with

Also associated with

No associations

Rating

Nominal Unification from a Higher-Order Perspective does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.

If you have personal experience with Nominal Unification from a Higher-Order Perspective, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Nominal Unification from a Higher-Order Perspective will most certainly appreciate the feedback.

Rate now

Comments { 0 }

Profile ID: LFWR-SCP-O-211276