Databases
StackOverflow2013
Postsdbo
PO
 

Note that there are some explanatory texts on larger screens.

plurals
  1. PO
    primarykey
    data
    text
    <p>Agda's termination checker only checks for structural recursion (i.e. calls that happen on structurally smaller arguments) and there's no way to establish that certain relation (such as <code>_&lt;_</code>) implies that one of the arguments is structurally smaller.</p> <hr> <p>Digression: Similar problem happens with positivity checker. Consider the standard fix-point data type:</p> <pre><code>data μ_ (F : Set → Set) : Set where fix : F (μ F) → μ F </code></pre> <p>Agda rejects this because <code>F</code> may not be positive in its first argument. But we cannot restrict <code>μ</code> to only take positive type functions, or show that some particular type function is positive.</p> <hr> <p>How do we normally show that a recursive functions terminates? For natural numbers, this is the fact that if the recursive call happens on strictly smaller number, we eventually have to reach zero and the recursion stops; for lists the same holds for its length; for sets we could use the strict subset relation; and so on. Notice that "strictly smaller number" doesn't work for integers.</p> <p>The property that all these relations share is called well-foundedness. Informally speaking, a relation is well-founded if it doesn't have any infinite descending chains. For example, <code>&lt;</code> on natural numbers is well founded, because for any number <code>n</code>:</p> <pre><code>n &gt; n - 1 &gt; ... &gt; 2 &gt; 1 &gt; 0 </code></pre> <p>That is, the length of such chain is limited by <code>n + 1</code>.</p> <p><code>≤</code> on natural numbers, however, is not well-founded:</p> <pre><code>n ≥ n ≥ ... ≥ n ≥ ... </code></pre> <p>And neither is <code>&lt;</code> on integers:</p> <pre><code>n &gt; n - 1 &gt; ... &gt; 1 &gt; 0 &gt; -1 &gt; ... </code></pre> <hr> <p>Does this help us? It turns out we can encode what it means for a relation to be well-founded in Agda and then use it to implement your function.</p> <p>For simplicity, I'm going to bake the <code>_&lt;_</code> relation into the data type. First of all, we must define what it means for a number to be accessible: <code>n</code> is accessible if all <code>m</code> such that <code>m &lt; n</code> are also accessible. This of course stops at <code>n = 0</code>, because there are no <code>m</code> so that <code>m &lt; 0</code> and this statement holds trivially.</p> <pre><code>data Acc (n : ℕ) : Set where acc : (∀ m → m &lt; n → Acc m) → Acc n </code></pre> <p>Now, if we can show that all natural numbers are accessible, then we showed that <code>&lt;</code> is well-founded. Why is that so? There must be a finite number of the <code>acc</code> constructors (i.e. no infinite descending chain) because Agda won't let us write infinite recursion. Now, it might seem as if we just pushed the problem back one step further, but writing the well-foundedness proof is actually structurally recursive!</p> <p>So, with that in mind, here's the definition of <code>&lt;</code> being well-founded:</p> <pre><code>WF : Set WF = ∀ n → Acc n </code></pre> <p>And the well-foundedness proof:</p> <pre><code>&lt;-wf : WF &lt;-wf n = acc (go n) where go : ∀ n m → m &lt; n → Acc m go zero m () go (suc n) zero _ = acc λ _ () go (suc n) (suc m) (s≤s m&lt;n) = acc λ o o&lt;sm → go n o (trans o&lt;sm m&lt;n) </code></pre> <p>Notice that <code>go</code> is nicely structurally recursive. <code>trans</code> can be imported like this:</p> <pre><code>open import <a href="http://vituscze.github.io/agda-stdlib-html/Data.Nat.html">Data.Nat</a> open import <a href="http://vituscze.github.io/agda-stdlib-html/Relation.Binary.html">Relation.Binary</a> open <a href="http://vituscze.github.io/agda-stdlib-html/Relation.Binary.html#7697">DecTotalOrder</a> <a href="http://vituscze.github.io/agda-stdlib-html/Data.Nat.html#4558">decTotalOrder</a> using (trans) </code></pre> <p>Next, we need a proof that <code>⌊ n /2⌋ ≤ n</code>:</p> <pre><code>/2-less : ∀ n → ⌊ n /2⌋ ≤ n /2-less zero = z≤n /2-less (suc zero) = z≤n /2-less (suc (suc n)) = s≤s (trans (/2-less n) (right _)) where right : ∀ n → n ≤ suc n right zero = z≤n right (suc n) = s≤s (right n) </code></pre> <p>And finally, we can write your <code>f</code> function. Notice how it suddenly becomes structurally recursive thanks to <code>Acc</code>: the recursive calls happen on arguments with one <code>acc</code> constructor peeled off.</p> <pre><code>f : ℕ → ℕ f n = go _ (&lt;-wf n) where go : ∀ n → Acc n → ℕ go zero _ = 0 go (suc n) (acc a) = go ⌊ n /2⌋ (a _ (s≤s (/2-less _))) </code></pre> <hr> <p>Now, having to work directly with <code>Acc</code> isn't very nice. And that's where Dominique's answer comes in. All this stuff I've written here has already been done in the standard library. It is more general (the <code>Acc</code> data type is actually parametrized over the relation) and it allows you to just use <code>&lt;-rec</code> without having to worry about <code>Acc</code>.</p> <hr> <p>Taking a more closer look, we are actually pretty close to the generic solution. Let's see what we get when we parametrize over the relation. For simplicity I'm not dealing with universe polymorphism.</p> <p>A relation on <code>A</code> is just a function taking two <code>A</code>s and returning <code>Set</code> (we could call it binary predicate):</p> <pre><code>Rel : Set → Set₁ Rel A = A → A → Set </code></pre> <p>We can easily generalize <code>Acc</code> by changing the hardcoded <code>_&lt;_ : ℕ → ℕ → Set</code> to an arbitrary relation over some type <code>A</code>:</p> <pre><code>data Acc {A} (_&lt;_ : Rel A) (x : A) : Set where acc : (∀ y → y &lt; x → Acc _&lt;_ y) → Acc _&lt;_ x </code></pre> <p>The definition of well-foundedness changes accordingly:</p> <pre><code>WellFounded : ∀ {A} → Rel A → Set WellFounded _&lt;_ = ∀ x → Acc _&lt;_ x </code></pre> <p>Now, since <code>Acc</code> is an inductive data type like any other, we should be able to write its eliminator. For inductive types, this is a fold (much like <code>foldr</code> is eliminator for lists) - we tell the eliminator what to do with each constructor case and the eliminator applies this to the whole structure.</p> <p>In this case, we'll do just fine with the simple variant:</p> <pre><code>foldAccSimple : ∀ {A} {_&lt;_ : Rel A} {R : Set} → (∀ x → (∀ y → y &lt; x → R) → R) → ∀ z → Acc _&lt;_ z → R foldAccSimple {R = R} acc′ = go where go : ∀ z → Acc _ z → R go z (acc a) = acc′ z λ y y&lt;z → go y (a y y&lt;z) </code></pre> <p>If we know that <code>_&lt;_</code> is well-founded, we can skip the <code>Acc _&lt;_ z</code> argument completly, so let's write small convenience wrapper:</p> <pre><code>recSimple : ∀ {A} {_&lt;_ : Rel A} → WellFounded _&lt;_ → {R : Set} → (∀ x → (∀ y → y &lt; x → R) → R) → A → R recSimple wf acc′ z = foldAccSimple acc′ z (wf z) </code></pre> <p>And finally:</p> <pre><code>&lt;-wf : WellFounded _&lt;_ &lt;-wf = {- same definition -} &lt;-rec = recSimple &lt;-wf f : ℕ → ℕ f = &lt;-rec go where go : ∀ n → (∀ m → m &lt; n → ℕ) → ℕ go zero _ = 0 go (suc n) r = r ⌊ n /2⌋ (s≤s (/2-less _)) </code></pre> <p>And indeed, this looks (and works) almost like the one in the standard library!</p> <hr> <p>Here's the fully dependent version in case you are wondering:</p> <pre><code>foldAcc : ∀ {A} {_&lt;_ : Rel A} (P : A → Set) → (∀ x → (∀ y → y &lt; x → P y) → P x) → ∀ z → Acc _&lt;_ z → P z foldAcc P acc′ = go where go : ∀ z → Acc _ z → P z go _ (acc a) = acc′ _ λ _ y&lt;z → go _ (a _ y&lt;z) rec : ∀ {A} {_&lt;_ : Rel A} → WellFounded _&lt;_ → (P : A → Set) → (∀ x → (∀ y → y &lt; x → P y) → P x) → ∀ z → P z rec wf P acc′ z = foldAcc P acc′ _ (wf z) </code></pre>
    singulars
    1. This table or related slice is empty.
    1. POAssisting Agda's termination checker
      singulars
      1. PTQuestion
    1. PTAnswer
    1. USVitus
    1. USVitus
    plurals
    1. This table or related slice is empty.
    1. This table or related slice is empty.
    1. POAssisting Agda's termination checker
      singulars
      1. PTQuestion
    1. This table or related slice is empty.
    1. VO
      singulars
      1. PO
      1. This table or related slice is empty.
      1. VTUpMod
    2. VO
      singulars
      1. PO
      1. This table or related slice is empty.
      1. VTAcceptedByOriginator
    3. VO
      singulars
      1. PO
      1. This table or related slice is empty.
      1. VTUpMod
    1. COIs there any reason why "go" would typecheck, with the exact same type as you have, but <-rec go would fail to typecheck?
      singulars
      1. PO
      1. USJonathan Gallagher
    2. CO@JonathanGallagher: Which `go` do you mean?
      singulars
      1. PO
      1. USVitus
    3. COgo : ∀ n → (∀ m → m < n → ℕ) → ℕ
      singulars
      1. PO
      1. USJonathan Gallagher
 

Querying!

 
Guidance
A row detail

Detail views are divided into sections. All the information in the data section comes from columns in the selected row. The other sections display data from other, related rows.

Related data can be related in a to-one or a to-many fashion. Captions of data related in a to-many fashion link to a list view showing a filtered view of the table.

Try moving around until you find a non-empty to-many entry and click on the label to get to one. You can move back to the root by clicking on the database name in the header.

SQuiL has stopped working due to an internal error.

If you are curious you may find further information in the browser console, which is accessible through the devtools (F12).

Reload