[racket] Redex: exponential runtime with certain judgments

I'm attaching a model of the simply typed lambda calculus which demonstrates the issue. The file includes a language definition, the necessary judgment forms, and a few macros for generating and timing programs of a given size.

I hope this helps.
Thanks
Dan 



----- Original Message -----
From: "Robby Findler" <robby at eecs.northwestern.edu>
To: "Daniel Feltey" <dfeltey at ccs.neu.edu>
Cc: "Racket Users" <users at racket-lang.org>
Sent: Friday, July 25, 2014 1:16:10 AM GMT -05:00 US/Canada Eastern
Subject: Re: [racket] Redex: exponential runtime with certain judgments

It's hard for me to see what exactly is going on -- would you have the
time to make a simple form of your judgment form and an input that
demonstrates the issue?

Thanks,
Robby

On Thu, Jul 24, 2014 at 11:53 PM, Daniel Feltey <dfeltey at ccs.neu.edu> wrote:
> I've been implementing a type system with subtyping using Redex's judgment forms and noticed that checking whether my typing judgment would hold was taking longer than seemed reasonable (5 - 10 minutes in some cases).
>
> Ultimately I tracked the bug down to a clause in the subtyping judgment that had the form:
>
> (< tau tau)
>
> Where tau is the grammar term that could represent any type in my language, and both uses of tau are in input positions. Removing this rule brought down the 10 minute runtime mentioned above to under half a second.
>
> Is this behavior expected in the case of judgment-form clauses similar to the above, it seemed natural to me to include a rule like this in my subtyping judgment and I definitely didn't expect this to be the main reason for my model performing so poorly.
>
> Thanks
> Dan
> ____________________
>   Racket Users list:
>   http://lists.racket-lang.org/users
-------------- next part --------------
A non-text attachment was scrubbed...
Name: bad-redex.rkt
Type: application/octet-stream
Size: 4191 bytes
Desc: not available
URL: <http://lists.racket-lang.org/users/archive/attachments/20140725/6f1ba5c3/attachment-0001.obj>