In the paper we constructively define the sub-class P of primitive recursive functions which can be defined from the base functions 0, s, x+y and x-y,and closed under composition. We show that the equivalence problem for P is solvable by reducing the function definitions according to a Church-Rosser Noetherian term rewriting system and testing the resulting irreducible terms for identity. Finally, we define an effective mapping from primitive recursive definitions to the definitions of the class P.

On solving the equivalence problem for a sub-class of primitive recursive functions

SIROVICH, Franco
1979-01-01

Abstract

In the paper we constructively define the sub-class P of primitive recursive functions which can be defined from the base functions 0, s, x+y and x-y,and closed under composition. We show that the equivalence problem for P is solvable by reducing the function definitions according to a Church-Rosser Noetherian term rewriting system and testing the resulting irreducible terms for identity. Finally, we define an effective mapping from primitive recursive definitions to the definitions of the class P.
1979
http://www.di.unito.it/~franco/PUBS/TR/N11.pdf
equivalence of functions; primitive recursive functions; loop programs; term rewriting systems; Church-Rosser and Noetherian properties
P. Degano; Franco Sirovich
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/2318/45241
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus ND
  • ???jsp.display-item.citation.isi??? ND
social impact