BCK-formulas having unique proofs

Research output: Chapter in Book/Report/Conference proceedingConference contribution

3 Citations (Scopus)

Abstract

The set of relevantly balanced formulas is introduced in implicational fragment of BCK-logic. It is shown that any relevantly balanced formula has unique normal form proof. Such formulas are defined by the ‘relevance relation’ between type variables in a formula. The set of balanced formulas (or equivalently one-two-formulas) is included in the relevantly balanced formulas. The uniqueness of normal form proofs is known for balanced formulas as the coherence theorem. Thus the result extends the theorem with respect to implicational formulas. The set of relevantly balanced formulas is characterized as the set of irrelevant substitution instances of principal type-schemes of BCK-λ-terms.

Original languageEnglish
Title of host publicationCategory Theory and Computer Science, Proceedings
EditorsDavid H. Pitt, Pierre-Louis Curien, Samson Abramsky, Axel Poigne, David E. Rydeheard, Andrew M. Pitts
PublisherSpringer Verlag
Pages106-120
Number of pages15
ISBN (Print)9783540544951
DOIs
Publication statusPublished - Jan 1 1991
Event4th Biennial Summer Conference on Category Theory and Computer Science, 1991 - Paris, France
Duration: Sep 3 1991Sep 6 1991

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume530 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Other

Other4th Biennial Summer Conference on Category Theory and Computer Science, 1991
CountryFrance
CityParis
Period9/3/919/6/91

Fingerprint

Substitution reactions
Normal Form
Theorem
Substitution
Fragment
Uniqueness
Logic
Term

All Science Journal Classification (ASJC) codes

  • Theoretical Computer Science
  • Computer Science(all)

Cite this

Hirokawa, S. (1991). BCK-formulas having unique proofs. In D. H. Pitt, P-L. Curien, S. Abramsky, A. Poigne, D. E. Rydeheard, & A. M. Pitts (Eds.), Category Theory and Computer Science, Proceedings (pp. 106-120). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 530 LNCS). Springer Verlag. https://doi.org/10.1007/BFb0013460

BCK-formulas having unique proofs. / Hirokawa, Sachio.

Category Theory and Computer Science, Proceedings. ed. / David H. Pitt; Pierre-Louis Curien; Samson Abramsky; Axel Poigne; David E. Rydeheard; Andrew M. Pitts. Springer Verlag, 1991. p. 106-120 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 530 LNCS).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Hirokawa, S 1991, BCK-formulas having unique proofs. in DH Pitt, P-L Curien, S Abramsky, A Poigne, DE Rydeheard & AM Pitts (eds), Category Theory and Computer Science, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 530 LNCS, Springer Verlag, pp. 106-120, 4th Biennial Summer Conference on Category Theory and Computer Science, 1991, Paris, France, 9/3/91. https://doi.org/10.1007/BFb0013460
Hirokawa S. BCK-formulas having unique proofs. In Pitt DH, Curien P-L, Abramsky S, Poigne A, Rydeheard DE, Pitts AM, editors, Category Theory and Computer Science, Proceedings. Springer Verlag. 1991. p. 106-120. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). https://doi.org/10.1007/BFb0013460
Hirokawa, Sachio. / BCK-formulas having unique proofs. Category Theory and Computer Science, Proceedings. editor / David H. Pitt ; Pierre-Louis Curien ; Samson Abramsky ; Axel Poigne ; David E. Rydeheard ; Andrew M. Pitts. Springer Verlag, 1991. pp. 106-120 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).
@inproceedings{3c1dc5e4f1a0496da1115c3b5f88c93f,
title = "BCK-formulas having unique proofs",
abstract = "The set of relevantly balanced formulas is introduced in implicational fragment of BCK-logic. It is shown that any relevantly balanced formula has unique normal form proof. Such formulas are defined by the ‘relevance relation’ between type variables in a formula. The set of balanced formulas (or equivalently one-two-formulas) is included in the relevantly balanced formulas. The uniqueness of normal form proofs is known for balanced formulas as the coherence theorem. Thus the result extends the theorem with respect to implicational formulas. The set of relevantly balanced formulas is characterized as the set of irrelevant substitution instances of principal type-schemes of BCK-λ-terms.",
author = "Sachio Hirokawa",
year = "1991",
month = "1",
day = "1",
doi = "10.1007/BFb0013460",
language = "English",
isbn = "9783540544951",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Verlag",
pages = "106--120",
editor = "Pitt, {David H.} and Pierre-Louis Curien and Samson Abramsky and Axel Poigne and Rydeheard, {David E.} and Pitts, {Andrew M.}",
booktitle = "Category Theory and Computer Science, Proceedings",
address = "Germany",

}

TY - GEN

T1 - BCK-formulas having unique proofs

AU - Hirokawa, Sachio

PY - 1991/1/1

Y1 - 1991/1/1

N2 - The set of relevantly balanced formulas is introduced in implicational fragment of BCK-logic. It is shown that any relevantly balanced formula has unique normal form proof. Such formulas are defined by the ‘relevance relation’ between type variables in a formula. The set of balanced formulas (or equivalently one-two-formulas) is included in the relevantly balanced formulas. The uniqueness of normal form proofs is known for balanced formulas as the coherence theorem. Thus the result extends the theorem with respect to implicational formulas. The set of relevantly balanced formulas is characterized as the set of irrelevant substitution instances of principal type-schemes of BCK-λ-terms.

AB - The set of relevantly balanced formulas is introduced in implicational fragment of BCK-logic. It is shown that any relevantly balanced formula has unique normal form proof. Such formulas are defined by the ‘relevance relation’ between type variables in a formula. The set of balanced formulas (or equivalently one-two-formulas) is included in the relevantly balanced formulas. The uniqueness of normal form proofs is known for balanced formulas as the coherence theorem. Thus the result extends the theorem with respect to implicational formulas. The set of relevantly balanced formulas is characterized as the set of irrelevant substitution instances of principal type-schemes of BCK-λ-terms.

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

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

U2 - 10.1007/BFb0013460

DO - 10.1007/BFb0013460

M3 - Conference contribution

AN - SCOPUS:84972504615

SN - 9783540544951

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 106

EP - 120

BT - Category Theory and Computer Science, Proceedings

A2 - Pitt, David H.

A2 - Curien, Pierre-Louis

A2 - Abramsky, Samson

A2 - Poigne, Axel

A2 - Rydeheard, David E.

A2 - Pitts, Andrew M.

PB - Springer Verlag

ER -