πŸ“₯ Download raw
{-# OPTIONS --cubical-compatible #-}
module Padova2025.ProvingBasics.Termination.BoveCapretta.Fun91 where

The 91 function

open import Padova2025.ProgrammingBasics.Naturals.Base
open import Padova2025.ProgrammingBasics.Naturals.Arithmetic
open import Padova2025.ProgrammingBasics.Lists
open import Padova2025.ProvingBasics.Equality.Base
open import Padova2025.ProvingBasics.Termination.Ordering
open import Padova2025.ProvingBasics.Termination.Gas
open import Padova2025.ProvingBasics.Connectives.Disjunction
open import Padova2025.ProvingBasics.Connectives.More

{-# BUILTIN NATURAL β„• #-}

Let us follow tradition and study the celebrated 91 function:

f : β„• β†’ β„•
f x with ≀-<-connex x 20
... | left  x≀20 = f (f (x + 11))
... | right x>20 = x ∸ 10
-- In the original, it is `100` instead of `20`.
-- We use the smaller value here to reduce load on the Let's play Agda server.

Because of the nested recursion, this definition presents a challenge to termination analysis. This function is total, but this fact is not obvious to Agda’s termination checkerβ€”Agda rejects this definition with the comment β€œTermination checking failed”.

Representing the function

To represent this function in Agda, we follow the same approach as in the previous module.

data Def : β„• β†’ Set
fβ‚€ : (n : β„•) β†’ Def n β†’ β„•

data Def where
  gt20 : {n : β„•} β†’ n > 20 β†’ Def n
  le20 : {n : β„•} β†’ n ≀ 20 β†’ (p : Def (n + 11)) β†’ Def (fβ‚€ (n + 11) p) β†’ Def n

fβ‚€ n (gt20 _)     = n ∸ 10
fβ‚€ n (le20 x p q) = fβ‚€ (fβ‚€ (n + 11) p) q

Verifying totality

Clever ways have been proposed to prove the 91 function to be total. Here we want to showcase a β€œbrute force” method. For the inputs 0 to 20 for which termination is not obvious, we blithely run the recursion (with a gas limit in place) to observe, without any actual insight to the function’s behavior, that the recursion terminates.

observe-termination : (gas : β„•) (n : β„•) β†’ Maybe (Def n)
observe-termination zero n = nothing
observe-termination (succ gas) n with ≀-<-connex n 20
... | right n>20 = just (gt20 n>20)
... | left n≀20  = do
  p ← observe-termination gas (n + 11)
  q ← observe-termination gas (fβ‚€ (n + 11) p)
  just (le20 n≀20 p q)

collect : {P : β„• β†’ Set} β†’ ((n : β„•) β†’ Maybe (P n)) β†’ (n : β„•) β†’ Maybe (All P (downFrom n))
collect = {!!}

empirical-fact : All Def (downFrom 21)
empirical-fact = from-just {!!}

With the difficult cases dealt with empirically, we are now in a position to verify totality.

total : (n : β„•) β†’ Def n
total n with ≀-<-connex n 20
... | left  n≀20 = {!!}
... | right n>20 = {!!}

With the totality proof in place, we can also define a manifestly total version of the 91 function.

f : β„• β†’ β„•
f n = fβ‚€ n (total n)

Determining the function values

It turns out that the 91 function has the same values as the following non-recursively defined function.

g : β„• β†’ β„•
g x = max 21 x ∸ 10

We want to prove agreement by using the brute force approach again.

observe-equality : (n : β„•) β†’ Maybe (f n ≑ g n)
observe-equality n with <-cmp (f n) (g n)
... | left  fn≑gn = just fn≑gn
... | right _     = nothing

empirical-fact' : All (Ξ» (n : β„•) β†’ f n ≑ g n) (downFrom 21)
empirical-fact' = from-just {!!}

fβ‰—g : (n : β„•) β†’ n ≀ 20 β†’ f n ≑ g n
fβ‰—g n n≀20 = lookup empirical-fact' (succ-monotone n≀20)