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.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
Babaev, A.A., Solov'ev, S.V., A coherence theorem for canonical morphism in cartesian closed categories, Zapiski nauchnykh Seminarov Lenigradskogo Otdeleniya matematichskogo Instituta im. V.A. Steklova An SSSR 88 (1979) 3–29.
Girard, J.-Y., Linear logic, Theoret. Comput. Sci. 50 (1987) 1–101.
Hindley, J.R., Seldin, J.P., Introduction to Combinators and Lambda-Calculus (Cambridge University Press, London, 1986)
Hindley, J.R., BCK-combinators and linear lambda-terms have types, Theoret. Comput. Sci. 64 (1989) 97–105.
Hindley, J.R., BCK and BCI logics, condensed detachment and the 2-property, a summary, Report, University of Wolongon, Aug 1990.
Hirokawa, S., Principal types of BCK-lambda terms, submitted.
Hirokawa, S., Principal type assignment to lambda terms, submitted.
Hirokawa, S., Converse principal-type-scheme theorem in lambda-calculus, Studia Logica (to appear).
Hirokawa, S., Linear lambda-terms and coherence theorem, preprint.
Howard, W.A., The formulae-as-types notion of construction, in: Hindley and Seldin Ed., To H.B. Curry, Essays on Combinatory Logic, Lambda Calculus and Formalism (Academic Press, 1980) 479–490.
Jaskowski, S., Über Tautologien, in welchen keine Variable mehr Als zweimal vorkommt, Zeitchrift für Math. Logic 9 (1963) 219–228.
Komori, Y., BCK algebras and lambda calculus, in: Proc. 10th Symp. on Semigroups, Sakado 1986, (Josai University, Sakado 1987) 5–11.
Mints, G.E., A simple proof of the coherence theorem for cartesian closed categories, Manuscript 1982.
Lambek,J., Scott,P.J., Introduction to higher order categorical logic, (Cambridge University Press, 1986)
Ono, H., Komori, Y., Logics without the contraction rule, J. Symbolic Logic 50 (1985) 169–201.
Tatsuta, M., Uniqueness of normal proofs in implicational logic, Manuscript, Sep 1988.
Wronski, A., On Bunder and Meyer's theorem, Manuscript, Aug 1987.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1991 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Hirokawa, S. (1991). BCK-formulas having unique proofs. In: Pitt, D.H., Curien, PL., Abramsky, S., Pitts, A.M., Poigné, A., Rydeheard, D.E. (eds) Category Theory and Computer Science. CTCS 1991. Lecture Notes in Computer Science, vol 530. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0013460
Download citation
DOI: https://doi.org/10.1007/BFb0013460
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-54495-1
Online ISBN: 978-3-540-38413-7
eBook Packages: Springer Book Archive