[racket] Redex: exponential runtime with certain judgments

Oh, PS: you can use unquote inside 'term' (or anywhere where you are
writing Redex terms), eg:

  (time (judgment-holds (J ,(build-list 14 add1))))

Robby

On Fri, Jul 25, 2014 at 6:42 PM, Robby Findler
<robby at eecs.northwestern.edu> wrote:
> I've pushed a fix for the specific issue in this program but, in
> general, there is a problem here that Redex can't solve on it's own.
>
> The issue is that the judgment-form you have has more than one way to
> establish the same fact and that ambiguity can have exponential
> blowup.
>
> Here's a simple example of the issue in a case where Redex is still
> going to be slow.
>
> #lang racket
> (require redex)
>
> (define-language L)
>
> (define-judgment-form L
>   #:mode (K I)
>   [(K (any_2 ...))
>    -------------- one
>    (K (natural_1 any_2 ...))]
>   [(K (any_2 ...))
>    -------------- two
>    (K (number_1 any_2 ...))])
>
> (time (judgment-holds (K (0 1 2 3 4 5 6 7 8 9 10 11 12 13 14))))
> (time (judgment-holds (K (0 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15))))
>
> In this case, each smaller list has two options and so we get roughly
> 2^14 or 2^15 different ways to (fail to) make this derivation, and
> they take a while to go thru.
>
> This next example is closer to how your code actually does the
> multiple derivations -- it actually builds them inside an ellipsis and
> in a way that Redex has a chance to notice that it's got the same
> result twice:
>
> ;; this one exists to have an ellipsis
> (define-judgment-form L
>   #:mode (J I)
>   [(D any_x) ...
>    --------------
>    (J (any_x ...))])
>
> ;; this one exists to have redundancy
> (define-judgment-form L
>   #:mode (D I)
>   [----------- nat
>    (D natural)]
>   [----------- num
>    (D number)])
>
> (time (judgment-holds (J (0 1 2 3 4 5 6 7 8 9 10 11 12 13))))
> (time (judgment-holds (J (0 1 2 3 4 5 6 7 8 9 10 11 12 13 14))))
>
> I've improved this case (but the related case where you use
> show-derivations instead of judgment-holds will still be slow because
> there are legitimately a LOT of answers that Redex has to actually
> construct in that case).
>
> Robby
>
> On Fri, Jul 25, 2014 at 1:10 AM,  <dfeltey at ccs.neu.edu> wrote:
>> 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