<div dir="ltr"><div>@Jon: The main point is indeed to have decidable typechecking, not normalization per se. Thanks for clarifying.</div><div><br></div><div>@Thorsten: But we *can* reduce the term when we give it the actual termination proof, the point here is only that the termination proof is not irrelevant for checking conversion. When compiling the code to Haskell, Agda even detects that Acc does not contain any interesting information and erases the termination proofs, so there's no run-time cost, only a compile-time one.</div><div><br></div><div>-- Jesper<br></div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Wed, May 1, 2019 at 5:17 PM Thorsten Altenkirch <<a href="mailto:Thorsten.Altenkirch@nottingham.ac.uk">Thorsten.Altenkirch@nottingham.ac.uk</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">That is not really an argument.<br>
<br>
Clearly there are many situations where we would like to reduce a term which will only terminate in a consistent context. E.g. we can reduce terms which are only guarded by a proof of well-foundedness. Another situation is wether you can reduce a coercion which relies on an equality proof. The latter could lead to a failure of type-soundness but does it matter when we execute symbolically (i.e. not at run-time).<br>
<br>
I don't say that the answer is always that we shouldn't care, but I was asking for better arguments why we should.<br>
<br>
Thorsten<br>
<br>
On 01/05/2019, 15:35, "Agda on behalf of Jon Sterling" <<a href="mailto:agda-bounces@lists.chalmers.se" target="_blank">agda-bounces@lists.chalmers.se</a> on behalf of <a href="mailto:jon@jonmsterling.com" target="_blank">jon@jonmsterling.com</a>> wrote:<br>
<br>
    To respond to Thorsten's comments a bit further down the thread, I tried really hard to make proof assistants without a complete decision procedure for typing practical, and I determined that it is not likely to work out. Decidable type checking is good.<br>
<br>
<br>
<br>
<br>
<br>
<br>
This message and any attachment are intended solely for the addressee<br>
and may contain confidential information. If you have received this<br>
message in error, please contact the sender and delete the email and<br>
attachment. <br>
<br>
Any views or opinions expressed by the author of this email do not<br>
necessarily reflect the views of the University of Nottingham. Email<br>
communications with the University of Nottingham may be monitored <br>
where permitted by law.<br>
<br>
<br>
<br>
<br>
_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
</blockquote></div>