Proof of termination of the rewriting system SUBSET on CCL
\textit{P. L. Curien} [Categorical combinators, sequential algorithms and functional programming (Pitman, London, 1985)] defines a translation of the \(\lambda\) c-calculus in the Pure Combinatory Categorical Logic and establishes an equivalence theorem between these two theories. The rewriting system SUBSET simulates in particular the substitution of the \(\lambda\) c-calculus. This system is locally confluent. We shall show here that it is also noetherian.
scientific article; zbMATH DE number 4003516
scientific article