Is it possible to determine if a reduction is correct?

Suppose we have an arbitrary term, x, in Lambda Calculus, or in an equivalent turing-complete system. Suppose we ask an oracle what is the normal form of that term, and it answers y. Is it possible to determine, in finite time, if the oracle answer's ir correct?

Secondary question: is there any system (non-turing complete, perhaps) where that would be possible?

• If you're asking because you're building a compiler, a standard method is to use proof-carrying code: the "oracle" that computes the normal form also collects, along the way, a proof that it has done its job correctly. There is a lot of literature about how to do this and how to reduce the impact on compiler design and maintenance.
– D.W.
Jun 6 '14 at 6:05
• @D.W. So it is possible for one to reduce a term in SKI calculus that has big complexity and thus takes a lot of time (say, months), and at the same time provide a proof that will allow anyone to verify that is correct in a few seconds? That is what I want, specifically. Jun 7 '14 at 13:26

$L:=\{ (t,u)\in\Lambda\times\Lambda \mathrel{|} t \rightarrow^* u, u \textrm{ normal}\}$
(with $\Lambda$ being the set of $\lambda$-terms). This is obviously not the case: for every Turing machine $M$, there is a $\lambda$-term $t_M$ (effectively computable from the description of $M$) such that $t_M$ reduces to a fixed normal form $u$ if $M$ terminates on the empty string and has no normal form otherwise; therefore, if $L$ were decidable, we would be able to decide the halting problem for $M$ on empty input by asking whether $(t_M,u)\in L$.