Principal types of BCK-lambda-terms (Q1208417)

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.