[Agda] Coinductive families

[Andreas Abel]

Actually, the record match in append is not translated away, since it  
cannot be replaced by projections.

Still, I modified the termination checker to not count a record  
constructor as increase in the structural ordering.
Otherwise, it seems like the termination checker is a bit too context  
sensitive.  It then relies completely on the record pattern translation.

Clearly this has to be rejected:

postulate
   lie : {b : Bool} -> T b

f : forall {A} -> List A -> Empty
f (list b h t) = f (t lie)

Since no constructor match is blocking this pattern, it is translated  
away

f l = f (tl l lie)

and that certainly loops.

However it feels funny to accept

f (list true h t) = f (t lie)

The record pattern is not translated away this time.  And I think it  
would not be a problem to allow this definition.  But it feels too  
context-sensitive.

What do you think?

Andreas

On Oct 5, 2010, at 1:42 PM, Dan Doel wrote:
> On Tuesday 05 October 2010 6:35:50 am Thorsten Altenkirch wrote:
>
>> Btw, when trying to define append
>>
>> append : ∀ {A} → List A → List A → List A
>> append (list true h t) bs = list true h (λ _ → append (t _) bs)
>> append (list false _ _) bs = bs
>>
>> the termination checker complains. I am not sure why, since (t _) is
>> smaller than (list true h t), isn't it?
>
> This theoretically rewrites to something like:
>
>  append l bs with isCons l | hd l | tl l
>  ... | true  | h | t = list true h (\_ -> append (t _) bs)
>  ... | false | _ | _ = bs
>
> and with the projection rule:
>
>  t = tl l <= l
>
> so, no; it is merely not-bigger (or, possibly, actually bigger if  
> your version
> is old enough; not sure). This is the same rule used to disqualify:
>
>  record R : Set where
>    constructor c
>    field
>      p : R
>
>  foo : R -> R
>  foo (c r) = foo r
>
> which *actually* translates internally to:
>
>  foo : R -> R
>  foo r = foo (p r)
>
> which won't normalize. append can't be translated, I think, because  
> the match
> on isCons blocks translation to projections (the translation I gave is
> probably a bit much to expect of the checker), but Andreas changed  
> the rule
> for pattern matching on record constructors to make the two  
> consistent, I
> think.
>
> -- Dan
>

Andreas Abel  <><      Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY

andreas.abel at ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/