[Agda] a termination problem

[Andreas Abel]

Hi Ramana,

would it be possible that you send me your agda file (including 
Name.agda which it relies on).  That would make my job easier than 
getting it from hpaste, fixing the problems due to absence of module 
Name, etc.

Cheers,
Andreas

On 11/30/11 12:31 PM, Ramana Kumar wrote:
> I found your MiniAgda paper, and some slides... I had a skim, and
> might read in more detail later...
> It seems like sizes would have to appear on a lot of stuff in the
> standard library for them to really be useful?
>
> I've put my next termination problem here http://hpaste.org/54700.
> Can you see a way to use sized types to do this?
> I will try myself, but I'm less sure about what's going on.
>
> I look forward to your reply :)
>
> On Wed, Nov 30, 2011 at 10:31 AM, Ramana Kumar<rk436 at cam.ac.uk>  wrote:
>> Wow, I would never have found that myself, thanks :)
>> Is there any information or papers on sized types I could look at? (Or
>> do you want to give a brief description here?)
>>
>> I have further similar termination problems later on in my
>> development... I'll see if the same trick works! If not, maybe there
>> is work on improving sized types support I could do?
>>
>> On Wed, Nov 30, 2011 at 12:18 AM, Andreas Abel<andreas.abel at ifi.lmu.de>  wrote:
>>> Hello Ramana,
>>>
>>> On 29.11.11 11:38 PM, Ramana Kumar wrote:
>>>>
>>>> Apart from the feeling that "there must be a better way", I also have
>>>> a real problem to do with termination.
>>>> In particular, I define a recursive function that passes itself to
>>>> Relation.Binary.List.StrictLex.transitive.
>>>> How can I convince Agda that transitive will only apply it to smaller
>>>> arguments, or how can I avoid having to try?
>>>
>>> This is the typical situation where you would use sized types for
>>> termination checking.  Unfortunately, the support for sized types is
>>> rudimentary in Agda at the moment.
>>>
>>> However, your example works!  I attach a version of your agda code with a
>>> sized definition of data type _<_.  [I removed Name since it was not
>>> available to me, but this is inessential.]
>>>
>>> Cheers,
>>> Andreas
>>>
>>> --
>>> 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/
>>>
>>
>

-- 
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/