Timeline for How to convince Agda that definition is terminating in the presence of unapplied recursion?
Current License: CC BY-SA 4.0
13 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Oct 14, 2022 at 19:58 | vote | accept | TerminationCheckFailed | ||
| Oct 14, 2022 at 18:34 | answer | added | Andrej Bauer | timeline score: 4 | |
| Oct 14, 2022 at 18:00 | comment | added | TerminationCheckFailed | @AndrejBauer I've updated the example. | |
| Oct 14, 2022 at 17:59 | history | edited | TerminationCheckFailed | CC BY-SA 4.0 |
added 319 characters in body
|
| Oct 14, 2022 at 17:54 | comment | added | Andrej Bauer |
Could you also include All just to make the example self-contained?
|
|
| Oct 14, 2022 at 17:52 | comment | added | TerminationCheckFailed |
At first I tried making a "depth" metric which allowed to define Value : ∀{n T} → Depth n T → Set. To remove the depth argument I made a function that calculates depth for any Type and then passes it to Value, but this function suffered the original problem. As @Nift suggested, unrolling All in plain Value or All.tabulate in my function allows them to pass termination checker. It doesn't seem to pose any problems besides disallowing to use Alls properties which I probably don't need anyway.
|
|
| Oct 14, 2022 at 12:00 | comment | added | TerminationCheckFailed | @AndrejBauer I've updated the post with an example. I don't know how recursion can be avoided there. | |
| Oct 14, 2022 at 11:54 | history | edited | TerminationCheckFailed | CC BY-SA 4.0 |
added 200 characters in body
|
| Oct 14, 2022 at 8:44 | comment | added | Andrej Bauer | Can you give an example that is not trivially fixed by avoiding the recursion, and gives an equivalent result? | |
| Oct 14, 2022 at 7:32 | comment | added | James Wood |
The code examples here are perhaps too simplified, making it hard to see which solutions are acceptable. For example, A P always has 1 inhabitant, so Df n could just be ⊤ in all cases. Maybe you want to make A a postulate or parameter, but, as I say, it's hard to know.
|
|
| Oct 14, 2022 at 0:56 | comment | added | Ilk |
A naive solution would be to unroll the definition of All in a recursive form, by defining branches of Value (struct []) = ⊤, Value (struct (x ∷ xs)) = Value x × Value (struct xs), but that might not be the solution you are looking for. A naive well-founded recursion would fail in your Df case, as Df takes no arguments in the recursive call and similarly in the Value case, you would have to essentially construct a proof about equivalence of the All definition to some well-founded recursive call, but the proof might allow you to use preexisting facts about All.
|
|
| S Oct 13, 2022 at 23:23 | review | First questions | |||
| Oct 14, 2022 at 5:19 | |||||
| S Oct 13, 2022 at 23:23 | history | asked | TerminationCheckFailed | CC BY-SA 4.0 |