<div dir="ltr"><div>Hello All!</div><div><br></div><div>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. </div><div><br></div><div>I'm encoding a certain version of the Search Property for binary trees. As an inductive family this is: <br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div><br>data Tree : Set where<br>  leaf : Tree<br>  node : Tree → ℕ → Tree → Tree<br><br>data BST : ℕ → ℕ → Tree → Set where<br>  leaf-bst : ∀ {n m}<br>           → BST n m leaf<br>  node-bst : ∀ {n m x l r}<br>           → BST n x l<br>           → BST x m r<br>           → x ≤ m<br>           → n ≤ x<br>           → BST n m (node l x r)<br></div></blockquote><div><br></div><div>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. <br></div><div><br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div>{-# TERMINATING #-}<br>BST-alg : ℕ → ℕ → Tree → Set<br>BST-alg n m t = (t ≡ leaf)<br>              ∨ ( ∃[ x ] ∃[ l ] ∃[ r ] (t ≡ (node l x r) × (x ≤ m) × (n ≤ x) × (BST-alg n x l) × (BST-alg x m r)))<br><br>-- proof that BST-alg terminates<br>BST-alg-t : ℕ → ℕ → Tree → Set<br>BST-alg-t n m leaf = ⊤<br>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)<br><br></div></blockquote><div><br></div><div>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?</div><div><br></div><div>Thanks!</div><div><br></div><div>Jack Martin</div><div>PhD Student - Programming Languages and Verification Laboratory - University of Colorado at Boulder<br></div></div>