Two Problems on Reduction Graphs in Lambda Calculus

Article type: Research Article

Authors: Intrigila, Benedetto | Laurenzi, Anna R.

Abstract: In this paper we solve two open problems in the theory of reduction graphs in lambda calculus. The first question is whether the condensed reduction graph of a lambda term is always locally finite (conjecture of M.Venturini Zilli 1984). We give a negative answer to the conjecture by providing a counterexample. The second problem is whether there is a term such that its reduction graph is composed of two reduction cycles (not loops) intersecting in just one point (problem of J.W.Klop 1980). We show that such a term cannot exist.

Keywords: Lambda calculus, reduction graphs, reduction cycles

Journal: Fundamenta Informaticae, vol. 44, no. 1-2, pp. 133-144, 2000