Carregant...
Carregant...

Vés al contingut (premeu Retorn)

The recursive path and polynomial ordering for first-order and higher-order terms

Autor
Bofill, M.; Borralleras, C.; Rodriguez, E.; Rubio, A.
Tipus d'activitat
Article en revista
Revista
Journal of logic and computation
Data de publicació
2013-01-23
Volum
23
Número
1
Pàgina inicial
263
Pàgina final
305
DOI
https://doi.org/10.1093/logcom/exs027 Obrir en finestra nova
URL
http://logcom.oxfordjournals.org/content/23/1/263 Obrir en finestra nova
Resum
In most termination tools two ingredients, namely recursive path orderings (RPOs) and polynomial interpretation orderings (POLOs), are used in a consecutive disjoint way to solve the final constraints generated from the termination problem. In this article we present a simple ordering that combines both RPO and POLO and defines a family of orderings that includes both, and extend them with the possibility of having, at the same time, an RPO-like treatment for some symbols and a POLO-like treatme...
Paraules clau
Program correctness, Term orderings, Term rewriting, Termination, Typed lambda-calculus
Grup de recerca
LOGPROG - Lògica i Programació

Participants