[racket] Redex: exponential runtime with certain judgments

From: Daniel Feltey (dfeltey at ccs.neu.edu)
Date: Fri Jul 25 00:53:38 EDT 2014

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

Posted on the users mailing list.