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" <ro...@eecs.northwestern.edu> To: "Daniel Feltey" <dfel...@ccs.neu.edu> Cc: "Racket Users" <users@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 <dfel...@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
bad-redex.rkt
Description: Binary data
____________________ Racket Users list: http://lists.racket-lang.org/users
