Questions tagged [termination]
The termination tag has no usage guidance.
14
questions
3
votes
1
answer
161
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 ...
- 411
6
votes
2
answers
426
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 ...
9
votes
2
answers
173
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-...
3
votes
1
answer
391
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,210
2
votes
1
answer
297
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
4
votes
4
answers
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
4
votes
2
answers
721
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
6
votes
2
answers
238
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
4
votes
3
answers
513
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
10
votes
1
answer
248
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,190
8
votes
1
answer
240
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
0
votes
1
answer
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
5
votes
1
answer
229
views
How to convince Agda that definition is terminating in the presence of unapplied recursion?
In the following, termination check fails for Df:
...
5
votes
1
answer
177
views
Strictly-monotone "max" operation for constructive Brouwer-trees?
The Setting
I'm trying to use Agda's well-founded ordering to prove that something is terminating using Brouwer Trees i.e.
...
- 921