Marginalia to a Theorem of Jacopini

Issue title: Typed Lambda Calculi and Applications (TLCA'99)

Article type: Research Article

Authors: Statman, Rick

Abstract: In 1975, G. Jacopini proved the existence of an easy term, i.e., a term which can be consistently (with beta conversion) identified with any other term. In 1980, A. Visser generalized Jacopini's result to R.E. theories; namely, easy terms for consistent (with beta conversion) R.E. theories exist. Of course, no such generalization for non-R.E. theories exists. For example, it is easy to see that there is no easy term for Barendregt's theory H. In this note we shall generalize Jacopini's result to non-R.E. theories as follows. Say that an equation M=N is easy if for any consistent (with beta conversion) extension T we have that T∪{M=N} is consistent. We shall prove that easy equations exist.

Keywords: Lambda calculus, consistency

Journal: Fundamenta Informaticae, vol. 45, no. 1-2, pp. 117-121, 2001