Skip to main content

Questions tagged [termination]

The tag has no usage guidance.

Filter by
Sorted by
Tagged with
3 votes
1 answer

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 ...
Jozef Mikušinec's user avatar
6 votes
2 answers

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 ...
Municipal-Chinook-7's user avatar
9 votes
2 answers

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-...
Ingo Blechschmidt's user avatar
3 votes
1 answer

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): ...
tinlyx's user avatar
  • 2,220
2 votes
1 answer

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 ...
Matematiflo's user avatar
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
  • 1,053
4 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
4 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
  • 3,200
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
  • 6,306
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