2

In the question about non-termination With clauses obscuring termination an answer suggests to recourse to <-wellFounded.

I looked at the definition of <-wellFounded before, and it strikes me there is a --safe in OPTIONS. Is it meant to work without this option? That is, is using --safe some optimisation, or is it working around some fundamental problem? So in this case we just delegate the termination problem to a function marked as "safe"?

Sassa NF
  • 5,306
  • 15
  • 22
  • You should have a look (maybe you already did) at the following wiki page which explains what safe stands for: https://agda.readthedocs.io/en/v2.6.0.1/language/safe-agda.html. From my understanding, it's better for a function to be in a safe context (obviously) because no unsafe pragmas or such are accepted inside the module where it is defined - or any imported module. It makes sense for the well-foundness to be marked as safe because it messes with soundness of proofs and such. – MrO Nov 13 '19 at 21:56
  • 1
    @MrO well-foundedness does not mess with anything. It is plain and vanilla Agda, using only core features which have been available since ages. – András Kovács Nov 13 '19 at 22:20
  • @AndrásKovács Ofc this is not what I meant, sorry if I wasn't clear enough. I meant that, since well-foundedness deals with termination, if it was allowed not to be safe, then it could lead to inconsistencies. Hopefully my point is clearer this time ! – MrO Nov 13 '19 at 22:22
  • Well-foundedness does not have special features with respect to termination, and most of the standard lib is sprinkled with `--safe` in any case. – András Kovács Nov 13 '19 at 22:29
  • @AndrásKovács Thanks. I did see the well-founded defined for a few things that were obviously terminating, but it is not always the indicator that it is obvious to Agda. There's a follow-up question: https://stackoverflow.com/questions/58899323/how-to-choose-the-design-for-a-well-founded-inductive-type – Sassa NF Nov 17 '19 at 10:02

1 Answers1

4

It is completely safe. --safe holds a module to a stricter standard than default. It does not mean that something is unsafe, it means that something is safe. Using well-founded recursion from any module, safe or not, will not introduce non-termination. Termination is rather strongly baked into the inductive definition of accessibility.

András Kovács
  • 29,931
  • 3
  • 53
  • 99