Proof of termination of the rewriting system SUBSET on CCL
type: Item
instance of: scholarly article
title: Proof of termination of the rewriting system SUBSET on CCL
zbMATH Open document ID: 0618.68031
DOI: 10.1016/0304-3975(86)90035-6
author: Thérèse Hardin
author: Alain Laville
published in: Theoretical Computer Science
publication date: 1986-01-01T00:00:00Z
review text: \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.
Mathematics Subject Classification ID: 68Q65
Mathematics Subject Classification ID: 03B40
Mathematics Subject Classification ID: 68N01
zbMATH DE Number: 4003516
zbMATH Keywords: \(\lambda \) c-calculus
zbMATH Keywords: Pure Combinatory Categorical Logic
zbMATH Keywords: rewriting system
describes a project that uses: REVE
MaRDI profile type: Publication
full work available at URL: 0304-3975(86)90035-6
OpenAlex ID: W1970547272
cites work: Termination by completion
cites work: Q3783523
cites work: Q3785893
cites work: Orderings for term-rewriting systems
cites work: Q3703288
cites work: Proving termination with multiset orderings
cites work: Q3667939
description: scientific article; zbMATH DE number 4003516