[Agda] non-constructor indices

[James Chapman]

Hi,

On 15 Jan 2008, at 22:42, Patrik Jansson wrote:
> As to your problem with the termination checker, it cannot see  
> termination because the recursive call is "hidden by" / wrapped by  
> subst.  It would be interesting to investigate if the checker could  
> be told to "inline" definitions like that of subst.


In my limited experience it is best to avoid subst (and, to an extent,  
its friend resp) at all costs. It doesn't scale at all well to  
complicated situations.

Agda has a great feature for dealing with equations on the right-hand  
side of a function definition: the with rule. It allows you to pattern  
match on intermediate results and rewrite by equations:

Your

-- termination problems:
height : Indexed Z -> Nat
height B = Z
height (I {n} {m} p1 p2 id) = height (subst Indexed (invert-plus-z-2  
{n} {m} id) p2)

can be rewritten as

-- termination checker seems happy:
height : Indexed Z -> Nat
height B = Z
height (I {n} {m} p1 p2 id) with m | invert-plus-z-2 {n} {m} id
... | .Z | Refl = height p2

See Ulf's thesis for info on the with rule:

http://www.cs.chalmers.se/~ulfn/papers/thesis.pdf

Actually it's really the 'magic' with rule, which is even more clever  
but that is another story and one better told by some other than me.

Cheers,

James


This message has been checked for viruses but the contents of an attachment
may still contain software viruses, which could damage your computer system:
you are advised to perform your own checks. Email communications with the
University of Nottingham may be monitored as permitted by UK legislation.