[Agda] Termination in algebraic encodings of families

[John Paul Martin]

Hello All!

I'm playing around with different ways of encoding type families and hit on
an interesting little error(/feature?). Sorry in advance, I'm sure this has
been discussed before.

I'm encoding a certain version of the Search Property for binary trees. As
an inductive family this is:

>
> data Tree : Set where
>   leaf : Tree
>   node : Tree → ℕ → Tree → Tree
>
> data BST : ℕ → ℕ → Tree → Set where
>   leaf-bst : ∀ {n m}
>            → BST n m leaf
>   node-bst : ∀ {n m x l r}
>            → BST n x l
>            → BST x m r
>            → x ≤ m
>            → n ≤ x
>            → BST n m (node l x r)
>

But, for personal reasons 😉,  I'd like to encode this as a single-line
algebraic type. This is BST-alg below. The multi-clause/recursive version
is also included.

{-# 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)))
>
> -- proof that BST-alg terminates
> BST-alg-t : ℕ → ℕ → Tree → Set
> BST-alg-t n m leaf = ⊤
> BST-alg-t n m (node l x r) = (x ≤ m) × (n ≤ x) × (BST-alg-t n x l) ×
> (BST-alg-t x m r)
>
>
The termination checker is obviously unable to tell that I've lifted the
recursive case matching as propositional equalities. Thus the need for the
terminating flag. My question: Does this family(BST-alg) actually
terminate? Is it really any different than either of the other definitions?

Thanks!

Jack Martin
PhD Student - Programming Languages and Verification Laboratory -
University of Colorado at Boulder
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20210107/a007935b/attachment.html>