摘要: Abstract BCK-λ-terms are the λ-terms in which each variable occurs at most once. The principal type of a λ-term is general term. In this paper we prove that if two β-normal form have same then they identical. This solves following problem (Y. Komori, 1987) more form: closed βη-normal assigned to minimal BCK-formula, identical? A BCK-formula formula among BCK-provable formulas with respect substitutions for variables. To analyze assignment, notion “connection” introduced. connection series occurrences assignment figure. Connected meaning. distinct classes can be rewritten separately; as result, assignment. By “formulae-as-types” correspondence, result implies uniqueness normal proof figure BCK-formulas. valid BCI-logic or implicational fragment linear logic well.
elsevier.com
sci-hub.se 参考文章(17)
Hiroakira Ono, Structural Rules and a Logical Hierarchy Springer, Boston, MA. pp. 95- 104 ,(1990) , 10.1007/978-1-4613-0609-2_8
Mariangiola Dezani-Ciancaglini, J.Roger Hindley, Intersection types for combinatory logic Theoretical Computer Science. ,vol. 100, pp. 303- 324 ,(1992) , 10.1016/0304-3975(92)90306-Z
J.Roger Hindley, BCK-combinators and linear l-terms have types Theoretical Computer Science. ,vol. 64, pp. 97- 105 ,(1989) , 10.1016/0304-3975(89)90100-X
A. A. Babaev, S. V. Solov'ev, A coherence theorem for canonical morphisms in cartesian closed categories Journal of Mathematical Sciences. ,vol. 20, pp. 2263- 2279 ,(1982) , 10.1007/BF01629434
R. Hindley, The Principal Type-Scheme of an Object in Combinatory Logic Transactions of the American Mathematical Society. ,vol. 146, pp. 29- 60 ,(1969) , 10.1090/S0002-9947-1969-0253905-6
Robin Milner, Fully abstract models of typed λ-calculi Theoretical Computer Science. ,vol. 4, pp. 1- 22 ,(1977) , 10.1016/0304-3975(77)90053-6
J. Roger Hindley, David Meredith, Principal type-schemes and condensed detachment Journal of Symbolic Logic. ,vol. 55, pp. 90- 105 ,(1990) , 10.2307/2274956
J. Roger Hindley, Introduction to combinators and [lambda]-calculus ,(1986)
Grigori Mints, Tanel Tammet, Condensed Detachment is Complete for Relevance Logic: A Computer-Aided Proof Journal of Automated Reasoning. ,vol. 7, pp. 587- 596 ,(1991) , 10.1007/BF01880330
Robert K. Meyer, Martin W. Bunder, Lawrence Powers, Implementing the "Fool's model" of combinatory logic Journal of Automated Reasoning. ,vol. 7, pp. 597- 630 ,(1991) , 10.1007/BF01880331