4
$\begingroup$

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?

$\endgroup$
6
$\begingroup$

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.

$\endgroup$
  • $\begingroup$ 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"). $\endgroup$ – Blaisorblade Jun 14 '18 at 10:17
  • $\begingroup$ 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? $\endgroup$ – Łukasz Lew Jun 14 '18 at 16:01
  • $\begingroup$ @ŁukaszLew No, evaluation strategies do not get inherited in this manner. $\endgroup$ – cody Jun 14 '18 at 18:58
  • $\begingroup$ 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? $\endgroup$ – Łukasz Lew Jun 14 '18 at 22:37
  • $\begingroup$ @Ł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). $\endgroup$ – cody Jun 15 '18 at 12:51

Your Answer

By clicking "Post Your Answer", you acknowledge that you have read our updated terms of service, privacy policy and cookie policy, and that your continued use of the website is subject to these policies.

Not the answer you're looking for? Browse other questions tagged or ask your own question.