Skip to main content
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 ...
Jesper's user avatar
  • 506
7 votes

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 ...
Andrej Bauer's user avatar
  • 9,593
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 ...
Andrej Bauer's user avatar
  • 9,593
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: <...
Dan Doel's user avatar
  • 982
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: ...
Jozef Mikušinec's user avatar
5 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 ...
gallais's user avatar
  • 1,256
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 ...
ice1000's user avatar
  • 6,276
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 ...
Trebor's user avatar
  • 4,015
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 ...
Meven Lennon-Bertrand's user avatar
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 <...
Andrej Bauer's user avatar
  • 9,593
4 votes

Defining a terminating `ripple`, with arguments swapping places

Idris is also happy with this definition: ...
gallais's user avatar
  • 1,256
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$)...
aws's user avatar
  • 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 ...
Meven Lennon-Bertrand's user avatar
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 ...
Simon Eatwell's user avatar
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: ...
David Thrane Christiansen's user avatar
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: ...
Jason Rute's user avatar
  • 8,960
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: ...
James Wood's user avatar
  • 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 ...
Andrej Bauer's user avatar
  • 9,593
2 votes

How to prove the termination of Ackermann in Lean?

Here's a variant that doesn't require termination_by: ...
François G. Dorais's user avatar
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:...
Jason Rute's user avatar
  • 8,960
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: ...
Michael Norrish's user avatar
2 votes

Defining a terminating `ripple`, with arguments swapping places

In Coq, using Equations, the program is pretty much as simple as in Agda: ...
Meven Lennon-Bertrand's user avatar
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 ...
Felipe's user avatar
  • 273

Only top scored, non community-wiki answers of a minimum length are eligible