Questions tagged [termination]
The termination tag has no usage guidance.
9
questions
4
votes
4
answers
750
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 ...
- 758
3
votes
2
answers
622
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 ...
- 197
6
votes
2
answers
139
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
3
votes
3
answers
346
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
...
- 131
10
votes
1
answer
218
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 ...
- 2,912
8
votes
1
answer
199
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 (...
- 5,877
0
votes
1
answer
92
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
184
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
162
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.
...
- 773