Proof of termination of the rewriting system SUBSET on CCL (Q1822494)
From MaRDI portal
 | This is the item page for this Wikibase entity, intended for internal use and editing purposes. Please use this page instead for the normal view: Proof of termination of the rewriting system SUBSET on CCL |
scientific article; zbMATH DE number 4003516
| Language | Label | Description | Also known as |
|---|---|---|---|
| English | Proof of termination of the rewriting system SUBSET on CCL |
scientific article; zbMATH DE number 4003516 |
Statements
Proof of termination of the rewriting system SUBSET on CCL (English)
0 references
1986
0 references
\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.
0 references
\(\lambda \) c-calculus
0 references
Pure Combinatory Categorical Logic
0 references
rewriting system
0 references
