Principal types of BCK-lambda-terms
type: Item
instance of: scholarly article
title: Principal types of BCK-lambda-terms
zbMATH Open document ID: 0770.03006
DOI: 10.1016/0304-3975(93)90171-O
author: Sachio Hirokawa
published in: Theoretical Computer Science
publication date: 1993-05-16T00:00:00Z
review text: A BCK-\(\lambda\)-term is one in which each variable appears at most once. A pair \(\langle B,\alpha\rangle\) of a set of type assignments to variables \(B\) and a type \(\alpha\), is said to be a principal pair if \(B\lvdash M: \alpha'\) whenever \(\alpha'\) is a substitution instance of \(\alpha\). If \(B\) is empty (and so \(M\) is closed), \(\alpha\) is the principal type scheme of \(M\). In this paper the author gives a characterization of principal pairs for BCK-\(\lambda\)-terms using a new notion of ``connection'' between types in a type assignment figure. From this he is able to show that if two closed BCK-\(\lambda\)-terms in \(\beta\)-normal form have the same principal type then they are identical (modulo \(\alpha\)-conversion). A type \(\alpha\) is BCK-minimal if it is not a nontrivial substitution instance of any BCK-type. It follows that if two closed BCK-\(\lambda\)- terms in \(\beta\)-normal form have the same minimal types then these are also identical (modulo \(\alpha\)-conversion). This resolves a conjecture of Komori. By the formulas as types isomorphism, it also follows that the corresponding minimal theorems of BCK-implicational logic have unique normalized proofs.
Mathematics Subject Classification ID: 03B40
Mathematics Subject Classification ID: 68N15
zbMATH DE Number: 166428
zbMATH Keywords: BCK-minimal type
zbMATH Keywords: BCK-\(\lambda\)-term
zbMATH Keywords: type assignments
zbMATH Keywords: principal type scheme
zbMATH Keywords: BCK-type
zbMATH Keywords: BCK-implicational logic
zbMATH Keywords: normalized proofs
reviewed by: Martin W. Bunder
describes a project that uses: ML
MaRDI profile type: Publication
cites work: Q3866104
cites work: Q3691634
cites work: Q3352995
cites work: Combinatory logic. With two sections by William Craig.
cites work: Combinatory logic. Vol. II
cites work: Intersection types for combinatory logic
cites work: Linear logic
cites work: The Principal Type-Scheme of an Object in Combinatory Logic
cites work: BCK-combinators and linear \(\lambda\)-terms have types
cites work: BCK and BCI logics, condensed detachment and the 2-property
cites work: Principal type-schemes and condensed detachment
cites work: Q4722037
cites work: Über Tautologien, in Welchen Keine Variable Mehr Als Zweimal Vorkommt
cites work: Q3727946
cites work: Coherence and valid isomorphism in closed categories applications of proof theory to category theory in a computer sclentist perspective
cites work: Why commutative diagrams coincide with equivalent proofs
cites work: Implementing the `Fool's model' of combinatory logic
cites work: Fully abstract models of typed \(\lambda\)-calculi
cites work: A theory of type polymorphism in programming
cites work: Condensed detachment is complete for relevance logic: A computer-aided proof
cites work: Q4694214
cites work: Logics without the contraction rule
cites work: Q5559220
cites work: Principal type scheme and unification for intersection type discipline
description: scientific article; zbMATH DE number 166428