[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