Strong Typed Böhm Theorem and Functional Completeness on the Linear Lambda Calculus

Satoshi Matsuoka
(National Institute of Advanced Industrial Science and Technology)

In this paper, we prove a version of the typed Böhm theorem on the linear lambda calculus, which says, for any given types A and B, when two different closed terms s1 and s2 of A and any closed terms u1 and u2 of B are given, there is a term t such that t s1 is convertible to u1 and t s2 is convertible to u2. 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 s1 and s2, then A is functionally complete with regard to s1 and s2. So far, it was only known that a few types are functionally complete.

In Robert Atkey and Neelakantan Krishnaswami: Proceedings 6th Workshop on Mathematically Structured Functional Programming (MSFP 2016), Eindhoven, Netherlands, 8th April 2016, Electronic Proceedings in Theoretical Computer Science 207, pp. 1–22.
Published: 1st April 2016.

ArXived at: http://dx.doi.org/10.4204/EPTCS.207.1 bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org