Completeness of Park induction

Research output: Contribution to journalArticle

34 Citations (Scopus)

Abstract

The (in)equational properties of iteration, i.e., least (pre-)fixed point solutions over cpo's, are captured by the axioms of iteration theories. All known axiomatizations of iteration theories consist of the Conway identities and a complicated equation scheme, the commutative identity. The results of this paper show that the commutative identity is implied by the Conway identities and a weak form of the Park induction principle. Hence, we obtain a simple first order axiomatization of the (in)equational theory of iteration. It follows that a few simple identities and a weak form of the Scott induction principle, formulated to involve only inequations, are also complete. We also show that the Conway identities and the Park induction principle are not complete for the universal Horn theory of iteration.

Original languageEnglish
Pages (from-to)217-283
Number of pages67
JournalTheoretical Computer Science
Volume177
Issue number1
Publication statusPublished - Apr 30 1997

Fingerprint

Completeness
Proof by induction
Iteration
Axiomatization
Equational Theory
Axioms
Fixed point
First-order
Form

ASJC Scopus subject areas

  • Computational Theory and Mathematics

Cite this

Completeness of Park induction. / Ésik, Z.

In: Theoretical Computer Science, Vol. 177, No. 1, 30.04.1997, p. 217-283.

Research output: Contribution to journalArticle

Ésik, Z. / Completeness of Park induction. In: Theoretical Computer Science. 1997 ; Vol. 177, No. 1. pp. 217-283.
@article{c7b49abf04164e2b932e04e49ede0df0,
title = "Completeness of Park induction",
abstract = "The (in)equational properties of iteration, i.e., least (pre-)fixed point solutions over cpo's, are captured by the axioms of iteration theories. All known axiomatizations of iteration theories consist of the Conway identities and a complicated equation scheme, the commutative identity. The results of this paper show that the commutative identity is implied by the Conway identities and a weak form of the Park induction principle. Hence, we obtain a simple first order axiomatization of the (in)equational theory of iteration. It follows that a few simple identities and a weak form of the Scott induction principle, formulated to involve only inequations, are also complete. We also show that the Conway identities and the Park induction principle are not complete for the universal Horn theory of iteration.",
author = "Z. {\'E}sik",
year = "1997",
month = "4",
day = "30",
language = "English",
volume = "177",
pages = "217--283",
journal = "Theoretical Computer Science",
issn = "0304-3975",
publisher = "Elsevier",
number = "1",

}

TY - JOUR

T1 - Completeness of Park induction

AU - Ésik, Z.

PY - 1997/4/30

Y1 - 1997/4/30

N2 - The (in)equational properties of iteration, i.e., least (pre-)fixed point solutions over cpo's, are captured by the axioms of iteration theories. All known axiomatizations of iteration theories consist of the Conway identities and a complicated equation scheme, the commutative identity. The results of this paper show that the commutative identity is implied by the Conway identities and a weak form of the Park induction principle. Hence, we obtain a simple first order axiomatization of the (in)equational theory of iteration. It follows that a few simple identities and a weak form of the Scott induction principle, formulated to involve only inequations, are also complete. We also show that the Conway identities and the Park induction principle are not complete for the universal Horn theory of iteration.

AB - The (in)equational properties of iteration, i.e., least (pre-)fixed point solutions over cpo's, are captured by the axioms of iteration theories. All known axiomatizations of iteration theories consist of the Conway identities and a complicated equation scheme, the commutative identity. The results of this paper show that the commutative identity is implied by the Conway identities and a weak form of the Park induction principle. Hence, we obtain a simple first order axiomatization of the (in)equational theory of iteration. It follows that a few simple identities and a weak form of the Scott induction principle, formulated to involve only inequations, are also complete. We also show that the Conway identities and the Park induction principle are not complete for the universal Horn theory of iteration.

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

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

M3 - Article

VL - 177

SP - 217

EP - 283

JO - Theoretical Computer Science

JF - Theoretical Computer Science

SN - 0304-3975

IS - 1

ER -