<p>I don't know what your "oracle" is, but without further information what you are asking is whether the following language is decidable:</p>

<p>$L:=\{ (t,u)\in\Lambda\times\Lambda \mathrel{|} t \rightarrow^* u, u \textrm{ normal}\}$</p>

<p>(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$.</p>

<p>If your "oracle" gives more information, then of course the situation may very well be different.  For instance, if the oracle also gives an upper bound to the number of reduction steps needed to reach the purported normal form, then it is obviously decidable whether the oracle's answer is correct.</p>

<p>If you are actually asking about proof-carrying code (like D.W. suggests), please modify your question accordingly and I'll be happy to modify/remove my answer.</p>

CC BY-SA 3.0
2014-06-06T07:23:58.603Z
To the moderators: as it is, I'm not sure this is a research-level question (as you see, the answer is pretty obvious and standard).  If the OP doesn't give further information, is it maybe more appropriate to migrate this question to cs.stackexchange?
Damiano Mazza
CC BY-SA 3.0
2014-06-06T07:19:12.410Z
2014-06-06T07:19:12.410Z
Damiano Mazza
<p>Suppose we have an arbitrary term, <code>x</code>, 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 <code>y</code>. Is it possible to determine, in finite time, if the oracle answer's ir correct?</p>

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

CC BY-SA 3.0
2014-06-06T06:05:11.707Z
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.
CC BY-SA 3.0
2014-06-07T13:26:24.897Z
@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.
MaiaVictor
<pl.programming-languages><computability>
Is it possible to determine if a reduction is correct?
MaiaVictor
# Is it possible to determine if a reduction is correct?

(Asked by: username_0 on 2014-06-05)

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?

**Tags:** pl.programming-languages, computability
> **Comments:**
> **username_1**: 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.  
> **username_0**: @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.  

---

## 1 answers

### Answer by username_2 on 2014-06-06. Score: 4

I don't know what your "oracle" is, but without further information what you are asking is whether the following language is decidable:

$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$.

If your "oracle" gives more information, then of course the situation may very well be different. For instance, if the oracle also gives an upper bound to the number of reduction steps needed to reach the purported normal form, then it is obviously decidable whether the oracle's answer is correct.

If you are actually asking about proof-carrying code (like D.W. suggests), please modify your question accordingly and I'll be happy to modify/remove my answer.

> **Comments:**
> **username_2**: To the moderators: as it is, I'm not sure this is a research-level question (as you see, the answer is pretty obvious and standard).  If the OP doesn't give further information, is it maybe more appropriate to migrate this question to cs.stackexchange?  

---

