[Prev][Next][Index][Thread]
Paper available by ftp
The following is available by anonymous FTP from theory.doc.ic.ac.uk
in directory /theory/papers/Loader/ in the files define.dvi and define.ps.Z
`The Undecidability of Lambda Definability'
by R. Loader
Abstract. I show that in a model of the simply typed lambda calculus
which is finite at each type, the problem of deciding whether a given
object is definable by a term, is undecidable. (This (or rather its
negation) is known as the Statman-Plotkin conjecture.) This is done
by encoding word problems.