A note on rewriting theory for uniqueness of iteration

Mitsuhiro Okada, P. J. Scott

Research output: Contribution to journalArticle

7 Citations (Scopus)

Abstract

Uniqueness for higher type term constructors in lambda calculi (e.g. surjective pairing for product types, or uniqueness of iterators on the natural numbers) is easily expressed using universally quantified conditional equations. We use a technique of Lambek [18] involving Mal'cev operators to equationally express uniqueness of iteration (more generally, higher-order primitive recursion) in a simply typed lambda calculus, essentially Godel's T [29,13]. We prove the following facts about typed lambda calculus with uniqueness for primitive recursors: (i) It is undecidable, (ii) Church-Rosser fails, although ground Church-Rosser holds, (iii) strong normalization (termination) is still valid. This entails the undecidability of the coherence problem for cartesian closed categories with strong natural numbers objects, as well as providing a natural example of the following computational paradigm: a non-CR, ground CR, undecidable, terminating rewriting system.

Original languageEnglish
Pages (from-to)47-64
Number of pages18
JournalTheory and Applications of Categories
Volume6
Publication statusPublished - 2000
Externally publishedYes

Fingerprint

Rewriting
Uniqueness
Iteration
Typed lambda Calculus
Natural number
Cartesian Closed Category
Strong Normalization
Rewriting Systems
Undecidability
Lambda Calculus
Recursion
Pairing
Termination
Express
Paradigm
Valid
Higher Order
Term
Operator

Keywords

  • Mal'cev operations
  • Rewriting theory
  • Strong normalization
  • Typed lambda calculus

ASJC Scopus subject areas

  • Mathematics(all)

Cite this

A note on rewriting theory for uniqueness of iteration. / Okada, Mitsuhiro; Scott, P. J.

In: Theory and Applications of Categories, Vol. 6, 2000, p. 47-64.

Research output: Contribution to journalArticle

@article{be21954ed3e24c379876da7217e40a7e,
title = "A note on rewriting theory for uniqueness of iteration",
abstract = "Uniqueness for higher type term constructors in lambda calculi (e.g. surjective pairing for product types, or uniqueness of iterators on the natural numbers) is easily expressed using universally quantified conditional equations. We use a technique of Lambek [18] involving Mal'cev operators to equationally express uniqueness of iteration (more generally, higher-order primitive recursion) in a simply typed lambda calculus, essentially Godel's T [29,13]. We prove the following facts about typed lambda calculus with uniqueness for primitive recursors: (i) It is undecidable, (ii) Church-Rosser fails, although ground Church-Rosser holds, (iii) strong normalization (termination) is still valid. This entails the undecidability of the coherence problem for cartesian closed categories with strong natural numbers objects, as well as providing a natural example of the following computational paradigm: a non-CR, ground CR, undecidable, terminating rewriting system.",
keywords = "Mal'cev operations, Rewriting theory, Strong normalization, Typed lambda calculus",
author = "Mitsuhiro Okada and Scott, {P. J.}",
year = "2000",
language = "English",
volume = "6",
pages = "47--64",
journal = "Theory and Applications of Categories",
issn = "1201-561X",
publisher = "Mount Allison University",

}

TY - JOUR

T1 - A note on rewriting theory for uniqueness of iteration

AU - Okada, Mitsuhiro

AU - Scott, P. J.

PY - 2000

Y1 - 2000

N2 - Uniqueness for higher type term constructors in lambda calculi (e.g. surjective pairing for product types, or uniqueness of iterators on the natural numbers) is easily expressed using universally quantified conditional equations. We use a technique of Lambek [18] involving Mal'cev operators to equationally express uniqueness of iteration (more generally, higher-order primitive recursion) in a simply typed lambda calculus, essentially Godel's T [29,13]. We prove the following facts about typed lambda calculus with uniqueness for primitive recursors: (i) It is undecidable, (ii) Church-Rosser fails, although ground Church-Rosser holds, (iii) strong normalization (termination) is still valid. This entails the undecidability of the coherence problem for cartesian closed categories with strong natural numbers objects, as well as providing a natural example of the following computational paradigm: a non-CR, ground CR, undecidable, terminating rewriting system.

AB - Uniqueness for higher type term constructors in lambda calculi (e.g. surjective pairing for product types, or uniqueness of iterators on the natural numbers) is easily expressed using universally quantified conditional equations. We use a technique of Lambek [18] involving Mal'cev operators to equationally express uniqueness of iteration (more generally, higher-order primitive recursion) in a simply typed lambda calculus, essentially Godel's T [29,13]. We prove the following facts about typed lambda calculus with uniqueness for primitive recursors: (i) It is undecidable, (ii) Church-Rosser fails, although ground Church-Rosser holds, (iii) strong normalization (termination) is still valid. This entails the undecidability of the coherence problem for cartesian closed categories with strong natural numbers objects, as well as providing a natural example of the following computational paradigm: a non-CR, ground CR, undecidable, terminating rewriting system.

KW - Mal'cev operations

KW - Rewriting theory

KW - Strong normalization

KW - Typed lambda calculus

UR - http://www.scopus.com/inward/record.url?scp=0006983647&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=0006983647&partnerID=8YFLogxK

M3 - Article

AN - SCOPUS:0006983647

VL - 6

SP - 47

EP - 64

JO - Theory and Applications of Categories

JF - Theory and Applications of Categories

SN - 1201-561X

ER -