<p>If you implement an evaluator for the terms of a language $A$ in a total system $B$, and you have furthermore <strong>proven that your evaluator is correct</strong>, that is for every $t$ well-typed in $A$,</p>

<p>$$\mathrm{eval}(t) \simeq_A t $$</p>

<p>where $\simeq_A$ is the equality in $A$, then you have only shown that $\simeq_A$ is decidable.</p>

<p>If furthermore $\simeq_A$ naturally leads to a notion of reduction $\rightarrow_A$, and $\mathrm{eval}(t)$ is always in normal form, then you have proven that every term $t$ in $A$ is equivalent to a term in normal form.</p>

<p>This is enough for consistency of $A$ but is <strong>not</strong> equivalent to weak normalization, unless $\rightarrow_A$ is furthermore <a href="http://mathworld.wolfram.com/Church-RosserProperty.html" rel="nofollow noreferrer">church-rosser</a>!</p>

<p>This is essentially the approach taken by <a href="https://en.wikipedia.org/wiki/Normalisation_by_evaluation" rel="nofollow noreferrer">normalization by evaluation</a>.</p>

<p>A proof of weak normalization in a constructive logic naturally leads to an evaluator, as every $\forall\exists$ statement leads to an algorithm (correct by construction).</p>

<p>There is a nice article by Ulrich Berger, <em><a href="https://link.springer.com/chapter/10.1007/BFb0037100" rel="nofollow noreferrer">Program extraction from normalization proofs</a></em>, which implements this idea for simply typed $\lambda$-calculus.</p>

<hr>

<p>For your second question, here is a counter example. Consider the language $A$ to have only two terms, $\Delta$ and $\bot$, with the reduction rules</p>

<p>$$\Delta\rightarrow \Delta $$
$$\Delta\rightarrow \bot $$</p>

<p>Feel free to add types if you like. The computation rules are weakly normalizing and confluent.</p>

<p>In Coq, you might write the <code>eval</code> function thus:</p>

<pre><code>Fixpoint eval (t : A) : A :=
  match t with
     | Delta =&gt; Bottom
     | Bottom =&gt; Bottom
</code></pre>

<p>It's not too hard to prove that if $t\leftrightarrow^* u$ then <code>eval(t) = eval(u)</code>. Coq's reduction can be taken to be non-deterministic, in which case you have a counter-example to the SN "inheritance" that you expect.</p>

