[Agda] Termination in algebraic encodings of families

Nils Anders Danielsson nad at cse.gu.se
Wed Jan 13 10:05:05 CET 2021


On 2021-01-08 02:26, John Paul Martin wrote:
>     {-# TERMINATING #-}
>     BST-alg : ℕ → ℕ → Tree → Set
>     BST-alg n m t = (t ≡ leaf)
>                    ∨ ( ∃[ x ] ∃[ l ] ∃[ r ] (t ≡ (node l x r) × (x ≤ m) × (n ≤ x) × (BST-alg n x l) × (BST-alg x m r)))

> Does this family(BST-alg) actually terminate?

No. Try normalising BST-alg in Agda.

-- 
/NAD


More information about the Agda mailing list