# Questions tagged [termination]

The tag has no usage guidance.

14 questions
Filter by
Sorted by
Tagged with
165 views

### How to prove termination of mutually recursive functions if only some decrease their arguments?

I need to prove termination of mutually recursive functions. However, only some of those functions actually (structurally) decrease their arguments, other functions do some other calculations and pass ...
434 views

### Possible root cause(s) of the misunderstanding that DTT implies not Turing complete?

I myself have fallen prey to this misconception, i.e., that being dependently typed as in Agda, Coq, etc., implies not being Turing complete, which can be (whether now or previously) found at quite a ...
175 views

### Can strict propositions (Rocq's SProp, Agda's Prop) be used to show termination?

I got the impression that there is quite a bit of justified hype around the new(ish) strict propositions as proposed by Gilbert, Cockx, Sozeau and Tabareau in their paper Definitional Proof-...
393 views

### How to provide proof for termination in Agda?

I am trying to write an integer division function from scratch in agda2 (as of 2.6.3): ...
• 2,220
316 views

### Using decreasing_by to prove termination in Lean 4

Warning: This was written for Lean v4.5.0. To make the accepted answer work, please use v4.6.0-rc1. I would like to define an elementary quicksort function for ...
• 167
768 views

### Defining a terminating ripple, with arguments swapping places

In Agda, I can make the following definition, and Agda believes that the recursion terminates. Notice that the arguments “swap places” in the recursive call, so neither of the arguments individually ...
• 1,053
724 views

### proof of termination for zip in Lean

I'm making my way through Functional Programming in Lean and there's an exercise to implement zip, which takes two lists and returns a list of tuples the length of ...
• 237
242 views

### How does one show termination of a function that is structurally recursive over a type T with subterms of type List T?

I've been having a bit of difficulty proving termination of a particular kind of function. I'm quite new to using Lean, so it's possible that what I'm missing is a language feature and not a technique,...
• 135
517 views

### How to prove the termination of Ackermann in Lean?

I'm trying to write the Ackermann function and prove it terminates in Lean 4 ...
• 141
249 views

### Universe inconsistency as an effect

The Internet tells me there is some work on languages that permit general recursion but carry information about possible divergence in the type system. For instance, the simply-typed language Koka ...
• 3,200
241 views

### Termination and confluence -- which goes first?

I'm implementing a version of cubical type theory where the well-definedness of pattern matching functions is implied by: the well-typedness of the clauses (type check) the coverage of the patterns (...
• 6,306
98 views

### Well founded recursion through lists

I'm trying out Lean for programming, and I'm struggling with the termination checker. Here's the toy I'm playing with: ...
• 273