(HO)RPO Revisited

Details (HO)RPO Revisited (HO)RPO Revisited

2006-09-08

arxiv.org/abs/cs/0609037v1

Computer Science

Logic in Computer Science

Scientific paper

The notion of computability closure has been introduced for proving the termination of the combination of higher-order rewriting and beta-reduction. It is also used for strengthening the higher-order recursive path ordering. In the present paper, we study in more details the relations between the computability closure and the (higher-order) recursive path ordering. We show that the first-order recursive path ordering is equal to an ordering naturally defined from the computability closure. In the higher-order case, we get an ordering containing the higher-order recursive path ordering whose well-foundedness relies on the correctness of the computability closure. This provides a simple way to extend the higher-order recursive path ordering to richer type systems.

Affiliated with

Also associated with

No associations

Rating

(HO)RPO Revisited 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 (HO)RPO Revisited, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and (HO)RPO Revisited will most certainly appreciate the feedback.

Rate now

Comments { 0 }

Profile ID: LFWR-SCP-O-111990