Probabilistic Approach to the Lambda Definability for Fourth Order Types

It has been proved by Loader [Ralph Loader, The Undecidability of λ - Definability, In Logic, Meaning and Computation: Essays in Memory of Alonzo Church, 331-342, C.A. Anderson and Zeleny editors, Kluwer Academic Publishers, 2001] that Statman-Plotkin conjecture (see [Richard. Statman. Equality of functionals revisited, in L.A. Harrington et al. (Eds.), Harvey Friedman's Research on the Foundations of Mathematics, North-Holland, Amsterdam, 1985, 331-338] and [Gordon D. Plotkin. λ definability and logical relations, Memorandum SAI-RM-4, School of Artificial Intelligence, University of Edinburgh, Ocober 1973]) fails. The Loader proof was done by encoding the word problem in the full type hierarchy based on the domain with 7 elements. The aim of this paper is to show that the lambda definability problem limited to regular fourth order types is decidable in any finite domain. Obviously λ definability is decidable for 1, 2 and 3 order types. As an additional effect of the result described we may observe that for certain types there is no finite context free grammar generating all closed terms. We prove also that probability that randomly chosen fourth order type (or type of the order not grater then 4 ) admits decidable lambda definability problem is zero.