10
votes
Accepted
Termination and confluence -- which goes first?
As you have noticed there is no "natural" way to prove confluence and termination: to prove confluence from local confluence you need termination, but proving termination often depends on ...
- 506
8
votes
Accepted
Possible root cause(s) of the misunderstanding that DTT implies not Turing complete?
[Supplemental: I rewrote the answer so that any shred of vagueness is gone, as it was evoking religuous zeal, and I would prefer to stick to math. Everything is explained in terms of a widely accepted ...
- 9,812
6
votes
Accepted
How to prove termination of mutually recursive functions if only some decrease their arguments?
The trick is to "order" the functions themselves by using a product as the measure. Here's a working example:
...
- 411
6
votes
Possible root cause(s) of the misunderstanding that DTT implies not Turing complete?
Is this perhaps a problem with 'common understanding' regarding what it means to be Turing complete?
Indeed it is: a pop-science understanding of dependent types has led to this myth being deeply ...
- 1,266
6
votes
Universe inconsistency as an effect
I don't have an answer, but I would like to provide some buzzwords and references that will make it easier to find relevant literature.
Some background information
Computational effects and dependent ...
- 9,812
6
votes
Strictly-monotone "max" operation for constructive Brouwer-trees?
You can define a max that will be better behaved by induction on x and y. Something like:
<...
- 982
5
votes
Accepted
How to provide proof for termination in Agda?
There are three possible approaches:
Use a different algorithm, like division in stdlib, see div-helper.
Use the well-founded induction library. There are many ...
- 6,316
5
votes
How to prove the termination of Ackermann in Lean?
Usually x-1 is harder to work with (but not impossible). Pattern matching is much easier from a type theoretic perspective. So (this is actually one of the test ...
- 4,025
5
votes
Accepted
proof of termination for zip in Lean
It seems you are trying to use Simultaneous Matching on the two lists as and bs but messed up the syntax, and instead are ...
- 5,530
4
votes
Accepted
How to convince Agda that definition is terminating in the presence of unapplied recursion?
I can think of two ways of solving the problem.
First, make All and Value mutually recursive so that you don't have to pass <...
- 9,812
4
votes
Defining a terminating `ripple`, with arguments swapping places
Idris is also happy with this definition:
...
- 1,266
4
votes
Can strict propositions (Rocq's SProp, Agda's Prop) be used to show termination?
It's consistent to interpret the type of strict propositions as the type of double negation stable propositions (or more generally as $j$-stable propositions for any given Lawvere-Tierney topology $j$)...
- 301
4
votes
Can strict propositions (Rocq's SProp, Agda's Prop) be used to show termination?
Sadly, a big issue of strict propositions is that in their current form they validate very little choice principles.
For instance, I don't think that your example is provable. Indeed, Pujet and ...
- 5,530
4
votes
How to prove the termination of Ackermann in Lean?
With dependent types and the awesome prelude of Lean 4, one can define the Ackermann function in any equivalent way as long as the definition is constructive. However, the more closely the definition ...
- 155
3
votes
Defining a terminating `ripple`, with arguments swapping places
In Lean 4, this is done using well-founded recursion by specifying a termination measure:
...
3
votes
proof of termination for zip in Lean
The answer by Meven Lennon-Bertrand is exactly right, but the best way to ensure you are doing structural recursion is to avoid writing the match statement in the first place:
...
- 9,195
3
votes
Accepted
How does one show termination of a function that is structurally recursive over a type T with subterms of type List T?
For reference, in Coq, termination checking “just works” on this function:
...
- 1,053
3
votes
How does one show termination of a function that is structurally recursive over a type T with subterms of type List T?
The part of Lean that tries to determine whether recursion is well-founded does not look inside definitions (it's dangerous to do so when one is dealing with recursive definitions). You can solve the ...
- 9,812
2
votes
How to prove the termination of Ackermann in Lean?
Here's a variant that doesn't require termination_by:
...
2
votes
Accepted
Using `decreasing_by` to prove termination in Lean 4
You can follow the examples in TPIL4 Chapter 8. (Edit: This answer is for the new syntax, which changed in Lean 4.6. See the 4.6 release notes for a comparison with the former syntax.) In particular:...
- 9,195
2
votes
Defining a terminating `ripple`, with arguments swapping places
HOL4's automatic search for a well-founded termination relation succeeds in this case, so you need only write:
...
- 1,112
2
votes
Defining a terminating `ripple`, with arguments swapping places
In Coq, using Equations, the program is pretty much as simple as in Agda:
...
- 5,530
1
vote
Well founded recursion through lists
Well, this kind of blew up, but at least I feel there's still decent modularity. I kind of brute-forced my way through the multi-motive JSON.rec -- if there are ...
- 273
Only top scored, non community-wiki answers of a minimum length are eligible