The typed Böhm theorem

Abstract

A proof of the analogue of Böhm's theorem in the typed lambda calculus with only functional types was presented. In order to use the finite model property of the typed lambda calculus, P-functionals were used as the elements of the sets obtained from a finite set P. It was shown that every P-functional is lambda-definable in the sense that for two lambda terms a and b whose interpretations in a finite model based on P are not equal, there is a syntactical procedure deriving [m] = [n] from a type instance of a = b , where m and n are Church numerals. The approach was shown to provide an alternative proof of this type-reducing result.