[Agda] a termination problem

Ramana Kumar rk436 at cam.ac.uk
Wed Nov 30 15:19:34 CET 2011


I put the Name module on hpaste too originally here http://hpaste.org/54676

if you would still prefer agda files let me know.... but I'm currently
in the middle of editing so I'd need to make them usable again first

I'm experimenting with making Type sized and not just _<_ ... but I'm
not sure if you can compare/enforce sizes attached to different
types... but I think the termination argument for <-cmp would consider
sizes on Type and not on _<_.

On Wed, Nov 30, 2011 at 2:16 PM, Andreas Abel <andreas.abel at ifi.lmu.de> wrote:
> 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/
>


More information about the Agda mailing list