Strong Typed Bohm Theorem and Functional Completeness on the Linear Lambda Calculus

In this paper, we prove a version of the typed Bohm theorem on the linear lambda calculus, which says, for any given types A and B, when two different closed terms s(1) and s(2) of A and any closed terms u(1) and u(2) of B are given, there is a term t such that t s(1) is convertible to u(1) and t s(2) is convertible to u(2). Several years ago, a weaker version of this theorem was proved, but the stronger version was open. As a corollary of this theorem, we prove that if A has two different closed terms s(1) and s(2), then A is functionally complete with regard to s(1) and s(2). So far, it was only known that a few types are functionally complete.