CC BY-SA 4.0
2018-06-14T10:17:50.107Z
To answer the last question more explicitly: having an evaluator (even with all the above assumption) does not prove strong normalization *because* an evaluator considers one way to reduce the term, but strong normalization talks about _all_ ways of reducing the term — as soon as reduction is non-deterministic, the two are different.
(If reduction is deterministic, arguably weak and strong normalization coincide, but I would just talk of "normalization" there, even if the literature does also use "strong normalization").
Blaisorblade
CC BY-SA 4.0
2018-06-14T16:01:05.707Z
If the host language is also non-deterministic and strongly normalizing and reduction in the client language correspond to reductions in the client language, then SN would be proven right?
Łukasz Lew
CC BY-SA 4.0
2018-06-14T18:58:28.497Z
@ŁukaszLew No, evaluation strategies do not get inherited in this manner.
cody
CC BY-SA 4.0
2018-06-14T22:37:19.413Z
I see now that normalization by evaluation reflects the condition $t\leftrightarrow^* u \implies \mathtt{eval}(u) = \mathtt{eval}(t)$. For the "SN inheritance" I was thinking about evaluator implementation that would have the property $u \rightarrow t \implies \mathtt{eval}(u) \rightarrow^* \mathtt{eval}(t)$, which is a simulation relation (as in bisimulation). (Perhaps there is a better definition) Does such approach exists? Meta question: What's the etiquette: should I 'Edit' the question and expand it or ask in comments the way I'm doing now or ask new question?
Łukasz Lew
CC BY-SA 4.0
2018-06-15T12:51:23.333Z
@ŁukaszLew I believe asking a new question is the way to go, though you might want to go to cs.stackexchange if you feel your question is not research-level (and I'm not sure this one is).
cody
CC BY-SA 4.0
2018-06-12T14:27:48.000Z
2018-06-14T19:07:31.310Z
2018-06-14T19:07:31.310Z
cody
<p>Implementing an normalization (cut elimination) procedure for a type system A in a language with a total type system B, automatically proves cut elimination for type system A since the implementation will be total.</p>

<p>What's the difference between proving weak normalization and implementing the evaluator?</p>

<p>If there is none, is that effect also present in proving consistency of all the mathematical proof systems?</p>

<p>The same question in a strong normalization setting:
If the host language is strongly normalizing does strong normalization of client language follows?</p>

<lo.logic><type-theory><type-systems><normalization>
What's the difference between proving weak normalization and implementing evaluator?
Łukasz Lew
# What's the difference between proving weak normalization and implementing evaluator?

(Asked by: username_0 on 2018-06-12)

Implementing an normalization (cut elimination) procedure for a type system A in a language with a total type system B, automatically proves cut elimination for type system A since the implementation will be total.

What's the difference between proving weak normalization and implementing the evaluator?

If there is none, is that effect also present in proving consistency of all the mathematical proof systems?

The same question in a strong normalization setting:
If the host language is strongly normalizing does strong normalization of client language follows?

**Tags:** lo.logic, type-theory, type-systems, normalization

---

## 1 answers

### Answer by username_1 on 2018-06-12. Score: 7 | Accepted answer

If you implement an evaluator for the terms of a language $A$ in a total system $B$, and you have furthermore proven that your evaluator is correct, that is for every $t$ well-typed in $A$,
$$\mathrm{eval}(t) \simeq_A t $$
where $\simeq_A$ is the equality in $A$, then you have only shown that $\simeq_A$ is decidable.
If furthermore $\simeq_A$ naturally leads to a notion of reduction $\rightarrow_A$, and $\mathrm{eval}(t)$ is always in normal form, then you have proven that every term $t$ in $A$ is equivalent to a term in normal form.
This is enough for consistency of $A$ but is not equivalent to weak normalization, unless $\rightarrow_A$ is furthermore church-rosser!
This is essentially the approach taken by normalization by evaluation.
A proof of weak normalization in a constructive logic naturally leads to an evaluator, as every $\forall\exists$ statement leads to an algorithm (correct by construction).
There is a nice article by Ulrich Berger, Program extraction from normalization proofs, which implements this idea for simply typed $\lambda$-calculus.

For your second question, here is a counter example. Consider the language $A$ to have only two terms, $\Delta$ and $\bot$, with the reduction rules
$$\Delta\rightarrow \Delta $$
$$\Delta\rightarrow \bot $$
Feel free to add types if you like. The computation rules are weakly normalizing and confluent.
In Coq, you might write the eval function thus:
Fixpoint eval (t : A) : A :=
  match t with
     | Delta => Bottom
     | Bottom => Bottom

It's not too hard to prove that if $t\leftrightarrow^* u$ then eval(t) = eval(u). Coq's reduction can be taken to be non-deterministic, in which case you have a counter-example to the SN "inheritance" that you expect.

> **Comments:**
> **username_2**: To answer the last question more explicitly: having an evaluator (even with all the above assumption) does not prove strong normalization *because* an evaluator considers one way to reduce the term, but strong normalization talks about _all_ ways of reducing the term — as soon as reduction is non-deterministic, the two are different. (If reduction is deterministic, arguably weak and strong normalization coincide, but I would just talk of "normalization" there, even if the literature does also use "strong normalization").  
> **username_0**: If the host language is also non-deterministic and strongly normalizing and reduction in the client language correspond to reductions in the client language, then SN would be proven right?  
> **username_1**: @ŁukaszLew No, evaluation strategies do not get inherited in this manner.  
> **username_0**: I see now that normalization by evaluation reflects the condition $t\leftrightarrow^* u \implies \mathtt{eval}(u) = \mathtt{eval}(t)$. For the "SN inheritance" I was thinking about evaluator implementation that would have the property $u \rightarrow t \implies \mathtt{eval}(u) \rightarrow^* \mathtt{eval}(t)$, which is a simulation relation (as in bisimulation). (Perhaps there is a better definition) Does such approach exists? Meta question: What's the etiquette: should I 'Edit' the question and expand it or ask in comments the way I'm doing now or ask new question?  
> **username_1**: @ŁukaszLew I believe asking a new question is the way to go, though you might want to go to cs.stackexchange if you feel your question is not research-level (and I'm not sure this one is).  

---

