Questions tagged [termination]

The tag has no usage guidance.

Filter by
Sorted by
Tagged with
4 votes
4 answers

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 ...
James Wood's user avatar
3 votes
2 answers

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 ...
Nate Glenn's user avatar
6 votes
2 answers

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,...
mobotsar's user avatar
  • 135
3 votes
3 answers

How to prove the termination of Ackermann in Lean?

I'm trying to write the Ackermann function and prove it terminates in Lean 4 ...
Mikaël Mayer's user avatar
10 votes
1 answer

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 ...
Mike Shulman's user avatar
  • 2,912
8 votes
1 answer

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 (...
ice1000's user avatar
  • 5,877
0 votes
1 answer

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: ...
Felipe's user avatar
  • 273
5 votes
1 answer

How to convince Agda that definition is terminating in the presence of unapplied recursion?

In the following, termination check fails for Df: ...
TerminationCheckFailed's user avatar
5 votes
1 answer

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. ...
Joey Eremondi's user avatar